Foundation Face Winding All Faces Length

The cube's six faces

A cube, in the ordinary geometry of three-dimensional space, has six faces. You can see them without counting: top and bottom, front and back, left and right. The declaration allFaces_length is a formal statement inside the Recognition Science framework's machine-checked library of formal theorems that certifies exactly this fact for a specific mathematical object: the list of all faces of the three-dimensional cube Q₃ has length 6.

The object in question is the Hamiltonian cycle, a closed path that visits each of the cube's eight vertices exactly once before returning to its start. The framework models an eight-tick recognition cycle as such a path. The declaration allFaces is a definition that lists the six faces by fixing one coordinate to a constant value: x=0, x=1, y=0, y=1, z=0, z=1. The theorem allFaces_length then verifies, by a computational decision procedure, that this list indeed contains six entries.

This count is a small but load-bearing piece of a larger structure. The faces of the cube correspond to generation pairs in the framework, and the winding number of the Hamiltonian cycle around each face measures an asymmetry between clockwise and counterclockwise traversal. A nonzero winding at a face means the cycle distinguishes forward from backward there, which the framework identifies as the geometric origin of CP violation. The fact that there are exactly six faces, each with four boundary edges, is what allows the framework to speak of three axes and their paired faces.

What allFaces_length does not claim is just as precise. It does not assert that the cube is the only object with six faces, nor does it say anything about the physical existence of three-dimensional space. It is a statement about a list defined in the library: that list has six elements. The theorem does not prove that the winding numbers are nonzero, nor that CP violation occurs; those are separate claims in the same module. It also does not establish that the recognition cycle is the correct description of nature. The declaration is a certified count, nothing more and nothing less.

In Recognition Science, this certified count is a foundation stone. The framework proves that an eight-tick cycle forces three spatial dimensions, and the six faces of the resulting cube are the stage on which the cycle's asymmetry is measured. The theorem allFaces_length ensures that this stage has the right number of sides before any physical claim is built on it.

theorem allFaces_length : allFaces.length = 6 := by native_decide

theorem allFaces_length : allFaces.length = 6 := by native_decide

/-- 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

What this page does not claim

The theorem does not assert that the cube is the only object with six faces. The theorem does not prove that the winding numbers are nonzero or that CP violation occurs. The theorem does not establish that the recognition cycle is the correct description of nature.

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: