anchor_electron_Z

formal source

  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) -/
 105
 106theorem Z_poly_strictly_increasing (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
 107    (q₁ q₂ : ℕ) (hq : q₂ < q₁) (_hq₂ : 0 < q₂) :
 108    Z_poly a b q₂ < Z_poly a b q₁ := by
 109  unfold Z_poly
 110  have h2 : (q₂ : ℤ) ^ 2 < (q₁ : ℤ) ^ 2 := by
 111    exact_mod_cast Nat.pow_lt_pow_left hq (by omega)
 112  have h4 : (q₂ : ℤ) ^ 4 < (q₁ : ℤ) ^ 4 := by
 113    exact_mod_cast Nat.pow_lt_pow_left hq (by omega)
 114  have ha' : (0 : ℤ) < a := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
 115  have hb' : (0 : ℤ) < b := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one hb
 116  linarith [mul_lt_mul_of_pos_left h2 ha', mul_lt_mul_of_pos_left h4 hb']
 117
 118/-! ## Summary
 119
 120The lepton charge index Z_ℓ = 1332 is determined by:
 1211. k = F(3) = 6 (cube faces — structural input)
 1222. Q̃_e = -6 (integerized electron charge)
 1233. (a,b) = (1,1) (minimal complete even polynomial)
 1244. Z = Q̃² + Q̃⁴ = 36 + 1296 = 1332
 125-/
 126