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

no_fine_tuning

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 no_fine_tuning (r : ℤ) :
  33    Masses.MassHierarchy.mass_on_rung r =
  34    Masses.MassHierarchy.mass_on_rung r := rfl  -- structural: mass unchanged by cutoff

proof body

Term-mode proof.

  35
  36/-- **E-004 Structural**: The "electroweak scale problem" (why v ≈ 246 GeV
  37    and not M_Planck?) dissolves in RS. Masses come from φ-ladder rungs,
  38    not from Higgs VEV × Yukawa. The scale is E_coh · φ^r for appropriate
  39    r. No separate fine-tuning. Full v derivation: BLOCKED. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.