proof

P30T Top theorem LayeredAligned ∧ Risk ≤ δ (certified_class_safety_from_spine_and_bridges)

Lean spine source

formal/AlignmentProofSpine/Certification.lean

Declarations: certified_class_safety_from_spine_and_bridges, certified_class_safety_from_core_cruxes

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.

theorem certified_class_safety_from_spine_and_bridges
    (A : System) (δ : Int)
    (hcert : Certified A)
    (hinv : SatisfiesInvariants A)
    (hbound : BoundaryAligned A)
    (hgroundingCert : GroundingCertificate A)
    (haccess : AccessModelAdequate A)
    (hfilters : FilterCoverageAdequate A)
    (hbundle : BundleTransport A)
    (hbearer : BearerTransport A)
    (hsucc : SuccessorStable A)
    (hpercolation : PercolationEvidenceSys A)
    (hcci : Control A ≤ CCI A + δ) :
    CertifiedSafetyCase A δ :=
  certified_class_safety_from_bridge_record standardBridges A δ
    { certified := hcert
      invariants := hinv
      direct :=
        { boundary := hbound
          bundle := hbundle
          bearer := hbearer
          successor := hsucc }
      bridgeInputs :=
        { groundingCert := hgroundingCert
          access := haccess
          filters := hfilters
          percolation := hpercolation }
      numeric := { cci_slack := hcci } }

/-- Same assembly as `certified_class_safety_from_spine_and_bridges`, with core
    bridge content threaded as explicit `CoreBridgeCruxes` hypotheses. -/

theorem certified_class_safety_from_core_cruxes
    (cruxes : CoreBridgeCruxes)
    (A : System) (δ : Int)
    (hcert : Certified A)
    (hinv : SatisfiesInvariants A)
    (hbound : BoundaryAligned A)
    (hgroundingCert : GroundingCertificate A)
    (haccess : AccessModelAdequate A)
    (hfilters : FilterCoverageAdequate A)
    (hbundle : BundleTransport A)
    (hbearer : BearerTransport A)
    (hsucc : SuccessorStable A)
    (hpercolation : PercolationEvidenceSys A)
    (hcci : Control A ≤ CCI A + δ) :
    CertifiedSafetyCase A δ :=
  certified_class_safety_from_bridge_record cruxes.toBridgeAssumptions A δ
    { certified := hcert
      invariants := hinv
      direct :=
        { boundary := hbound
          bundle := hbundle
          bearer := hbearer
          successor := hsucc }
      bridgeInputs :=
        { groundingCert := hgroundingCert
          access := haccess
          filters := hfilters
          percolation := hpercolation }
      numeric := { cci_slack := hcci } }