Foundation Gray Code Chirality Cycle Visits All Vertices

The complete walk

A Gray code is a sequence of binary strings in which consecutive entries differ by exactly one bit. The canonical three-bit example is 000, 001, 011, 010, 110, 111, 101, 100, a path that steps along the edges of a cube and touches all eight vertices. The machine-checked theorem cycle_visits_all_vertices proves that the framework's own eight-tick walk, written as [0,1,3,2,6,7,5,4], is such a complete tour: the function mapping each step to a vertex is bijective, meaning it hits every one of the cube's eight corners exactly once and never repeats.

The proof is computational. The library defines the walk as a list of bit flips, then verifies by direct evaluation that the resulting path is a bijection. This is not a claim about the physical world; it is a statement about a finite combinatorial object. The theorem guarantees that the walk is a closed loop covering all vertices, which is a necessary structural property for the cycle to serve as a recognition cycle in the framework's account of particle generations.

In Recognition Science, the eight-step walk is the recognition cycle, a discrete sequence of events the framework uses to model how a system tracks its own states. The fact that the cycle visits all vertices means the model does not leave any state unvisited: every corner of the cube, corresponding to a distinct combination of three bits, appears exactly once in the cycle. This completeness is what lets the framework attach a flip count to each bit and compare those counts across the three axes.

The theorem does not say anything about the order of the visits beyond that it is a Gray code, and it does not assert that the walk is unique. Other Gray codes exist; this one is the canonical choice. The proof also does not establish that the cycle is chiral. Chirality, the asymmetry between clockwise and counterclockwise traversal, is a separate theorem in the same module, proved by showing that bit 0 flips four times while bits 1 and 2 each flip twice, a 4:2:2 split that breaks the cube's permutation symmetry.

What the completeness result changes is simple: it guarantees that the flip-count comparison is meaningful. If the walk skipped a vertex, the counts would be skewed by an incomplete tour. Because every vertex is visited exactly once, the asymmetry in flip counts is a property of the cycle itself, not an artifact of a partial path. That asymmetry is what the framework then links, by further theorems, to the breaking of CP symmetry and to the different treatment of particle generations.

/-- The cycle visits each vertex exactly once (bijectivity), so the total
    interaction is balanced — but the per-axis distribution is not. -/
theorem cycle_visits_all_vertices :
    Function.Bijective grayCycle3Path := grayCycle3_bijective

/-- The cycle visits each vertex exactly once (bijectivity), so the total
    interaction is balanced — but the per-axis distribution is not. -/
theorem cycle_visits_all_vertices :
    Function.Bijective grayCycle3Path := grayCycle3_bijective

/-- The cycle visits each vertex exactly once (bijectivity), so the total
    interaction is balanced — but the per-axis distribution is not. -/
theorem cycle_visits_all_vertices :
    Function.Bijective grayCycle3Path := grayCycle3_bijective

What this page does not claim

The theorem does not prove that the walk is chiral; that is a separate result in the same module. The theorem does not claim that the Gray code walk is the only possible complete cycle on the cube. The theorem does not make any statement about the physical universe; it is a purely combinatorial fact about a finite list.

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/GrayCodeChirality.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: