bridge

MB8 CEV / process convergence

MB8 defeater toy model (legitimacy theater)

Spine theorem: AlignmentProofSpine.MB8_defeater_toy_legitimacy_theater

Lean spine source

Declarations: MB8_cev_process_convergence, constitutionalTarget, TargetRealizable

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 MB8_cev_process_convergence :
  ∀ (A : System) (U : ValueUpdateOperator), PreservesValueUpdateOperator A U → CorrectionIntegrity A

/-- MB9: grounding certificate validity. A certified conservative abstraction
    warrants the abstract grounding-viability layer in the deployment domain. -/

def constitutionalTarget (C : ConstitutionalRule) : AlignmentTarget where
  requiresCorrectionChannel := C.extrapolation
  requiresBundleStructure := C.aggregation

def TargetRealizable (P : AlignmentTarget) : Prop :=
  ∃ A : System, Realizes A P

/-- Field-facing alias for the open construction crux (Krym §9; not an `MB*` bridge). -/

Axiom footprint (headline check)

propext