 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 := {
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.