theorem
proved
leptons_same_Z
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RSBridge.ZMapDerivation on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
127end ZMapDerivation
128end RSBridge
129end IndisputableMonolith