pith. machine review for the scientific record. sign in
theorem proved term proof high

anchor_electron_Z

show as:
view Lean formalization →

The electron charge index evaluates to 1332 under the lepton-sector formula of ZOf. Researchers modeling lepton masses on the phi-ladder cite this fixed anchor when placing the electron rung. The proof is a one-line reflexivity that evaluates the definition of ZOf on the electron.

claim$Z(e) = 1332$, where $Z$ is the lepton charge index given by $q^2 + q^4$ evaluated at the integerized charge $q = -6$.

background

The Z-map assigns an integer charge index to each fermion. For leptons the index follows the even polynomial $Z = q^2 + q^4$ with $q = tildeQ(f)$, while quarks receive an extra offset of 4. The integerization step sets $tildeQ_e = 6 times (-1) = -6$, where the prefactor 6 equals the face count of the 3-cube and supplies one independent 2D symmetry channel per face. This construction is stated as a geometric structural input rather than a consequence of the T0-T8 forcing chain.

proof idea

The proof is a one-line reflexivity that directly evaluates the definition of ZOf on the electron fermion.

why it matters in Recognition Science

This theorem supplies the concrete anchor value 1332 for the electron in the Z-map derivation. It supports the sibling results on Z_lepton_eq and Z_lepton_decomposition that decompose the lepton indices. Within the Recognition framework it fixes the starting rung for the electron mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)), closing the charge-integerization step that precedes the phi-ladder mass assignments. The module notes that the face count k=6 is a geometric input rather than a consequence of the T0-T8 forcing chain.

scope and limits

formal statement (Lean)

  96theorem anchor_electron_Z : RSBridge.ZOf .e = 1332 := rfl

proof body

Term-mode proof.

  97
  98/-- All three leptons share the same charge index. -/

depends on (3)

Lean names referenced from this declaration's body.