quark_mass_positive

formal source

  86Each quark mass is a specific phi-power divided by a sector-dependent scale.
  87The formulas are fully determined by cube geometry—no free parameters. -/
  88
  89theorem quark_mass_positive (s : Sector) (r : ℤ) :
  90    0 < rs_mass_MeV s r := by
  91  unfold rs_mass_MeV
  92  apply div_pos
  93  · apply mul_pos
  94    apply mul_pos
  95    apply mul_pos
  96    · exact zpow_pos (by norm_num : (0 : ℝ) < 2) _
  97    · exact zpow_pos Constants.phi_pos _
  98    · exact zpow_pos Constants.phi_pos _
  99    · exact zpow_pos Constants.phi_pos _
 100  · norm_num
 101
 102/-! ## Generation Structure: Torsion Determines Rung Spacing
 103
 104The key structural prediction: within each sector, generation spacing
 105is exactly {0, 11, 17} — the torsion schedule from cube geometry. -/
 106
 107theorem up_generation_spacing :
 108    r_up "c" - r_up "u" = 11 ∧ r_up "t" - r_up "u" = 17 := by
 109  simp only [r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
 110             cube_edges, active_edges_per_tick, D, wallpaper_groups]
 111  omega
 112
 113theorem down_generation_spacing :
 114    r_down "s" - r_down "d" = 11 ∧ r_down "b" - r_down "d" = 17 := by
 115  simp only [r_down, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
 116             cube_edges, active_edges_per_tick, D, wallpaper_groups]
 117  omega
 118
 119/-! ## Mass Ratio Predictions (Sector-Internal)