`QuarkAbsoluteMassResidual`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.QuarkScoreCard
domain: Masses
line: 172 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.QuarkScoreCard on GitHub at line 172.

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

used by

formal source

 169    formula and the gap-corrected `massAtAnchor` formula on a chosen
 170    quark sector. A proof of this proposition would close the absolute
 171    quark-mass row of the scorecard. -/
 172def QuarkAbsoluteMassResidual : Prop :=
 173  ∀ (f : Fermion),
 174    sectorOf f = Sector.up →
 175    Verification.rs_mass_MeV Anchor.Sector.UpQuark (RSBridge.rung f)
 176      = M0 * Real.exp (((RSBridge.rung f : ℝ) - 8 + gap (ZOf f)) *
 177            Real.log Constants.phi)
 178
 179/-! ## ScoreCard certificate
 180
 181A single record bundling every theorem-grade row of this Phase 0
 182deliverable. -/
 183
 184structure QuarkScoreCardCert where
 185  ZOf_up : ZOf .u = 276 ∧ ZOf .c = 276 ∧ ZOf .t = 276
 186  ZOf_down : ZOf .d = 24 ∧ ZOf .s = 24 ∧ ZOf .b = 24
 187  ZOf_lep : ZOf .e = 1332 ∧ ZOf .mu = 1332 ∧ ZOf .tau = 1332
 188  charm_up_ratio_eq :
 189    Verification.charm_quark_pred / Verification.up_quark_pred =
 190      Constants.phi ^ (11 : ℕ)
 191  top_charm_ratio_eq :
 192    Verification.top_quark_pred / Verification.charm_quark_pred =
 193      Constants.phi ^ (6 : ℕ)
 194  top_in_band : (10000 : ℝ) < Verification.top_quark_pred ∧
 195      Verification.top_quark_pred < 1000000
 196  quark_preds_pos : 0 < Verification.up_quark_pred ∧
 197      0 < Verification.charm_quark_pred ∧ 0 < Verification.top_quark_pred
 198  electron_pct :
 199    |Verification.rs_mass_MeV .Lepton 2 - Verification.m_e_exp| /
 200        Verification.m_e_exp < 0.003
 201  muon_pct :
 202    |Verification.rs_mass_MeV .Lepton 13 - Verification.m_mu_exp| /

papers checked against this theorem

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