rev_add_one_eq
plain-language theorem explainer
The lemma establishes that reversing a Fin index after incrementing it and then adding one recovers the reverse of the original index, whenever the increment stays strictly below n. Researchers constructing recursive BRGC paths for Gray cycles in arbitrary dimension cite this identity when proving one-bit adjacency along the cycle. The proof reduces the Fin equality to a Nat identity via Fin.ext and chains associativity, commutativity, and right cancellation on the subtracted expressions.
Claim. Let $n$ be a positive integer and $i$ an element of Fin $n$ such that $i+1<n$. Then rev$(i+1)+1=$rev$(i)$, where rev denotes the reversal map on Fin $n$ given by rev$(k)=n-1-k$.
background
The declaration sits inside the module that builds an axiom-free Gray cycle for general dimension via the standard BRGC recursion: BRGC(0)=[0] and BRGC(d+1)=[0·BRGC(d), 1·(BRGC(d)) reversed]. The reversal map on Fin n implements the recursive flip that produces the reflected half of the path. The local theoretical setting is therefore purely combinatorial and independent of the bitwise Gray-code formula or any Recognition Science axioms.
proof idea
The proof applies classical, then Fin.ext, to reduce to a natural-number equality. It first records the valuation of i+1, derives the two inequalities i.val+1≤n and i.val+2≤n, and proves the auxiliary identity (n-(i.val+2))+1 = n-(i.val+1) by a calc that invokes add_assoc and add_comm from ArithmeticFromLogic together with add_right_cancel. It then computes the valuations of rev(i+1) and rev(i) directly from the definition of Fin.rev, assembles the left- and right-hand sides via val_add_one_of_lt', and closes the calc with the auxiliary identity.
why it matters
The lemma is invoked by brgc_oneBit_step, the theorem that shows consecutive elements of the BRGC path differ by exactly one bit. It therefore supplies a technical step required to package the recursive construction as a GrayCycle d and a GrayCover d (2^d). In the Recognition Science setting the construction supplies an axiom-free model of cyclic adjacency that can be used for pattern recognition at any spatial dimension, including the D=3 case forced by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.