Z_lepton_decomposition
The declaration verifies the arithmetic decomposition 36 + 1296 = 1332 for the lepton Z index built from integerized charge -6 under the even polynomial ansatz. Researchers anchoring lepton masses on the Recognition Science ladder would cite it to confirm consistency with the hardcoded Anchor value. The proof is a one-line term-mode wrapper that applies norm_num to each conjunct.
claimFor integerized charge $Q̃_e = -6$, the minimal even polynomial $Z(Q̃) = 1·Q̃² + 1·Q̃⁴$ satisfies $1·(-6)² = 36$, $1·(-6)⁴ = 1296$, and $36 + 1296 = 1332$.
background
The module derives lepton Z from charge integerization k = F(3) = 6 (one 2D symmetry channel per face of Q₃), giving Q̃_e = 6·(-1) = -6. The even polynomial ansatz Z(Q̃) = a·Q̃² + b·Q̃⁴ enforces charge-conjugation invariance and non-negativity, with coefficient minimality selecting (a,b) = (1,1). Upstream Anchor.Z for the Lepton sector defines Z(Q) := (Q6)² + (Q6)⁴ where Q6 = 6Q, so the theorem simply checks that this expression evaluates to 1332 at Q = -1.
proof idea
The proof is a one-line term-mode wrapper that applies norm_num to verify each of the three conjuncts.
why it matters in Recognition Science
This result closes the Z-map derivation by confirming the computed Z_ℓ = 1332 matches the Anchor value used in mass formulas. It supplies the concrete numerical anchor for the lepton sector on the phi-ladder without requiring the full T0-T8 forcing chain, relying instead on the geometric input k=6. The module doc states the outcome directly: Z_ℓ = 1·(-6)² + 1·(-6)⁴ = 36 + 1296 = 1332.
scope and limits
- Does not derive k=6 from T0-T8 alone.
- Does not prove coefficient minimality beyond the stated ansatz.
- Does not compute actual masses or apply phi-ladder scaling.
- Does not address quark sectors or other species.
formal statement (Lean)
84theorem Z_lepton_decomposition :
85 (1 : ℤ) * (-6) ^ 2 = 36 ∧
86 (1 : ℤ) * (-6) ^ 4 = 1296 ∧
87 (36 : ℤ) + 1296 = 1332 := by
proof body
Term-mode proof.
88 refine ⟨by norm_num, by norm_num, by norm_num⟩
89
90/-- Consistency: the derived Z equals 1332, matching Anchor.lean's hardcoded value. -/