snocBit
plain-language theorem explainer
The snocBit definition appends a single boolean coordinate to the end of a d-dimensional pattern, producing a pattern of dimension d+1. Researchers constructing recursive binary reflected Gray codes cite this helper when extending paths from dimension d to d+1 in the BRGC recursion. It is realized as a one-line functional definition that routes the new bit to the final Fin index via Fin.lastCases while copying the original pattern on the initial coordinates.
Claim. Let $p :$ Fin $d$ $→$ Bool be a pattern and $b$ a boolean. Then snocBit$(p,b) :$ Fin$(d+1)$ $→$ Bool is defined by snocBit$(p,b)(j) = b$ when $j$ is the last element of Fin$(d+1)$, and $p(k)$ when $j = k$.castSucc for $k :$ Fin $d$.
background
In the GrayCycleBRGC module, a Pattern $d$ is a finite binary string of length $d$, represented as the function type Fin $d$ $→$ Bool. The module builds an axiom-free Gray cycle for arbitrary dimension via the standard BRGC recursion: the path for dimension 0 is the single zero pattern, and the path for dimension $d+1$ is formed by prefixing 0 to the path for $d$ and 1 to its reverse. Upstream results supply the basic Pattern type from IndisputableMonolith.Measurement.Pattern (finite windows of length $n$), IndisputableMonolith.Patterns.Pattern, IndisputableMonolith.Streams.Pattern, and IndisputableMonolith.Streams.Blocks.Pattern, each defining a finite window as Fin $n$ $→$ Bool.
proof idea
This is a one-line wrapper that applies Fin.lastCases to insert the appended bit $b$ at the final coordinate while delegating all preceding coordinates to the original pattern $p$.
why it matters
snocBit supplies the core primitive for the recursive step inside brgcPath, which defines the BRGC path for dimension $d+1$ from the path in dimension $d$. It is invoked directly in brgcPath_injective to prove injectivity, in oneBitDiff_snocBit_same to preserve one-bit differences under identical appended bits, and in oneBitDiff_snocBit_flip to establish the flip case. These feed the packaged GrayCycle $d$ and GrayCover $d$ ($2^d$) results that realize the module's axiom-free construction of Hamiltonian paths on the hypercube with one-bit adjacency including wrap-around.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.