IndisputableMonolith.Patterns.GrayCycleGeneral
GrayCycleGeneral defines the binary-reflected Gray code path as a total function from Fin(2^d) to the d-dimensional pattern space. Researchers formalizing Hamiltonian cycles on hypercubes cite this module for its axiom-free construction. The module composes the recursive BRGC definition imported from GrayCycleBRGC into an explicit map.
claimThe BRGC path is the function $p : Fin(2^d) → (Fin d → Bool)$ given by the recursive binary-reflected Gray code construction.
background
The module operates in the Patterns domain, where Pattern d denotes maps from Fin d to Bool. Adjacency holds when two patterns differ in exactly one coordinate, and a Gray cycle is a closed Hamiltonian path of length 2^d visiting each pattern once. GrayCycleBRGC supplies the recursive definition: BRGC(0) = [0] and BRGC(d+1) = [0·BRGC(d), 1·(BRGC(d))ʳ]. GrayCodeAxioms records the classical properties of this construction pending full bitwise formalization, while GrayCode supplies the background that BRGC generates a Hamiltonian cycle on the d-dimensional hypercube Q_d.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the explicit BRGC path that realizes the Gray cycle for general dimension, feeding into the broader pattern enumeration results in the Patterns module. It completes the axiom-free construction outlined in GrayCycleBRGC and supports the existence claim exists_grayCycle among its sibling declarations.
scope and limits
- Does not verify that the path is adjacent under single-bit flips.
- Does not prove that the path forms a cycle or covers all patterns.
- Does not extend to dimensions outside powers of two.
- Does not provide computational examples for specific d values.
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