Pith. sign in
module module high

IndisputableMonolith.Patterns.GrayCycle

show as:
view Lean formalization →

Defines one-bit adjacency on binary patterns and the Gray-cycle / Gray-cover structures that realize Hamiltonian tours of the hypercube. Specializes to the unique (up to symmetry) 8-tick cover of the 3-cube Q₃, with injectivity and minimality facts. Foundation and mass modules cite it as the combinatorial source of the eight-tick octave and the cycle operator on ℂ⁸.

claimOn binary patterns of length $d$, two vertices are adjacent when their Hamming distance is $1$. A Gray cover of length $T$ is a walk of $T$ steps that visits every vertex of the $d$-cube using only such edges; a Gray cycle is a closed cover. For $d=3$, the module supplies an explicit $8$-tick Gray cycle on $Q_3$ (period $2^3$), proves the map is injective on $\mathbb{Z}/8\mathbb{Z}$, and records the minimality bound $T\ge 8$.

background

Recognition Science forces an eight-tick octave (forcing chain T7): the shortest closed recognition schedule in $D=3$ has period $2^3=8$. Combinatorially this is a Hamiltonian cycle on the 3-cube graph $Q_3$, whose edges flip exactly one coordinate.

This module sits in Patterns and introduces the elementary predicates: OneBitDiff (Hamming distance one), GrayCover / GrayCycle (adjacent covers and cycles of prescribed length), and the concrete $d=3$ objects pattern3, gray8At, and grayCycle3Path. The parent Patterns import supplies the ambient pattern type; Mathlib supplies finite arithmetic and injectivity tooling.

Downstream foundation work treats the same cycle as a unitary on $\mathbb{C}^8$ and as the graph shape whose defect is a circle $S^1$, so the definitions here are the discrete skeleton those modules import.

proof idea

Definition-heavy module with short supporting lemmas rather than a single deep theorem. One-bit difference is the Hamming-distance-1 relation; symmetry is immediate. Gray cover/cycle are structure packages (path plus adjacency and coverage obligations). The $d=3$ path is given explicitly by a standard binary-reflected Gray enumeration gray8At; injectivity of the time-to-vertex map and the lower bound that any cover needs at least eight ticks are proved by finite case analysis / pigeonhole on the eight vertices of $Q_3$. General-$D$ recursive BRGC constructions live in sibling modules that import this interface.

why it matters in Recognition Science

This is the combinatorial home of T7's eight-tick octave on $Q_3$. Foundation.CycleOperator builds the unitary $\hat R$ on $\mathbb{C}^8$ "induced by the 8-tick Gray code cycle on $Q_3$" from which the CKM matrix is said to emerge. Foundation.FaceWinding uses the same Hamiltonian cycle to define signed face windings (generation pairs, CP-violation geometry). Foundation.T7CycleRealization strengthens the T7/T8 route: the closed cycle is graph-shaped, so realized defect is $S^1$ rather than higher spheres. Masses.TorsionForcing derives generation torsions ${0,11,17}$ as the unique values compatible with the 8-tick cycle projected through RCL onto the $\varphi$-ladder. Generalizations GrayCycleBRGC and GrayCycleGeneral reuse the cover/cycle API for arbitrary $d$. Without the $d=3$ Gray skeleton, the cycle operator, face windings, and torsion forcing have no discrete carrier.

scope and limits

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)