cast_add_one
plain-language theorem explainer
The lemma establishes that successor on Fin n commutes with casting to Fin m whenever n equals m (both nonzero). It is invoked inside the recursive step of the BRGC path to maintain one-bit adjacency when indices wrap across the midpoint. The proof is a direct substitution of the equality hypothesis followed by simplification.
Claim. Let $n,m$ be nonzero natural numbers with $n=m$. For $i$ in the finite set of size $n$, the successor of $i$ cast to the finite set of size $m$ equals the cast of $i$ followed by successor: $(i+1).cast h = (i.cast h)+1$.
background
The GrayCycleBRGC module constructs an axiom-free Gray cycle for arbitrary dimension $d$ by recursing on the binary reflected Gray code: BRGC(0) is the single zero pattern and BRGC(d+1) concatenates the zero-prefixed BRGC(d) with the one-prefixed reverse of BRGC(d). The path is realized as a map Fin(2^d) to Pattern d using snocBit and Fin.append, with the size-doubling equality 2^{d+1}=2^d+2^d supplied by twoPow_succ_eq_add. The cast_add_one helper appears when the recursive definition must add one to an index that has already been cast across equal-sized Fin types.
proof idea
Term-mode one-liner: substitute the hypothesis that n equals m, then invoke simp to reduce the cast and successor expressions on Fin.
why it matters
The lemma is used by brgc_oneBit_step, which proves that consecutive elements of brgcPath differ by exactly one bit (including the cycle-closing step). This supplies the adjacency half of the packaged GrayCycle d / GrayCover d (2^d) theorems, giving an explicit recursive construction that avoids the bitwise gray(n) = n XOR (n >> 1) formula. Within the Recognition framework it supports the pattern-level realization of the eight-tick octave (T7) by furnishing a concrete, dimension-independent cycle whose one-bit transitions align with the phi-ladder mass formula and the D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.