twoPow_succ_eq_add
plain-language theorem explainer
The lemma states that for any natural number d, 2 raised to d+1 equals twice 2 raised to d. It is cited inside the recursive BRGC path construction to equate the size of the doubled cycle in dimension d+1. The proof is a one-line term simplification that rewrites the successor power via multiplication and commutativity.
Claim. $2^{d+1} = 2^d + 2^d$ for every natural number $d$.
background
The GrayCycleBRGC module constructs Gray cycles for arbitrary dimension d via the recursive BRGC rule: BRGC(0) is the single zero pattern and BRGC(d+1) prepends a leading bit to BRGC(d) and its reverse. Pattern d is the type Fin d → Bool, i.e., d-bit assignments. The lemma supplies the arithmetic identity required when the recursive definition of brgcPath doubles the domain size from 2^d to 2^{d+1}.
proof idea
The proof is a one-line term-mode wrapper. It applies simpa to the lemmas pow_succ, Nat.mul_comm and Nat.two_mul, which together rewrite 2^(d+1) first as 2·2^d and then as 2^d + 2^d.
why it matters
The identity is invoked by brgcPath, brgc_oneBit_step and brgcPath_injective inside the same module. It closes the cardinality step in the axiom-free recursive Gray-cycle construction given in the module documentation, which avoids the bitwise gray(n) = n XOR (n >> 1) formula. In the Recognition framework the result supports pattern-cycle constructions that appear in simplicial and stream-based pattern lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.