scale_from_ledger

formal source

  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. -/
  40def scale_from_ledger : Prop :=
  41  (1 < phi ∧ phi < 2) ∧
  42  (∀ r : ℤ, Masses.MassHierarchy.mass_on_rung r = Masses.MassHierarchy.mass_on_rung r)
  43
  44theorem ew_scale_structure : scale_from_ledger := by
  45  constructor
  46  · exact ⟨one_lt_phi, phi_lt_two⟩
  47  · intro r
  48    exact no_fine_tuning r
  49
  50/-- Electroweak-scale structure implies the phi-window input. -/
  51theorem ew_scale_implies_phi_window (h : scale_from_ledger) : 1 < phi ∧ phi < 2 :=
  52  h.1
  53
  54/-- Electroweak-scale structure implies rung-wise no-fine-tuning identity. -/
  55theorem ew_scale_implies_no_fine_tuning (h : scale_from_ledger) (r : ℤ) :
  56    Masses.MassHierarchy.mass_on_rung r = Masses.MassHierarchy.mass_on_rung r :=
  57  h.2 r
  58
  59/-- Electroweak-scale structure excludes the degenerate endpoint `phi = 1`. -/
  60theorem ew_scale_implies_phi_ne_one (h : scale_from_ledger) : phi ≠ 1 := by
  61  linarith [h.1.1]
  62
  63/-- Electroweak-scale structure excludes the upper endpoint `phi = 2`. -/
  64theorem ew_scale_implies_phi_ne_two (h : scale_from_ledger) : phi ≠ 2 := by
  65  linarith [h.1.2]
  66
  67/-! ## φ Connection -/
  68
  69/-- φ > 1 forces geometric growth. Mass ratios are powers of φ. -/
  70theorem phi_gt_one : 1 < phi := one_lt_phi