proof

P30T Top theorem LayeredAligned ∧ Risk ≤ δ (certified_class_safety_from_spine_and_bridges)

Lean spine source

Declarations: certified_class_safety_from_spine_and_bridges

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.

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_explicit_bridges standardBridges A δ hcert hinv
    hbound hgroundingCert haccess hfilters hbundle hbearer hsucc hpercolation hcci