recognition / Masses / Masses.MassLaw / gap_zero_neutral

theorem

`gap_zero_neutral`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.MassLaw
domain: Masses
line: 75 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.MassLaw on GitHub at line 75.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

Derivations using this theorem

Mass Spectrum on the Phi-Ladder · foundational / THEOREM
All Standard-Model masses follow m = yardstick * phi^{rung - 8 + gap(Z)}

depends on

formal source

  72
  73/-- The "gap" term corrects for the charge-based shift.
  74    When Z=0 (neutral sector baseline), gap(0) = 0. -/
  75theorem gap_zero_neutral : gap_correction 0 = 0 := by
  76  unfold gap_correction
  77  simp only [Int.cast_zero, zero_div, add_zero, Real.log_one, zero_div]
  78
  79end MassLaw
  80end Masses
  81end IndisputableMonolith

papers checked against this theorem

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