Pith. sign in
module module high

IndisputableMonolith.Patterns.GrayCycle

show as:
view Lean formalization →

Defines one-bit adjacency, Gray covers, and Gray cycles on binary patterns, with an explicit 8-vertex Hamiltonian path on the 3-cube. Pattern and mass theorists cite it as the combinatorial source of the eight-tick octave. The module builds the D=3 objects by hand (injective gray8At schedule, cover-minimality) and records the Hamming-distance-1 edge relation used everywhere downstream.

claimOn binary patterns of length $d$, two patterns are adjacent when their Hamming distance is exactly $1$. A Gray cover of length $N$ is a walk of $N$ steps along such edges that visits every vertex of $\{0,1\}^d$; a Gray cycle is a closed Gray cover. For $d=3$, an explicit injective schedule $\mathrm{gray8At}:\mathbb{Z}/8\mathbb{Z}\to\{0,1\}^3$ realizes a Hamiltonian cycle of length $8=2^3$, and any Gray cover needs at least $8$ ticks.

background

Recognition Science forces an eight-tick fundamental period once spatial dimension is three (forcing chain T7–T8): the state space of local yes/no distinctions is the 3-cube $Q_3={0,1}^3$, and a complete recognition pass must traverse every vertex while flipping only one coordinate at a time. That combinatorial requirement is exactly a Gray code (Hamiltonian path or cycle in the hypercube graph).

This module sits in Patterns and introduces the primitive edge relation (Hamming distance one), the cover/cycle predicates that quantify over walks of a given length, and the concrete $d=3$ data: a pattern3 encoding, a map toNat3 to ${0,\ldots,7}$, and the schedule gray8At together with its injectivity. Minimality lemmas record that no shorter walk can cover all eight vertices.

Upstream is only the parent Patterns namespace; the Gray-cycle language is the first concrete graph structure the foundation layers import.

proof idea

Definition-heavy module with a short arithmetic spine for $d=3$. One-bit difference is a Prop on pairs of patterns; symmetry is immediate. GrayCover and GrayCycle package existence of an adjacent walk (open or closed) of prescribed length. The eight-tick objects are constructed by exhibiting an explicit list/path grayCycle3Path and the indexing map gray8At, then proving injectivity by finite case analysis on $\mathbb{Z}/8\mathbb{Z}$. Cover-minimality (grayCover_min_ticks, grayCover_eight_tick_min) is a counting argument: a walk of length less than $2^d$ cannot hit every vertex. No deep algebra; the work is finite enumeration plus the Hamming-edge definition.

why it matters in Recognition Science

This is the combinatorial seed of the eight-tick octave (primer T7, period $2^3$). Downstream, Foundation.CycleOperator promotes the Gray cycle on $Q_3$ to a unitary $\hat R$ on $\mathbb{C}^8$ from which the CKM matrix is read; Foundation.FaceWinding uses the same cycle to define signed face windings (CP-violation geometry); Foundation.T7CycleRealization cites the graph-shaped closed cycle to argue the realized defect is $S^1$ rather than a higher sphere. Masses.TorsionForcing projects the 8-tick Hamiltonian cycle through the Recognition Composition Law onto the $\varphi$-ladder to force generation torsions ${0,11,17}$. General-$D$ extensions (GrayCycleBRGC, GrayCycleGeneral) reuse the cover/cycle predicates defined here. Without the $d=3$ Gray cycle, the T7 realization and the cycle-operator route to mixing angles have no combinatorial 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)