unit_coefficients_minimal

formal source

  71  fun _ _ ha hb => by omega
  72
  73/-- (1,1) achieves the minimum. -/
  74theorem unit_coefficients_minimal :
  75    ∀ a b : ℕ, 1 ≤ a → 1 ≤ b → 1 + 1 ≤ a + b :=
  76  fun _ _ ha hb => by omega
  77
  78/-! ## The Derivation: Z_ℓ = 1332 -/
  79
  80/-- Z_poly with (a,b) = (1,1) at Q̃ = -6 gives 1332. -/
  81theorem Z_lepton_eq : Z_poly 1 1 (-6) = 1332 := by native_decide
  82
  83/-- Decomposition: 36 + 1296 = 1332. -/
  84theorem Z_lepton_decomposition :
  85    (1 : ℤ) * (-6) ^ 2 = 36 ∧
  86    (1 : ℤ) * (-6) ^ 4 = 1296 ∧
  87    (36 : ℤ) + 1296 = 1332 := by
  88  refine ⟨by norm_num, by norm_num, by norm_num⟩
  89
  90/-- Consistency: the derived Z equals 1332, matching Anchor.lean's hardcoded value. -/
  91theorem Z_lepton_matches_anchor_value :
  92    Z_poly 1 1 Q_tilde_e = 1332 := by
  93  simp [Z_poly, Q_tilde_e, integerization_scale_eq]
  94
  95/-- The hardcoded ZOf for the electron is 1332. -/
  96theorem anchor_electron_Z : RSBridge.ZOf .e = 1332 := rfl
  97
  98/-- All three leptons share the same charge index. -/
  99theorem leptons_same_Z :
 100    RSBridge.ZOf .e = RSBridge.ZOf .mu ∧
 101    RSBridge.ZOf .mu = RSBridge.ZOf .tau := by
 102  exact ⟨rfl, rfl⟩
 103
 104/-! ## Z is strictly increasing (for hierarchy ordering) -/