Towards Superintelligence Alignment
bridge

Lean proof spine

MB9 Grounding certificate soundness

Lean spine source

formal/Core.lean

Declarations: MB9_grounding_certificate_soundness

From the machine-checked spine in formal/ (Mathlib + spine imports). 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 nine `Core.lean`-level bridge assumptions packaged as one record.
    Constructing `standardBridges` forces every `MB1`–`MB9` axiom to be
    referenced; some bridges are alternate routes or legacy comparison points
    rather than the live certification path. `MB10` is not a field here (see
    `AlignmentProofSpine.Forgeability`): it needs the numeric risk leaf, which
    does not exist at this point in the module order. -/