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, MB1Crux

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

-- MB2 is not a `BridgeAssumptions` field; see `MB2Identifiability.lean` (`MB2Crux`).

/-- MB3: bearer import. Preserved bearer maps under a substrate translation make
    value-bundle transport more than merely semantic. -/

def MB1Crux : Prop :=
  ∀ b : Boundary, EpsilonBoundary 1 b → BoundaryCondition b

Axiom footprint (headline check)

propext