bridge

To MB7d Inferential detector validity

Lean spine source

Declarations: MB7d_inferential_uad_detector_soundness

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 MB7d_inferential_uad_detector_soundness :
  ∀ A : System, AccessRobust A → InferentialDetectorAdequate A → InferentialCouplingMeasurementValid A

/-- MB8 (legacy / gravestone). Preserving a human value-update operator was once
    packaged as an alternate route to `CorrectionIntegrity`. CEV now factorizes
    through `AlignmentConstruction.constitutionalTarget`; this axiom remains for
    the Chokepoint `MB6b` vs `MB8` worked instance only — not in
    `BridgeAssumptions`. -/