`step_e_mu`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs
domain: RRF
line: 37 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  34
  35/-- Step 1: Electron to Muon.
  36    Driven by Passive Edges (11) and Spherical Geometry (1/4π). -/
  37noncomputable def step_e_mu : ℝ :=
  38  (E_passive : ℝ) + 1 / (4 * Real.pi) - α ^ 2
  39
  40/-- Step 2: Muon to Tau.
  41    Driven by Faces (6) and Wallpaper Symmetry (17). -/
  42noncomputable def step_mu_tau : ℝ :=
  43  (cube_faces 3 : ℝ) - (2 * wallpaper_groups + 3) / 2 * α
  44
  45/-! ## Predicted Residues -/
  46
  47/-- Predicted Muon Residue. -/
  48noncomputable def predicted_residue_mu : ℝ :=
  49  (gap 1332 - refined_shift) + step_e_mu
  50
  51/-- Predicted Tau Residue. -/
  52noncomputable def predicted_residue_tau : ℝ :=
  53  predicted_residue_mu + step_mu_tau
  54
  55/-! ## Mass Predictions -/
  56
  57/-- Predicted Muon Mass. -/
  58noncomputable def predicted_mass_mu : ℝ :=
  59  electron_structural_mass * phi ^ predicted_residue_mu
  60
  61/-- Predicted Tau Mass. -/
  62noncomputable def predicted_mass_tau : ℝ :=
  63  electron_structural_mass * phi ^ predicted_residue_tau
  64
  65end LeptonGenerations
  66end Physics
  67end IndisputableMonolith

papers checked against this theorem

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