bridge

MB10

Lean spine source

Declarations: MB10_conserved_property_signature_not_forged

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

/-- What `MB10` buys on top of the existing spine: combine the successor-safe
    risk-monotonicity theorem (`SuccessorSafe_risk_monotone`, given the ch48
    audit links `SuccessorAuditLinks`) with `MB10` to turn a predecessor's
    numeric risk bound into a bound on the successor's *true* harm, not just
    its measured risk. This is the corollary a deployment would actually cite
    once it has both a `CertifiedSafetyCase`-style risk bound and a
    verifiable conserved-property audit. -/