pith. machine review for the scientific record. sign in
theorem proved term proof

mass_ratio_geometric

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  32theorem mass_ratio_geometric :
  33    Masses.MassHierarchy.mass_on_rung (r_lepton "mu") / Masses.MassHierarchy.mass_on_rung (r_lepton "e") =
  34      phi ^ 11 :=

proof body

Term-mode proof.

  35  Masses.MassHierarchy.lepton_hierarchy_geometric.1
  36
  37/-- **P-013 Resolution**: The hierarchy "problem" dissolves in RS because:
  38    1. Masses = E_coh · φ^r (from ledger rung)
  39    2. No Yukawa couplings as free parameters
  40    3. No divergent radiative corrections to scalar masses
  41    4. The φ-ladder spacing is fixed by dimension (F-003) and φ-forcing (C-003)
  42
  43    The Standard Model hierarchy problem assumes masses come from
  44    renormalization; in RS they come from geometry. -/

depends on (24)

Lean names referenced from this declaration's body.