IndisputableMonolith.Patterns.GrayCycleGeneral
General-d binary-reflected Gray code (BRGC) path from indices Fin(2^d) into Pattern d, with injectivity, single-bit steps, and a closed Hamiltonian cycle covering the hypercube. Anyone citing an explicit adjacent Gray cycle for arbitrary dimension (beyond the fixed eight-tick case) uses this module. The argument builds the path from the recursive BRGC construction, then verifies adjacency, injectivity, and cycle closure with bit lemmas.
claimFor each dimension $d$, the binary-reflected Gray code supplies a map $\mathrm{brgcPath}_d : \mathrm{Fin}(2^d) \to \mathrm{Pattern}\, d$ (where $\mathrm{Pattern}\, d = \mathrm{Fin}\, d \to \mathrm{Bool}$) that is injective, changes exactly one coordinate at successive indices, and closes under the wrap-around step, yielding a Hamiltonian cycle and a full cover of the $d$-cube. In particular there exists a Gray cycle on $\mathrm{Pattern}\, d$ for every $d$.
background
Recognition patterns live on the hypercube: a state is a bit-vector $\mathrm{Pattern}, d := \mathrm{Fin}, d \to \mathrm{Bool}$, and two states are adjacent when they differ in exactly one coordinate. A Gray cycle is a length-$2^d$ closed walk that visits every pattern once (a Hamiltonian cycle on $Q_d$).
The binary-reflected Gray code is the classical recursive construction: $\mathrm{BRGC}(0)=[0]$ and $\mathrm{BRGC}(d+1)=[0\cdot\mathrm{BRGC}(d),, 1\cdot(\mathrm{BRGC}(d))^r]$. Upstream modules supply the BRGC combinatorics (GrayCode), classical properties sometimes held as axioms (GrayCodeAxioms), the abstract adjacent-cycle interface (GrayCycle), and an axiom-free recursive BRGC cycle (GrayCycleBRGC).
This module packages the BRGC path as an explicit map $\mathrm{Fin}(2^d)\to\mathrm{Pattern}, d$, together with bit-level support (all-ones masks, testBit bounds) needed to prove single-bit steps and wrap-around adjacency in general $d$.
proof idea
Definition-first module, not a single theorem. It introduces brgcPath as the BRGC enumeration into patterns, plus helpers (allOnes, testBit lemmas) that control which bits are live below dimension $d$.
Injectivity of the path and one-bit difference on successive steps are proved from the BRGC bit structure and those mask lemmas. Wrap-around adjacency (last to first) is a separate one-bit fact. Those pieces assemble into brgcGrayCycle and brgcGrayCover, and finally exists_grayCycle packages existence of a Gray cycle for every $d$.
why it matters in Recognition Science
In the Recognition framework the discrete tick structure is an octave on the hypercube: T7 forces period $2^3$ (eight-tick) once $D=3$ spatial dimensions are fixed (T8). A dimension-general, adjacency-true Gray cycle is the combinatorial backbone that specializes to that eight-tick cover and justifies pattern enumeration without double-counting or non-local jumps.
No downstream edges are recorded yet on this page; within the module the existence theorem exists_grayCycle and the concrete brgcGrayCycle / brgcGrayCover objects are the export surface for any later forcing or counting argument that needs a Hamiltonian cycle on $\mathrm{Pattern}, d$. Relative to GrayCycleBRGC, this file emphasizes the path-as-function view and the bit lemmas that make general-$d$ adjacency checkable in Lean.
scope and limits
- Does not fix d=3 or prove the eight-tick octave; that is a specialization elsewhere (T7).
- Does not derive physics constants, mass rungs, or the J-cost functional equation.
- Does not claim uniqueness of the Gray cycle; only existence via BRGC.
- Does not replace GrayCodeAxioms for every classical identity; only what the path proofs need.
- Does not address continuous limits or non-hypercube state spaces.
depends on (5)
declarations in this module (15)
-
def
brgcPath -
def
allOnes -
lemma
allOnes_succ_eq_bit -
lemma
allOnes_testBit_lt -
lemma
allOnes_testBit_eq_false_at -
theorem
brgc_wrap_oneBitDiff -
lemma
natToGray_testBit_false_of_ge -
theorem
brgcPath_injective -
lemma
brgc_oneBit_step -
def
brgcGrayCycle -
def
brgcGrayCover -
theorem
exists_grayCycle -
theorem
exists_grayCover -
theorem
exists_grayCycle_of_le64 -
theorem
exists_grayCover_of_le64