Foundation Face Winding

Face winding and handedness

A cube has six square faces, and a closed path along its edges can loop around each face in either of two directions. In the Recognition Science framework, the eight-step cycle that represents a full recognition tick traces a specific Hamiltonian cycle on the cube Q₃, meaning a closed loop that visits all eight vertices exactly once. The winding number of this cycle around a face is the net signed count of how many times the loop goes around that face's boundary, with clockwise and counterclockwise traversals canceling. The framework's module FaceWinding defines this winding for every face and proves that the total, summed over all six faces, is nonzero. That nonzero total is the geometric origin of CP violation in the framework: a measurable difference between how the cycle behaves and how its mirror image behaves.

Classically, a winding number is a topological invariant that counts how many times a curve wraps around a point or region. Here the faces are indexed by fixing one coordinate of the cube to 0 or 1, giving the six faces x=0, x=1, y=0, y=1, z=0, z=1. Each edge of the cycle is assigned a sign depending on whether it traverses a face boundary in the positive or negative direction, and the winding for a face is the sum of those signs over the eight steps. The module proves elementary facts about this setup: there are exactly six faces, each edge lies on exactly two faces, and the bit-flip sequence that generates the cycle flips the x-bit four times, the y-bit twice, and the z-bit twice. That asymmetry in how often each axis is flipped is what makes the cycle prefer one handedness over the other.

In Recognition Science, the cube's faces correspond to generation pairs of particles, and the winding measures how the eight-tick cycle wraps around each face. A nonzero winding means the cycle distinguishes forward from backward at that face, which the framework reads as the geometric seed of CP violation, the observed particle physics asymmetry where certain processes differ under charge conjugation and parity reversal. The module does not derive the full CP violation; it establishes the geometric foundation by proving the total chiral charge is nonzero and by providing the explicit enumeration of faces, edges, and signed traversals. The machine-checked library of formal theorems verifies each of these claims by computation.

What the module changes is the status of handedness in the framework: it is not an assumption but a proved consequence of the recognition cycle's structure. The cycle flips axes unevenly, and that unevenness forces a nonzero total winding. A reader can now see that the framework's account of CP violation rests on a concrete, checkable property of a path on a cube, rather than on an unexplained asymmetry.

/-- The winding number of the Gray code cycle around a face:
    the sum of signed edge contributions over all 8 cycle steps. -/
def faceWinding (f : CubeFace) : ℤ :=
  ∑ i : Fin 8, edgeFaceSign i f

/-- The total chiral charge: sum of absolute face windings.
    Measures the total asymmetry of the cycle's interaction with face boundaries.
    Nonzero means the cycle is chiral. -/
def totalChiralCharge : ℤ :=
  ∑ i : Fin 8, ∑ f ∈ allFaces.toFinset, (edgeFaceSign i f).natAbs

/-- The net chiral charge: signed sum of face windings.
    This can be zero even when individual face windings are nonzero
    (opposite faces may have opposite windings). -/
def netChiralCharge : ℤ :=
  allFaces.foldl (fun acc f => acc + faceWinding f) 0

/-- Bit 0 flips 4 times, bit 1 flips 2 times, bit 2 flips 2 times.
    This asymmetry (4 vs 2 vs 2) is the combinatorial origin of chirality. -/
theorem bit_flip_counts :
    (List.ofFn flippedBit).count 0 = 4 ∧
    (List.ofFn flippedBit).count 1 = 2 ∧
    (List.ofFn flippedBit).count 2 = 2 := by native_decide

/-- Each edge of the cycle is incident to exactly 2 of the 6 faces
    (the edge lies on exactly 2 faces of the cube). -/
theorem each_edge_on_two_faces (step : Fin 8) :
    (allFaces.filter (fun f => edgeOnFace step f)).length = 2 := by
  fin_cases step <;> native_decide

What this page does not claim

This answer does not claim the module derives the magnitude of CP violation, only its geometric seed. This answer does not claim the winding number is a conventional topological invariant on a continuous surface; it is defined on the discrete cube's edges. This answer does not claim the framework explains why the cycle flips axes unevenly; that unevenness is part of the cycle's definition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/FaceWinding.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: