IndisputableMonolith.Patterns.GrayCycleGeneral
The module defines the BRGC path as the explicit map from Fin(2^d) into the space of d-bit patterns. Researchers constructing Hamiltonian cycles on hypercubes cite it for the general-dimensional case. The module assembles the recursive BRGC definition from its imports into a single path function.
claimThe binary-reflected Gray code path is the function $brgcPath : \Fin(2^d) \to (\Fin d \to \Bool)$.
background
Pattern d is the state space of d-bit strings, realized as functions Fin d to Bool. Adjacency holds when two patterns differ in exactly one coordinate. GrayCode supplies the recursive BRGC construction: BRGC(0) equals the singleton list containing 0, with the standard doubling step that prepends a bit and reverses the second half. GrayCycle upgrades counting facts to an explicit adjacent cycle of length 2^d that visits every pattern once. GrayCycleBRGC gives the axiom-free recursive realization of such a cycle for arbitrary d.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the general BRGC path that feeds explicit cycle constructions used by GrayCycle and GrayCycleBRGC. It realizes the Hamiltonian path on the hypercube Q_d without axioms, supporting downstream coverage and enumeration results in the Patterns domain.
scope and limits
- Does not prove cycle closure or adjacency properties.
- Does not introduce new axioms or hypotheses.
- Does not specialize the construction to fixed d.
- Does not contain usage sites inside the module itself.
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