twoPow_succ_eq_add
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 in Recognition Science
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.
scope and limits
- Does not prove injectivity or adjacency of the Gray path.
- Does not extend the identity beyond natural-number exponents.
- Does not address infinite-dimensional or continuous analogues.
- Does not connect to the J-cost or phi-ladder structures elsewhere in the monolith.
formal statement (Lean)
47private lemma twoPow_succ_eq_add (d : Nat) : 2 ^ (d + 1) = 2 ^ d + 2 ^ d := by
proof body
Term-mode proof.
48 -- `2^(d+1) = 2^d * 2 = 2 * 2^d = 2^d + 2^d`
49 simpa [pow_succ, Nat.mul_comm, Nat.two_mul]
50
51/-- The recursive BRGC path as a `Fin (2^d) → Pattern d`. -/