Z_lepton_eq
The declaration fixes the lepton charge index at 1332 under the minimal even polynomial with integerized charge -6. Researchers deriving lepton masses in the Recognition Science framework cite this to anchor the Z value for the electron. The proof reduces to direct arithmetic evaluation of the polynomial via a native decision procedure that confirms the decomposition 36 + 1296 = 1332.
claim$Z(1,1,-6)=1332$ where $Z(a,b,q):=a q^2 + b q^4$ for $a,b$ natural numbers and $q$ an integer.
background
The module derives the lepton charge index from charge integerization: the face count k=F(3)=6 supplies one independent 2D symmetry channel per face of Q_3, yielding the integerized charge Q̃_e = 6 · (-1) = -6. The even polynomial ansatz Z(Q̃) = a Q̃² + b Q̃⁴ enforces charge-conjugation invariance, neutral vanishing, and non-negative coefficients, with (a,b)=(1,1) the unique minimal pair minimizing a+b under a≥1, b≥1. The upstream Z_poly definition in BaselineDerivation notes that such polynomials are strictly increasing on positive integers when a,b≥1.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the polynomial expression directly, confirming the arithmetic identity 1·(-6)² + 1·(-6)⁴ = 36 + 1296 = 1332.
why it matters in Recognition Science
This result supplies the concrete Z_ℓ=1332 value required by the Z-map derivation for lepton masses on the phi-ladder. It sits inside the RSBridge module that converts the geometric input k=6 into the mass formula yardstick · phi^(rung-8+gap(Z)), consistent with T5 J-uniqueness and the eight-tick octave. The module records that k=6 remains a structural geometric choice not derived from T0-T8, leaving open a deeper justification from the forcing chain.
scope and limits
- Does not derive the face count k=6 from the T0-T8 forcing chain.
- Does not prove uniqueness of (1,1) beyond the stated minimality conditions on a and b.
- Does not connect the result to the alpha band or G constant derivations.
formal statement (Lean)
81theorem Z_lepton_eq : Z_poly 1 1 (-6) = 1332 := by native_decide
proof body
Term-mode proof.
82
83/-- Decomposition: 36 + 1296 = 1332. -/