bridge

MB2 Bundle identifiability

Lean spine source

formal/AlignmentProofSpine/MB2Identifiability.lean

Declarations: MB2Crux, bundle_aligned_from_mb2_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.

def MB2Crux {nErr nAct k : Nat} : Prop :=
  MB2aCrux (nErr := nErr) (nAct := nAct) (k := k) ∧
  MB2bCrux (nErr := nErr) (nAct := nAct) (k := k) ∧
  MB2c1Crux (nErr := nErr) (nAct := nAct) (k := k)

theorem bundle_aligned_from_mb2_chain {nErr nAct k : Nat}
    (h : @MB2Crux nErr nAct k)
    (E : BundleExperiment nErr nAct k)
    (audit : FinBundleAudit nErr nAct k)
    (hadequate : BundleEvidenceAdequate E)
    (hhost : E.observed = audit.audited)
    (hcausal : FinBundleCausallyControlsPolicy audit.audited)
    (htradeoff : FinBundleTradeoffDirectionMatches audit)
    : BundleAlignedFin ⟨audit⟩ := by
  refine ⟨?_, hcausal, htradeoff⟩
  have hgrad := h.2.1 E audit hhost (h.1 E hadequate)
  exact h.2.2 audit hgrad