`gap_down_theory`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RSBridge.ResidueData on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  42
  43/-- Theoretical gap for Down Quarks: F(24).
  44    Numerically: ln(1 + 24/φ) / ln(φ) ≈ 5.74 -/
  45noncomputable def gap_down_theory : ℝ := gap (ZOf d)
  46
  47/-! ## Verification: Z values match canonical bands -/
  48
  49theorem lepton_Z_is_1332 : ZOf e = 1332 := by native_decide
  50theorem up_Z_is_276 : ZOf u = 276 := by native_decide
  51theorem down_Z_is_24 : ZOf d = 24 := by native_decide
  52
  53/-! ## Lepton Certificates
  54    Leptons fit the integer rung model well.
  55    Audit data (delta shifted by +34.66):
  56    - e:   13.954
  57    - μ:   14.034
  58    - τ:   13.899
  59    Theoretical target: F(1332) ≈ 13.954
  60-/
  61
  62def cert_e : ResidueCert := {
  63  f := e,
  64  lo := 1395/100,  -- 13.95
  65  hi := 1396/100,  -- 13.96
  66  lo_le_hi := by norm_num
  67}
  68
  69def cert_mu : ResidueCert := {
  70  f := mu,
  71  lo := 1403/100,  -- 14.03
  72  hi := 1404/100,  -- 14.04
  73  lo_le_hi := by norm_num
  74}
  75

papers checked against this theorem

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