IndisputableMonolith.Patterns.GrayCycleGeneral
The GrayCycleGeneral module defines the binary-reflected Gray code path as a map from Fin(2^d) to the d-dimensional pattern space. Researchers formalizing Hamiltonian cycles on hypercubes within Recognition Science cite it for the explicit general-d construction. The module assembles this map from the recursive BRGC definition imported from GrayCycleBRGC and sibling modules.
claimThe binary-reflected Gray code path is the function $f : [2^d] → ( [d] → {0,1} )$ that enumerates every d-bit pattern exactly once according to the standard reflection recursion.
background
The module resides in the Patterns domain. Pattern d is the set of functions Fin d → Bool, the vertices of the d-dimensional hypercube. Two patterns are adjacent when they differ in exactly one coordinate; a Gray cycle is a closed walk of length 2^d that visits every pattern once. GrayCycleBRGC supplies the axiom-free recursive construction: BRGC(0) = [0] and BRGC(d+1) = [0·BRGC(d), 1·(BRGC(d)) reversed]. GrayCodeAxioms records classical properties as pending axioms while GrayCycle upgrades counting facts to the adjacent-cycle notion.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the concrete BRGC path that realizes the Gray cycle for arbitrary d. It feeds the sibling declarations brgcGrayCycle and exists_grayCycle inside the same module, closing the axiom-free general-d construction required by the GrayCycle hierarchy. The path directly implements the Hamiltonian cycle on the hypercube that later pattern-recognition results rely upon.
scope and limits
- Does not prove single-bit adjacency between consecutive path elements.
- Does not establish that the path returns to its starting pattern.
- Does not link the construction to the J-cost or phi-ladder of the core framework.
- Does not treat infinite-dimensional or continuous pattern 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