Towards Superintelligence Alignment
bridge

Lean proof spine

To MB7d Inferential detector validity

Lean spine source

formal/Core.lean

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

/-- MB8: legacy CEV/process bridge. If an external theory certifies preservation
    of a human value-update process, that suffices for correction integrity
    without knowing a final fixed point. The main certification path does not
    rely on this opaque route; it uses grounding, correction, and adversarial
    layer evidence directly. -/