Pith. sign in
module module high

IndisputableMonolith.Patterns.GrayCycleBRGC

show as:
view Lean formalization →

Binary reflected Gray code (BRGC) construction for the hypercube of boolean patterns. Defines snoc-bit append and the recursive BRGC path of length 2^d, with injectivity and single-bit adjacency lemmas. Feeds the general-dimension Gray cycle module. Arguments are inductive Fin casting and bit-append comparisons.

claimFor each dimension $d$, the BRGC path $\mathrm{brgcPath}_d:\mathrm{Fin}(2^d)\to(\mathrm{Fin}\,d\to\mathrm{Bool})$ enumerates all patterns so consecutive codes differ in one coordinate. The map $\mathrm{snocBit}$ appends a fresh last bit $b$ to a pattern in dimension $d$, yielding one in dimension $d+1$.

background

In Recognition Science patterns, a state is a boolean vector $\mathrm{Pattern},d:=\mathrm{Fin},d\to\mathrm{Bool}$. The upstream GrayCycle module upgrades counting facts to an explicit adjacent cycle: adjacency means differing in exactly one coordinate, and a cycle is a closed walk of length $2^d$ visiting every pattern once.

This module supplies the classical binary reflected Gray code realization of that walk. The key local operation is snoc-bit: append a fresh last coordinate $b$ to a $d$-pattern to obtain a $(d+1)$-pattern. The BRGC path is built by reflecting and stacking lower-dimensional paths with a flipped high bit, matching the standard formula $\mathrm{gray}(n)=n\oplus(n\gg 1)$ in spirit.

Sibling lemmas handle Fin casting across $2^{d}+2^{d}=2^{d+1}$, injectivity of the path, and the one-bit difference rules for same-bit versus flipped-bit snoc.

proof idea

Definition-heavy module with inductive lemmas. snocBit is the coordinate-append map; cast lemmas relate Fin indices under $2^{d+1}=2^d+2^d$. brgcPath is defined recursively by reflecting the lower path and snoc-ing 0 then 1 (or the reverse). Injectivity of brgcPath proceeds by case analysis on the high bit and induction. One-bit adjacency is proved by comparing snocBit on equal versus flipped last bits, plus a step lemma that consecutive BRGC indices differ in exactly one coordinate.

why it matters in Recognition Science

Workstream A needs an explicit adjacent Gray cover for every dimension so the eight-tick octave and higher hypercube schedules sit on a Hamiltonian cycle. This module is the concrete BRGC engine; GrayCycleGeneral imports it to expose Patterns.GrayCover d (2^d) and Patterns.GrayCycle d via the standard XOR formula. Without injectivity and the one-bit step lemmas here, the general-d cycle would remain a counting existence claim rather than a constructive adjacent walk. Ties to the T7 eight-tick structure only indirectly: the d=3 case is the octave skeleton once the cycle is in hand.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)