Pith. sign in
module module high

IndisputableMonolith.Foundation.GaugeFromCube

show as:
view Lean formalization →

Combinatorial skeleton of gauge structure on the forced 3-cube: vertices as bit-strings, edge/face counts, and the signed-permutation automorphism group. Cited by anyone building CKM geometry, cycle dynamics, face windings, or Lie completion from RS first principles. Mostly definitions and finite counting lemmas pinned by D = 3.

claimA vertex of the $D$-cube $Q_D$ is a map $\{0,\ldots,D-1\}\to\{0,1\}$. For $D=3$: $|V(Q_3)|=8$, $|E(Q_3)|=12$, $|F(Q_3)|=6$. Automorphisms are signed permutations of the axes, of order $3!\cdot 2^3=48$; pure axis permutations number $3$.

background

Recognition Science forces spatial dimension $D=3$ (DimensionForcing, chain step T8), three fermion generations (ParticleGenerations, P-001), and $N_c=3$ color (QuarkColors, P-007). Those three facts single out the Boolean 3-cube $Q_3$ as the discrete carrier of gauge and generation structure.

This module introduces the raw geometry: a cube vertex is a function from $\mathrm{Fin},D$ into ${0,1}$; edges flip one coordinate; faces fix one coordinate and free the other two. Signed permutations (axis reorderings plus independent sign flips) form the full hyperoctahedral automorphism group; axis permutations are the unsigned $S_D$ factor.

Notation is RS-native and finite: all cardinalities are closed-form powers of two and factorials, with specialized lemmas for the $D=3$ case used downstream.

proof idea

Definition-and-counting module, not a deep proof development. Vertices are typed as maps $\mathrm{Fin},D\to{0,1}$; edge, face, and automorphism counts are elementary double-counting or group-order identities ($|B_D|=D!\cdot 2^D$). Specialized cube3_* lemmas instantiate $D=3$. Axis-permutation predicates carve out the $S_3$ factor inside the hyperoctahedral group. No analytic or measure-theoretic argument appears here.

why it matters in Recognition Science

Supplies the discrete stage on which gauge and flavor structure are built. Downstream: CycleOperator constructs the unitary 8-tick Gray-code operator on $\mathbb{C}^8$ vertex states (source of CKM); FaceWinding assigns signed face windings that seed CP violation, with each face tied to a generation pair; GaugeLieCompletionFromCube lifts the $B_3$ layer counts (3 axis perms, even sign-flip completion) toward the SM gauge Lie algebra (punchlist P0-S2-01); MassWeakBases and CKMFromCube read mass vs weak eigenbases off the same cube geometry. Cosmology importers (SakharovFromLedger, SphaleronRate) and RelativisticDOF inherit the same $Q_3$ bookkeeping. Lands between T8 ($D=3$) and the eight-tick octave on the forcing chain.

scope and limits

used by (9)

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.

declarations in this module (43)