def
definition
cert_s
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RSBridge.ResidueData on GitHub at line 118.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
115 lo_le_hi := by norm_num
116}
117
118def cert_s : ResidueCert := {
119 f := s,
120 lo := 1396/100, -- 13.96
121 hi := 1397/100,
122 lo_le_hi := by norm_num
123}
124
125def cert_b : ResidueCert := {
126 f := b,
127 lo := 1586/100, -- 15.86
128 hi := 1587/100,
129 lo_le_hi := by norm_num
130}
131
132/-! ## Stability Predicate -/
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