IndisputableMonolith.Patterns.GrayCycleGeneral
The module defines the binary-reflected Gray code path as a map from Fin(2^d) to the space of d-bit patterns. Researchers formalizing Hamiltonian cycles on hypercubes or combinatorial layers in Recognition Science cite it for the explicit construction. It assembles the standard recursive BRGC definition into a closed cycle on the hypercube without axioms.
claimLet $P_d$ be the set of patterns (functions Fin $d$ to Bool). The BRGC path is the function brgcPath$_d$: Fin$(2^d) → P_d$ given by the recursion BRGC(0) = [0], BRGC($d+1$) = [0·BRGC($d$), 1·(BRGC($d$)) reversed].
background
This module sits in the Patterns domain. Patterns are boolean assignments to d coordinates, with adjacency when two patterns differ in exactly one coordinate. The GrayCycle import upgrades counting facts to an explicit adjacent Hamiltonian cycle of length 2^d that visits every pattern once and returns to the start.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the explicit BRGC path realizing the Gray cycle for arbitrary d. It feeds the combinatorial infrastructure for pattern recognition results and supports the forcing chain by providing an axiom-free cycle construction on the hypercube.
scope and limits
- Does not prove adjacency or closure properties; these are imported from GrayCycleBRGC.
- Does not treat non-power-of-two state spaces or non-hypercube graphs.
- Does not compute explicit bit-level representations beyond the path function.
- Does not connect to physical constants, mass ladders, or forcing steps T0-T8.
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