IndisputableMonolith.Patterns.GrayCycleBRGC
This module implements the Binary Reflected Gray Code construction to realize explicit Hamiltonian cycles on the d-dimensional hypercube inside the Patterns framework. It supplies the path via recursive bit-append helpers and proves the required adjacency and coverage properties. Researchers instantiating GrayCycle d for discrete modeling or hypercube traversals cite it as the concrete BRGC realization. The module proceeds by defining snocBit-style appends and establishing injectivity plus single-bit difference lemmas.
claimThe BRGC path is the sequence of all $2^d$ vertices in $\{0,1\}^d$ generated by $g(n)=n\oplus(n\gg1)$, forming a closed walk in which consecutive patterns differ in exactly one coordinate and every pattern appears once.
background
The Patterns module defines Pattern d as the set of functions Fin d → Bool, i.e., the vertices of the d-dimensional hypercube. GrayCycle (the immediate upstream module) upgrades the earlier counting facts to an explicit adjacent cycle: a length-$2^d$ closed walk visiting every pattern exactly once, with each step flipping precisely one coordinate. The present module supplies the standard BRGC formula as the concrete witness for that cycle notion.
proof idea
This is a definition module whose core is the recursive construction of brgcPath together with supporting lemmas (snocBit, brgcPath_injective, oneBitDiff_snocBit_*, brgc_oneBit_step). The lemmas establish that appending a final bit preserves adjacency and that the resulting list is injective and covers the full hypercube.
why it matters in Recognition Science
The module directly feeds GrayCycleGeneral, which lifts the BRGC construction to an arbitrary-dimension GrayCover d (2^d) and GrayCycle d. It therefore supplies the explicit adjacent-cycle witness required by the Patterns layer of the Recognition framework.
scope and limits
- Does not treat Gray codes over alphabets larger than two symbols.
- Does not address non-Hamiltonian or non-closed walks.
- Does not supply runtime or gate-complexity bounds for path generation.
- Does not generalize the construction beyond the standard BRGC reflection rule.
used by (1)
depends on (2)
declarations in this module (14)
-
def
snocBit -
lemma
snocBit_castSucc -
lemma
snocBit_last -
lemma
twoPow_succ_eq_add -
def
brgcPath -
lemma
cast_add_one -
theorem
brgcPath_injective -
theorem
oneBitDiff_snocBit_same -
theorem
oneBitDiff_snocBit_flip -
lemma
natAdd_eq_addNat -
lemma
rev_add_one_eq -
theorem
brgc_oneBit_step -
def
brgcGrayCycle -
def
brgcGrayCover