snocBit_castSucc
The lemma shows that appending a bit via snocBit to a d-dimensional pattern recovers the original values on the embedded first d coordinates. Researchers constructing recursive Gray codes for arbitrary dimensions cite it to maintain structural consistency during the BRGC inductive step. The proof is a one-line simplification that unfolds the definition of snocBit.
claimFor a pattern $p :$ Fin $d$ $→$ Bool, bit $b :$ Bool, and index $k :$ Fin $d$, the extended pattern satisfies snocBit$(p, b)(k^↑) = p(k)$, where $k^↑$ denotes the natural embedding of $k$ into Fin $(d+1)$.
background
Patterns are defined as functions Fin $d$ $→$ Bool, serving as finite binary windows in the streams and measurement layers. The snocBit operation appends a fresh last coordinate $b$ to $p$, producing a pattern of dimension $d+1$ by placing $b$ at the final position and copying the original values elsewhere via Fin.lastCases. This module builds an axiom-free Gray cycle for general $D$ using the recursive BRGC rule: BRGC$(d+1)$ concatenates the 0-prefixed BRGC$(d)$ with the 1-prefixed reversal of BRGC$(d)$. The lemma ensures the extension step leaves the lower coordinates invariant.
proof idea
The proof is a one-line wrapper that applies simp using the definition of snocBit, which directly reduces the castSucc case to the original pattern values.
why it matters in Recognition Science
The lemma anchors the inductive step in the BRGC recursion, enabling subsequent proofs of injectivity and one-bit adjacency for the full Gray path in arbitrary dimensions. It fills the structural preservation requirement inside the module's construction of GrayCycle $d$ and GrayCover $d$ $(2^d)$. No direct tie to the T0-T8 forcing chain or phi-ladder appears here; the result remains local to pattern recursion.
scope and limits
- Does not prove injectivity or adjacency of the complete Gray path.
- Does not handle the reversal step in the BRGC recursion.
- Does not apply outside the recursive BRGC definition.
- Does not address computational cost or enumeration bounds.
formal statement (Lean)
37@[simp] lemma snocBit_castSucc {d : Nat} (p : Pattern d) (b : Bool) (k : Fin d) :
38 snocBit p b k.castSucc = p k := by
proof body
One-line wrapper that applies simp.
39 simp [snocBit]
40