IndisputableMonolith.Foundation.FaceWinding
Defines faces of the 3-cube Q₃, directed cycle edges from the Gray walk, and the signed winding of that walk around each face boundary. Supplies the geometric primitives (CubeFace, edgeFaceSign, faceWinding) that later modules use to prove Gray-code chirality and extract a CP phase. Mostly definitional setup plus elementary counting and incidence lemmas on the cube.
claimA face of the 3-cube $Q_3$ is a pair $(a,s)$ with fixed axis $a\in\{0,1,2\}$ and side $s\in\{0,1\}$. For the directed 8-tick Gray cycle, each edge receives a sign relative to a face, and the face winding is the algebraic sum of those signed incidences around the face boundary.
background
Recognition Science forces spatial dimension $D=3$ (T8 / DimensionForcing) and works on the Boolean 3-cube $Q_3$ whose $2^3=8$ vertices are the eight-tick octave states. GrayCycle supplies an explicit Hamiltonian cycle: a closed adjacent walk of length 8 that visits every pattern exactly once.
GaugeFromCube and ParticleGenerations already extract SM gauge structure and three fermion generations from cube symmetry. This module sits one layer down: it names the six square faces of $Q_3$ and relates directed cycle edges to those faces.
A face is fixed by which coordinate is held constant and at which value (0 or 1). Free axes are the two unfixed coordinates; an edge lies on a face when its flipped bit is free and both endpoints match the face side. The edge-face sign records orientation of the directed edge relative to a chosen boundary orientation.
proof idea
Definition module with light supporting lemmas, not a deep proof chain. It introduces CubeFace, enumerates allFaces (length 6, matching the geometric face count), DirectedEdge and cycleEdges pulled from the Gray walk, then incidence helpers: flippedBit, vertexBit, edgeOnFace, freeAxes, edgeFaceSign, and finally faceWinding as the signed sum of cycle edges on the face.
Arguments are finite case analysis on Fin 3 / Bool and elementary list or Finset counting. No analytic estimates; everything is discrete cube combinatorics feeding later chirality claims.
why it matters in Recognition Science
Face winding is the geometric hinge between the eight-tick Gray cycle and CP violation. GrayCodeChirality imports it to prove the canonical 3-bit Gray walk is chiral: clockwise and counterclockwise face traversals are distinguished, which RS identifies as the origin of CP violation.
CycleOperator builds the unitary $\hat R$ on $\mathbb{C}^8$ induced by the directed cycle; oriented face data constrain how that operator acts. CPPhaseDerivation then reads $\delta_{\mathrm{CKM}}$ as a Berry phase of generation eigenstates transported around the same directed 8-tick loop.
In the forcing chain this sits after T7 (eight-tick octave) and T8 ($D=3$), and after the cube-automorphism gauge story, supplying the oriented 2-skeleton needed for a nonzero geometric phase.
scope and limits
- Does not prove chirality or CP violation; only defines faces, signs, and winding.
- Does not construct the cycle operator or CKM/Berry phase; those live downstream.
- Does not force D=3 or the Gray cycle existence; imports those modules.
- Does not treat higher-dimensional cubes or non-Gray Hamiltonian cycles.
- Does not assign physical units or numerical values to winding numbers.
used by (3)
depends on (4)
declarations in this module (22)
-
structure
CubeFace -
def
allFaces -
theorem
allFaces_length -
theorem
face_count_matches -
structure
DirectedEdge -
def
cycleEdges -
def
flippedBit -
def
vertexBit -
def
edgeOnFace -
def
freeAxes -
def
edgeFaceSign -
def
faceWinding -
def
allWindings -
def
totalChiralCharge -
def
netChiralCharge -
theorem
flippedBit_sequence -
theorem
bit_flip_counts -
theorem
face_pairs_have_three_axes -
theorem
each_edge_on_two_faces -
theorem
axis_flip_asymmetry -
def
reversedCycleEdges -
theorem
reversed_swaps_endpoints