bridge

MB10 Conserved-property signature not forged

Lean spine source

formal/AlignmentProofSpine/Forgeability.lean

Declarations: MB10_conserved_property_signature_not_forged, MB10Crux

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 MB10_conserved_property_signature_not_forged :
  ∀ (A B : System) (δ : Int),
    SuccessorSafe A B →
    ConservedPropertySignatureVerifiable A B →
    RiskGap B ≤ δ → TrueHarm B ≤ δ

def MB10Crux : Prop :=
  ∀ (A B : System) (δ : Int),
    SuccessorSafe A B →
    ConservedPropertySignatureVerifiable A B →
    RiskGap B ≤ δ → TrueHarm B ≤ δ

/-- **MB10**: conserved-property signature is not (cheaply) forged. A
    successor-safe step with bounded measured risk also bounds true harm,
    but only if the conserved-property audit itself was adversarially
    verifiable up to the successor's capability; otherwise "all seven read
    green" is, per `forgeability_gap` and ch31's own WWCTV, evidence of
    nothing against a capable adversarial predecessor. -/