Z_lepton_matches_anchor_value
The theorem proves that the lepton charge index obtained from the minimal even polynomial Z(Q̃) = Q̃² + Q̃⁴ at the integerized electron charge Q̃_e = -6 equals 1332. Researchers building the Recognition Science mass ladder cite it to confirm that the derived Z-map reproduces the hardcoded lepton value in the anchor ZOf definition. The proof is a one-line term-mode simplification that evaluates the polynomial directly from the referenced definitions of Z_poly, Q_tilde_e, and integerization_scale_eq.
claimLet $Z(q) = q^2 + q^4$ be the minimal even polynomial for the charge index. Let $Q̃_e = -6$ be the integerized electron charge obtained by scaling the elementary charge by the face count $k=6$ of the 3-cube. Then $Z(Q̃_e) = 1332$.
background
The Z-Map Derivation module constructs the lepton charge index from charge integerization k = F(3) = 6, the integerized charge Q̃_e = k · Q_e = -6, and the even polynomial ansatz Z(Q̃) = a Q̃² + b Q̃⁴ with minimal coefficients (a,b) = (1,1). The referenced Z_poly definition supplies the evaluation Z_poly a b q := a·q² + b·q⁴, while Q_tilde_e is defined as -(integerization_scale : ℤ). The module doc states that k=6 is a geometric structural input, not derived from T0–T8 alone.
proof idea
The proof is a one-line term-mode wrapper that applies simp to the list [Z_poly, Q_tilde_e, integerization_scale_eq]. This reduces the left-hand side by unfolding the polynomial and the integerization definition, yielding the arithmetic identity 36 + 1296 = 1332.
why it matters in Recognition Science
The result verifies consistency between the polynomial derivation in RSBridge.ZMapDerivation and the hardcoded ZOf value for leptons in Anchor.lean. It supports the mass formula yardstick · phi^(rung - 8 + gap(Z)) by ensuring Z_ℓ = 1332 arises from coefficient minimality rather than fiat. The module notes that the face count k=6 remains an independent geometric choice outside the UnifiedForcingChain.
scope and limits
- Does not derive the integerization scale k=6 from the T0–T8 forcing chain.
- Does not compute actual lepton masses or compare them to experiment.
- Does not prove uniqueness of coefficients beyond the stated minimality condition a ≥ 1, b ≥ 1.
- Does not extend the Z-map to quarks or neutrinos.
formal statement (Lean)
91theorem Z_lepton_matches_anchor_value :
92 Z_poly 1 1 Q_tilde_e = 1332 := by
proof body
Term-mode proof.
93 simp [Z_poly, Q_tilde_e, integerization_scale_eq]
94
95/-- The hardcoded ZOf for the electron is 1332. -/