Q_tilde_e_eq
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.