bridge

MB4 Correction legitimacy

MB4 defeater toy model (manipulated judge)

Spine theorem: AlignmentProofSpine.MB4_defeater_toy_manipulated_judge

Lean spine source

Declarations: MB4_correction_integrity, MB4Crux, preserves_correction_from_mb4_chain

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

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

def MB4Crux : Prop :=
  ∀ (A : System), CorrectionIntegrity A → PreservesCorrectionOperator A

/-- Packaged decomposition for documentation and future threading. -/

theorem preserves_correction_from_mb4_chain (A : System)
    (h : MB4DecomposedCrux) (hint : CorrectionIntegrity A) :
    PreservesCorrectionOperator A :=
  h.2.2.2 A hint

Axiom footprint (headline check)

propext