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

face_pairs

show as:
view Lean formalization →

The declaration defines the number of opposite face pairs on a D-dimensional cube as exactly D. Researchers deriving three fermion generations from cube geometry in Recognition Science cite this when linking D=3 to the ledger mode structure. The definition is a direct abbreviation requiring no further reduction.

claimLet $f(D)$ denote the number of pairs of opposite faces on the $D$-cube. Then $f(D) = D$.

background

Recognition Science forces D=3 spatial dimensions via the eight-tick octave and phi fixed point (T7-T8). Module ParticleGenerations formalizes P-001: the 3-cube Q_3 has three pairs of opposite faces, each pair supplying one generation in the ledger's mode structure. This definition supplies the geometric count used by SpectralEmergence.of, which states that Q_3 simultaneously forces the gauge group SU(3)×SU(2)×U(1) and exactly three generations from the face-pair count.

proof idea

The declaration is a direct definition that sets face_pairs D to D. It functions as a one-line abbreviation for the geometric count of opposite face pairs on the D-cube.

why it matters in Recognition Science

This definition supplies the face-pair count that feeds the gauge-generation unification theorem and the gauge group certificate from the 3-cube automorphism group. It closes the P-001 step: D=3 implies exactly three generations, ruling out four or two. It connects to the framework landmark that the same Q_3 geometry unifies generations with color and weak isospin.

scope and limits

formal statement (Lean)

  31def face_pairs (D : ℕ) : ℕ := D

proof body

Definition body.

  32
  33/-- For D = 3, there are exactly 3 pairs of opposite faces. -/

used by (33)

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

… and 3 more

depends on (6)

Lean names referenced from this declaration's body.