Q_tilde_e_eq
The theorem fixes the integerized electron charge at negative six. Workers deriving lepton mass indices via the even polynomial ansatz in Recognition Science cite it to anchor the Z-map step. The term proof reduces immediately by simplification of the defining expression together with the scale equality.
claimLet $k=6$ be the integerization scale and let $Q_e=-1$ be the elementary charge. The integerized electron charge then satisfies $kQ_e=-6$.
background
The module derives the lepton charge index from charge integerization, where $k=F(3)=6$ counts the faces of the cube $Q_3$ and supplies one independent 2D symmetry channel per face. The integerized charge is defined directly as the negation of this scale, so that the electron maps to $-6$. Upstream, the integer map $Z$ from Masses.Anchor applies the same scaling to produce the lepton index as $Q_6^2+Q_6^4$, while the companion theorem integerization_scale_eq records the concrete value $k=6$ by native decision.
proof idea
The proof is a one-line term-mode wrapper that applies simp to unfold the definition of the integerized charge and substitute the scale equality.
why it matters in Recognition Science
This supplies the concrete input value for the even polynomial ansatz $Z(Q̃)=aQ̃^2+bQ̃^4$ that yields the lepton index 1332. It implements the geometric charge-integerization step documented in the module, a structural choice outside the T0-T8 forcing chain. The result closes the definition of the integerized charge for use in the subsequent mass-ladder formulas.
scope and limits
- Does not derive the scale factor $k=6$ from the T0-T8 chain.
- Does not prove the even polynomial ansatz or coefficient minimality.
- Does not compute the resulting lepton index 1332.
- Does not address integerization for quarks or other sectors.
formal statement (Lean)
47theorem Q_tilde_e_eq : Q_tilde_e = -6 := by
proof body
Term-mode proof.
48 simp [Q_tilde_e, integerization_scale_eq]
49
50/-! ## Even Polynomial Ansatz -/
51
52/-- The charge index polynomial: Z(Q̃) = a·Q̃² + b·Q̃⁴.
53 Even in Q̃ (charge-conjugation invariance), no constant term
54 (neutral vanishing), non-negative coefficients. -/