StabilityCert

formal source

 133
 134/-- A fermion's residue is stable if its certificate is valid and the
 135    stationarity axiom holds at the canonical anchor. -/
 136structure StabilityCert (f : Fermion) where
 137  cert : ResidueCert
 138  cert_matches : cert.f = f
 139  cert_valid : cert.valid
 140
 141/-! ## Connection to AnchorPolicy -/
 142
 143/-- The canonical anchor from AnchorPolicy. -/
 144noncomputable def canonicalAnchorSpec : AnchorSpec := canonicalAnchor
 145
 146/-- At the canonical anchor, the display identity should hold:
 147    f_residue f μ⋆ = F(ZOf f) = gap(ZOf f)
 148
 149    This is the axiom `display_identity_at_anchor` from AnchorPolicy.
 150    The certificates above provide numerical bounds to verify this. -/
 151theorem display_identity_uses_gap (f : Fermion) :
 152    F (ZOf f) = gap (ZOf f) := rfl
 153
 154/-! ## Robustness Check Interface -/
 155
 156/-- Check if a certificate's bounds are within the AnchorPolicy tolerance of
 157    the theoretical gap. -/
 158def certificateWithinTolerance (c : ResidueCert) : Prop :=
 159  let theoretical := gap (ZOf c.f)
 160  (c.lo : ℝ) - anchorTolerance ≤ theoretical ∧
 161  theoretical ≤ (c.hi : ℝ) + anchorTolerance
 162
 163/-! ## Summary Statistics -/
 164
 165/-- The lepton certificates cluster around F(1332) ≈ 13.95. -/
 166def leptonCerts : List ResidueCert := [cert_e, cert_mu, cert_tau]