Foundation Face Winding Face Count Matches

The face count lemma

A cube has six faces. This is true in the ordinary geometry of everyday objects, and it is also true inside the Recognition Science framework, where the cube appears as a graph called Q₃ whose eight corners are the eight ticks of a recognition cycle. The framework's ledger, a discrete record of events, walks a Hamiltonian cycle through these eight corners, visiting each exactly once. The declaration face_count_matches is a machine-checked proof that the framework's own list of faces, built by fixing one coordinate to 0 or 1, has exactly six entries, matching the classical count.

The proof is a computation. The framework defines a face by choosing one of the three axes and one side, giving six possibilities: x=0, x=1, y=0, y=1, z=0, z=1. The theorem face_count_matches states that the length of this list equals the cube face count for dimension 3, and the proof runs by native_decide, a procedure that evaluates the claim directly. This is not a deep structural result; it is a consistency check, confirming that the framework's combinatorial definition of a face agrees with the standard count of six.

The same module goes further. It defines a signed winding number for each face, measuring how the eight-tick cycle wraps around the face boundary, distinguishing clockwise from counterclockwise traversal. A nonzero winding at a face means the cycle tells forward from backward there, and the framework identifies this asymmetry as the geometric origin of CP violation. The sum of absolute windings, called totalChiralCharge, is proved nonzero, and a separate theorem shows each edge of the cube lies on exactly two faces.

In Recognition Science, the framework models the physical world through such combinatorial structures. The face count lemma is a small but necessary anchor: it certifies that the graph the framework builds on, the cube Q₃, has the face structure ordinary geometry expects. Without this check, later claims about winding numbers and chiral charge would rest on an unverified foundation. The lemma itself, however, only counts faces. It does not establish that the winding numbers are nonzero, nor that any particular face has a nonzero winding, nor anything about the physical significance of those numbers. Those are separate results in the same module, each with its own proof.

What the lemma changes for a reader is simple: the framework's cube is the ordinary cube. When the framework speaks of six faces, it means the six faces of everyday geometry, and a machine has checked that agreement. The deeper claims about chirality and CP violation stand on their own theorems, not on this counting argument.

/-- A face has 6 total faces matching cube_face_count. -/
theorem face_count_matches : allFaces.length = cube_face_count 3 := by
  native_decide

/-- The 6 faces of Q₃. -/
def allFaces : List CubeFace :=
  [ ⟨0, false⟩, ⟨0, true⟩,   -- x = 0, x = 1
    ⟨1, false⟩, ⟨1, true⟩,   -- y = 0, y = 1
    ⟨2, false⟩, ⟨2, true⟩ ]  -- z = 0, z = 1

/-- A face has 6 total faces matching cube_face_count. -/
theorem face_count_matches : allFaces.length = cube_face_count 3 := 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

The lemma does not prove any winding number is nonzero. The lemma does not establish the physical significance of chiral charge. The lemma does not connect face counts to any empirical measurement.

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: