integerization_scale
plain-language theorem explainer
The integerization scale supplies the factor k = 6 that converts the electron charge into an integerized value for the Z-map polynomial. It is cited by derivations of the lepton charge index Z_ℓ = 1332 and the integerized charge Q̃_e. The definition is a direct application of the cube_faces function at dimension 3.
Claim. The integerization scale equals the number of faces of the three-dimensional cube, so $k = 6$.
background
Charge integerization in the Z-map derivation uses the factor k equal to the number of faces of the three-dimensional cube. Upstream results define cube_faces(d) as 2d, which evaluates to 6 when d equals 3. This choice provides one independent symmetry channel per face for quantizing charge.
proof idea
One-line definition that applies cube_faces to the dimension 3.
why it matters
This definition provides the integerization factor used by the theorems integerization_scale_eq and Q_tilde_e to derive the lepton index Z_ℓ = 1332. It implements the first step of the Z-map construction, where the even polynomial ansatz is applied to the scaled charge. The construction remains a geometric input rather than a consequence of the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.