def
definition
cert_d
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RSBridge.ResidueData on GitHub at line 111.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
108 lo_le_hi := by norm_num
109}
110
111def cert_d : ResidueCert := {
112 f := d,
113 lo := 1875/100, -- 18.75 (shifted)
114 hi := 1876/100,
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 -/