pith. sign in
module module high

IndisputableMonolith.Patterns.GrayCycleBRGC

show as:
view Lean formalization →

The GrayCycleBRGC module supplies the binary reflected Gray code construction that realizes an explicit adjacent Hamiltonian cycle on the d-dimensional hypercube of patterns. Researchers building concrete Gray covers or cycles in the Patterns framework cite it to obtain a dimension-independent explicit example. The module defines the brgcPath function via the standard XOR-shift formula and proves its injectivity together with the single-bit transition property between successive steps.

claimThe BRGC path in dimension $d$ is the sequence $k=0,1,2^d-1$ mapped to the pattern whose coordinates are the bits of $k$ XOR $(k$ right-shift $1)$, yielding an adjacent cycle of length $2^d$ on the hypercube.

background

The Patterns module defines Pattern d as the set of functions Fin d → Bool. The GrayCycle module upgrades this to an adjacent cycle: a closed walk of length 2^d that visits every pattern exactly once, with each consecutive pair differing in precisely one coordinate. The supplied upstream GrayCycle doc states the state space, adjacency, and cycle requirements explicitly. GrayCycleBRGC specializes this abstract notion by importing the standard BRGC formula gray(n) = n XOR (n >>> 1) and the supporting bit-manipulation lemmas.

proof idea

This is a definition module that introduces brgcPath together with auxiliary operations such as snocBit and cast_add_one. It contains targeted lemmas (brgcPath_injective, oneBitDiff_snocBit_same, oneBitDiff_snocBit_flip) that establish injectivity and the single-bit difference property; the overall structure is definitional with short algebraic verifications rather than long tactic scripts.

why it matters in Recognition Science

GrayCycleBRGC is imported by GrayCycleGeneral, which lifts the construction to a full GrayCycle d for arbitrary dimension via the BRGC formula. It therefore supplies the concrete adjacent cycle required for the workstream A generalization described in the downstream doc-comment. The module closes the explicit-construction gap between the abstract GrayCycle interface and the standard binary-reflected code used throughout the Patterns domain.

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)