snocBit_last
plain-language theorem explainer
snocBit_last establishes that appending bit b to a d-dimensional pattern p places b exactly at the final coordinate of the resulting (d+1)-dimensional pattern. Researchers constructing recursive Gray cycles via BRGC would cite it to confirm the base placement step before proving adjacency or injectivity. The proof is a one-line simplification that unfolds the definition of snocBit.
Claim. Let $p : (Fin d) → Bool$ be a pattern and $b : Bool$. The function obtained by appending $b$ as the new highest coordinate to $p$ satisfies that its value at position $d$ equals $b$.
background
In this module patterns are maps $Fin d → Bool$. snocBit extends a pattern $p$ of dimension $d$ to dimension $d+1$ by returning $b$ on the last index and copying $p$ on the preceding indices, via the Mathlib combinator Fin.lastCases. The module builds an axiom-free Gray cycle for arbitrary dimension by the standard recursive BRGC rule: BRGC(0) is the singleton [0] and BRGC(d+1) concatenates the 0-prefixed copy of BRGC(d) with the 1-prefixed reverse of BRGC(d). Upstream results supply the last element extractor from chains (IndisputableMonolith.Chain.last and Recognition.last) and the basic Pattern type from Streams and Measurement.
proof idea
The proof is a one-line wrapper that applies the definition of snocBit. Simplification immediately reduces the left-hand side to the Fin.lastCases clause that returns the appended bit b when the index is Fin.last d.
why it matters
The lemma supplies the coordinate-access fact required for the inductive step of the BRGC path construction inside the module. It therefore supports the subsequent proofs of injectivity and one-bit adjacency that package the path as a GrayCycle d. The construction sits inside the pattern-recognition layer that feeds the eight-tick octave (T7) and the general-D spatial structure (T8) of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.