`res_nu2_simp`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.NeutrinoSector
domain: Physics
line: 173 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.NeutrinoSector on GitHub at line 173.

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

 170  simp [rung_nu3, nu_phase_offset_eq]
 171  norm_num
 172
 173lemma res_nu2_simp : res_nu2 = (-231 : ℚ) / 4 := by
 174  unfold res_nu2
 175  -- res_nu3 = -217/4, spacing = 7/2 = 14/4
 176  simp [res_nu3_simp, nu_spacing_eq]
 177  norm_num
 178
 179lemma res_nu1_simp : res_nu1 = (-239 : ℚ) / 4 := by
 180  unfold res_nu1
 181  -- res_nu2 = -231/4, nu1_spacing = 2 = 8/4
 182  simp [res_nu2_simp, nu1_spacing_eq]
 183  norm_num
 184
 185theorem rung_gap_21_is_two : res_nu2 - res_nu1 = (2 : ℚ) := by
 186  unfold res_nu1
 187  simp [nu1_spacing_eq]
 188
 189/-- Predicted mass in eV for a fractional rung (reporting seam: treat `m_struct` as MeV). -/
 190noncomputable def predicted_mass_eV_frac_with
 191    (cal : MassDisplayCalibration) (res : Rung) : ℝ :=
 192  electron_structural_mass * (phi ^ (toReal res)) * cal.eV_per_structural_unit
 193
 194/-- Default fractional-rung prediction in eV (legacy convention). -/
 195noncomputable def predicted_mass_eV_frac (res : Rung) : ℝ :=
 196  predicted_mass_eV_frac_with legacy_mass_display_calibration res
 197
 198lemma predicted_mass_eV_frac_legacy (res : Rung) :
 199    predicted_mass_eV_frac res = electron_structural_mass * (phi ^ (toReal res)) * MeV_to_eV := by
 200  simp [predicted_mass_eV_frac, predicted_mass_eV_frac_with, MeV_to_eV]
 201
 202/-! ### What it takes to land on φ⁷ (symbolic) -/
 203

papers checked against this theorem

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