Z_poly

formal source

 243The minimal solution is (a, b) = (1, 1). -/
 244
 245/-- Z-map polynomial for the charge index. -/
 246def Z_poly (a b : ℕ) (q : ℤ) : ℤ := a * q^2 + b * q^4
 247
 248/-- **B-26 DERIVED**: If a ≥ 1 and b ≥ 1, then Z is strictly increasing
 249    on the positive integers: q₁ > q₂ > 0 implies Z(q₁) > Z(q₂). -/
 250theorem Z_strictly_increasing (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
 251    (q₁ q₂ : ℕ) (hq : q₂ < q₁) (hq₂ : 0 < q₂) :
 252    Z_poly a b q₂ < Z_poly a b q₁ := by
 253  unfold Z_poly
 254  have h1 : (q₂ : ℤ) ^ 2 < (q₁ : ℤ) ^ 2 := by
 255    have := Nat.pow_lt_pow_left hq (n := 2) (by omega)
 256    exact_mod_cast this
 257  have h2 : (q₂ : ℤ) ^ 4 < (q₁ : ℤ) ^ 4 := by
 258    have := Nat.pow_lt_pow_left hq (n := 4) (by omega)
 259    exact_mod_cast this
 260  have ha' : (0 : ℤ) < a := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one ha
 261  have hb' : (0 : ℤ) < b := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_one hb
 262  have h1' := mul_lt_mul_of_pos_left h1 ha'
 263  have h2' := mul_lt_mul_of_pos_left h2 hb'
 264  linarith
 265
 266/-- The minimal complete solution is (a, b) = (1, 1). -/
 267theorem minimal_complete_coefficients :
 268    ∀ a b : ℕ, 1 ≤ a → 1 ≤ b → a + b ≥ 2 :=
 269  fun a b ha hb => by omega
 270
 271/-! ## Derived Rung Table — All Three Sectors
 272
 273With the baseline rungs and generation torsion derived above, we can
 274state the complete rung table as cube-geometric consequences. -/
 275
 276/-- Lepton rungs: r_e, r_μ, r_τ -/