natAdd_eq_addNat
The lemma equates the two embeddings of a Fin T index k into Fin(T+T): Fin.natAdd T k coincides with k.addNat T. Researchers building recursive BRGC Gray cycles cite it to keep path indices consistent when appending left and right halves. The proof is a one-line wrapper that applies Fin.ext and simplifies with associativity and commutativity of addition.
claimFor any natural number $T$ and $k$ in Fin $T$, the embedding of $k$ into Fin$(T+T)$ via natAdd equals the result of adding $T$ to $k$ via addNat.
background
This lemma sits inside the axiom-free recursive BRGC construction of Gray cycles. The module defines brgcPath d recursively by splitting the range 2^{d+1} into two copies of T=2^d, casting the index via hTT : 2^{d+1}=T+T, then appending snocBit-wrapped copies of the lower-dimensional path. The equality ensures the cast index behaves identically under the two addition embeddings used in Fin.append. It draws on add_assoc and add_comm from ArithmeticFromLogic, which establish the corresponding properties for LogicNat, together with the period definitions T from Breath1024 and Gap45.
proof idea
The proof is a term-mode one-liner: apply Fin.ext reduces the Fin equality to an equality of underlying naturals; simp then rewrites the definitions of Fin.natAdd and addNat together with Nat.add_assoc, Nat.add_left_comm and Nat.add_comm to obtain the common value T+k.
why it matters in Recognition Science
The lemma is invoked inside brgc_oneBit_step, the theorem that consecutive BRGC path elements differ by exactly one bit (including wrap-around). It therefore supplies a technical step in the packaged GrayCycle d and GrayCover d (2^d) results. Within Recognition Science it supports the discrete path constructions that feed the eight-tick octave and the derivation of D=3 spatial dimensions.
scope and limits
- Does not apply when T is not a power of two.
- Does not prove injectivity or adjacency of the full path.
- Does not extend to infinite or non-finite index sets.
- Does not address bit-flip counts beyond the equality itself.
formal statement (Lean)
159private lemma natAdd_eq_addNat {T : Nat} (k : Fin T) :
160 (Fin.natAdd T k : Fin (T + T)) = k.addNat T := by
proof body
Term-mode proof.
161 apply Fin.ext
162 -- both sides represent the same natural number `T + k`
163 simp [Fin.natAdd, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
164