pith. machine review for the scientific record. sign in
def definition def or abbrev high

integerization_scale

show as:
view Lean formalization →

The integerization_scale definition sets the charge integerization factor k to the face count of the 3-cube, fixing k at 6 to supply one symmetry channel per face for quantizing lepton charges. Researchers deriving the lepton index Z_ℓ via even polynomials on integerized charges would cite this scale as the initial geometric input. It is realized as a direct one-line application of the cube_faces function at dimension 3.

claimLet $k = F(3)$ where $F(D)$ denotes the number of faces of the $D$-cube. The integerization scale is defined by $k := 6$.

background

In the Z-map derivation, charge integerization begins with the scale k set to the face count of the 3-cube Q₃. Each face supplies one independent 2D symmetry channel for quantizing the electron charge, producing the integerized value Q̃_e = k · Q_e = -6. The cube_faces function appears in three upstream modules, each defining it as 2D for D = 3 and thereby returning 6 faces for the cube.

proof idea

This definition is a one-line wrapper that applies the cube_faces function directly to the argument 3.

why it matters in Recognition Science

This definition supplies the integerization scale k = 6 that feeds the integerization_scale_eq theorem and the Q_tilde_e definition, enabling the even polynomial ansatz to reach Z_ℓ = 1332. It implements the first structural step of the Z-map derivation in the module documentation, grounding the lepton charge index in 3-cube geometry rather than the T0-T8 forcing chain.

scope and limits

formal statement (Lean)

  40def integerization_scale : ℕ := cube_faces 3

proof body

Definition body.

  41

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.