`certificateWithinTolerance`

definition

show as: view math explainer →

module: IndisputableMonolith.RSBridge.ResidueData
domain: RSBridge
line: 158 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RSBridge.ResidueData on GitHub at line 158.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 155
 156/-- Check if a certificate's bounds are within the AnchorPolicy tolerance of
 157    the theoretical gap. -/
 158def certificateWithinTolerance (c : ResidueCert) : Prop :=
 159  let theoretical := gap (ZOf c.f)
 160  (c.lo : ℝ) - anchorTolerance ≤ theoretical ∧
 161  theoretical ≤ (c.hi : ℝ) + anchorTolerance
 162
 163/-! ## Summary Statistics -/
 164
 165/-- The lepton certificates cluster around F(1332) ≈ 13.95. -/
 166def leptonCerts : List ResidueCert := [cert_e, cert_mu, cert_tau]
 167
 168/-- The quark certificates show more variation due to Quarter-Ladder effects. -/
 169def quarkCerts : List ResidueCert := [cert_u, cert_c, cert_t, cert_d, cert_s, cert_b]
 170
 171/-- All fermion certificates. -/
 172def allCerts : List ResidueCert := leptonCerts ++ quarkCerts
 173
 174end RSBridge
 175end IndisputableMonolith

papers checked against this theorem

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