Z_lepton_decomposition
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.