theorem
proved
tactic proof
Z_poly_strictly_increasing
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
127end ZMapDerivation
128end RSBridge
129end IndisputableMonolith