integerization_scale_eq
plain-language theorem explainer
The theorem fixes the integerization scale at exactly 6, the face count of a 3-cube. Workers deriving the lepton index Z_ℓ = 1332 in the Z-Map module cite it to lock the quantization factor before the even-polynomial step. The proof is a one-line native_decide that evaluates the constant definition cube_faces 3.
Claim. $k = F(3) = 6$, where $k$ is the integerization scale and $F(3)$ counts the faces of the 3-cube.
background
The Z-Map Derivation module derives the lepton charge index Z_ℓ = 1332 from charge integerization followed by an even polynomial ansatz. The upstream definition states: 'The integerization scale: one channel per cube face.' with the body integerization_scale : ℕ := cube_faces 3. This supplies the structural factor k used to form the integerized charge Q̃_e = k · Q_e = -6 and the subsequent polynomial Z(Q̃) = a·Q̃² + b·Q̃⁴ with minimal coefficients (1,1).
proof idea
The proof is a term-mode native_decide that directly evaluates the constant definition cube_faces 3 to the numeral 6.
why it matters
The result supplies the fixed k = 6 required by the downstream theorems Q_tilde_e_eq and Z_lepton_matches_anchor_value, which confirm that the derived Z equals the hardcoded Anchor value 1332. It implements the module's first listed step, charge integerization from cube faces, documented as a geometric structural input rather than a consequence of the T0–T8 chain. The module doc presents this choice as prerequisite for the even-polynomial construction that yields Z_ℓ = 1332.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.