allOnes_succ_eq_bit
plain-language theorem explainer
The lemma equates the all-ones integer of length t+1 with the binary number formed by setting the least-significant bit to 1 and shifting the all-ones integer of length t left by one position. Internal proofs of one-bit adjacency in the bounded BRGC Gray-cycle construction cite this step when handling the wrap-around from the final codeword to zero. The argument proceeds by adding one to both sides, reducing each to 2^(t+1) via the definition and algebraic distribution, then invoking right cancellation.
Claim. For every natural number $t$, the integer $2^{t+1}-1$ equals $2(2^t-1)+1$.
background
The declaration sits inside Patterns.GrayCycleGeneral, the bounded-BRGC development of Gray covers for general dimension d. There allOnes d is defined as $2^d-1$, the integer whose binary representation consists of d ones. The module builds a GrayCycle d object from the standard BRGC formula under the GrayCodeFacts axiom package when d ≤ 64, while the axiom-free recursive version lives in GrayCycleBRGC.
proof idea
The tactic proof first shows allOnes (t+1) + 1 = 2^(t+1) by unfolding the definition and cancelling the subtracted 1. It then expands Nat.bit true (allOnes t) + 1 through a calc block that distributes multiplication, applies mul_sub_left_distrib, and reduces via pow_succ and add_comm to reach the same power. Equality of the two augmented expressions is obtained by transitivity, after which add_right_cancel (imported from ArithmeticFromLogic) yields the desired identity.
why it matters
The result is invoked by allOnes_testBit_lt and brgc_wrap_oneBitDiff to certify the single-bit flip between the last and first codewords of the BRGC path. It therefore supplies the bitwise representation needed for the wrap-around adjacency claim inside the general-d GrayCycle construction. In the Recognition framework this supports the adjacent Gray-cover objects that appear in the patterns layer feeding the eight-tick octave and the D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.