bridge

MB4 Correction legitimacy

MB4 defeater toy model (manipulated judge)

Spine theorem: AlignmentProofSpine.MB4_defeater_toy_manipulated_judge

Lean spine source

Declarations: MB4_correction_legitimacy

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 MB4_correction_legitimacy :
  ∀ A : System, CorrectionIntegrity A → PreservesCorrectionOperator A

/-- MB5: ontology-shift successor audit. Full transport plus bearer transport
    surviving an ontology shift compose into successor safety. -/

Axiom footprint (headline check)

propext