def
definition
cert_c
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RSBridge.ResidueData on GitHub at line 95.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
92 lo_le_hi := by norm_num
93}
94
95def cert_c : ResidueCert := {
96 f := c,
97 -- NOTE: Charm matches Lepton gap (13.95), not Up gap (10.71)!
98 -- This suggests Charm has special structure or the Quarter-Ladder applies.
99 lo := 1395/100,
100 hi := 1396/100,
101 lo_le_hi := by norm_num
102}
103
104def cert_t : ResidueCert := {
105 f := t,
106 lo := 1816/100, -- 18.16
107 hi := 1817/100, -- 18.17
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 := {