Z_poly_even

formal source

  55def Z_poly (a b : ℕ) (q : ℤ) : ℤ := (a : ℤ) * q ^ 2 + (b : ℤ) * q ^ 4
  56
  57/-- Z is even: Z(Q̃) = Z(-Q̃). -/
  58theorem Z_poly_even (a b : ℕ) (q : ℤ) :
  59    Z_poly a b q = Z_poly a b (-q) := by
  60  unfold Z_poly; ring
  61
  62/-- Z vanishes at neutral: Z(0) = 0. -/
  63theorem Z_poly_zero (a b : ℕ) : Z_poly a b 0 = 0 := by
  64  unfold Z_poly; ring
  65
  66/-! ## Coefficient Minimality -/
  67
  68/-- The minimal choice: both terms present, minimum a + b. -/
  69theorem minimal_coefficients :
  70    ∀ a b : ℕ, 1 ≤ a → 1 ≤ b → 2 ≤ a + b :=
  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⟩