def
definition
cert_u
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 88.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
85 Theoretical target: F(276) ≈ 10.71 (up) or F(24) ≈ 5.74 (down)
86-/
87
88def cert_u : ResidueCert := {
89 f := u,
90 lo := 1170/100, -- 11.70
91 hi := 1171/100, -- 11.71
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 := {