bridge

MB1 Estimator soundness

MB1 defeater toy model (calibration-time certificate, later distribution shift)

Spine theorem: AlignmentProofSpine.MB1_defeater_toy_nonstationary_shift

Lean spine source

Declarations: MB1_estimator_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 MB1_estimator_soundness :
  ∀ b : Boundary, EpsilonBoundary 1 b → BoundaryCondition b

/-- MB2: bundle identifiability. Behavioural/internal traces identify stable
    value-bundle geometry well enough to license the bundle-alignment conclusion. -/

Axiom footprint (headline check)

propext