bridge

MB9 Grounding certificate soundness

Lean spine source

Declarations: MB9_grounding_certificate_soundness, MB9Crux

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

axiom MB9_grounding_certificate_soundness :
  ∀ A : System, GroundingCertificate A → GroundingViable A

/-- All `Core.lean`-level bridge assumptions packaged as one record.
    Constructing `standardBridges` forces every live `MB1`–`MB9` axiom to be
    referenced. **MB2** and **MB8** are threaded outside this record (finite
    `MB2Crux` hypotheses and legacy `MB8_cev_process_convergence` for the
    Chokepoint worked instance, respectively). `MB10` is not a field here (see
    `AlignmentProofSpine.Forgeability`). -/

def MB9Crux : Prop :=
  ∀ A : System, GroundingCertificate A → GroundingViable A