Q_tilde_e

formal source

  42theorem integerization_scale_eq : integerization_scale = 6 := by native_decide
  43
  44/-- The integerized electron charge: Q̃_e = k · Q_e = 6 · (-1) = -6. -/
  45def Q_tilde_e : ℤ := -(integerization_scale : ℤ)
  46
  47theorem Q_tilde_e_eq : Q_tilde_e = -6 := by
  48  simp [Q_tilde_e, integerization_scale_eq]
  49
  50/-! ## Even Polynomial Ansatz -/
  51
  52/-- The charge index polynomial: Z(Q̃) = a·Q̃² + b·Q̃⁴.
  53    Even in Q̃ (charge-conjugation invariance), no constant term
  54    (neutral vanishing), non-negative coefficients. -/
  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 :=