Z_lepton_matches_anchor_value
plain-language theorem explainer
The declaration shows that the minimal-coefficient even polynomial Z(Q̃) = Q̃² + Q̃⁴ evaluates to exactly 1332 at the integerized electron charge Q̃_e = -6. Researchers deriving lepton masses within the Recognition Science mass ladder cite this result to confirm consistency between the polynomial ansatz and the hardcoded ZOf anchor. The proof is a direct term-mode simplification that substitutes the definitions of Z_poly, Q_tilde_e, and the integerization scale equation.
Claim. $Z(1,1, Q̃_e) = 1332$, where $Z(a,b,q) = a q^2 + b q^4$ for natural numbers $a,b$ and $Q̃_e = -6$ is the integerized electron charge obtained by scaling the elementary charge by the cube-face count $k=6$.
background
This module derives the lepton charge index Z_ℓ from a minimal even polynomial ansatz that enforces charge-conjugation invariance, neutral vanishing, and non-negative coefficients. Z_poly(a,b,q) is the even polynomial a q² + b q⁴; the integerized charge Q_tilde_e is defined as -(integerization_scale) with the scale equal to 6 from the geometric choice of three cube faces supplying independent 2D symmetry channels for quantization. The local theoretical setting is the Z-map construction that produces Z_ℓ = 1332 to align with the lepton sector of the anchor definition ZOf, where leptons are assigned qq + qqqq.
proof idea
The proof is a one-line term-mode simplification that unfolds Z_poly(1,1,Q_tilde_e) together with the equation for the integerization scale. Substituting Q_tilde_e = -6 directly yields 1*(-6)² + 1*(-6)⁴ = 36 + 1296 = 1332.
why it matters
This theorem closes the consistency loop between the derived polynomial in RSBridge.ZMapDerivation and the hardcoded ZOf anchor used for fermion mass rungs. It supports the overall mass formula by fixing the Z value for the lepton sector at 1332 and validates the choice of minimal coefficients (a,b)=(1,1) under the even-polynomial ansatz. The result sits downstream of the charge integerization step documented as a geometric structural input and feeds into any mass derivation that invokes ZOf for leptons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.