brgcPath_injective
plain-language theorem explainer
The recursive binary-reflected Gray code construction yields an injective map from Fin(2^d) to the space of d-bit patterns for every natural number d. Researchers formalizing discrete cycles or Gray-code paths in combinatorial settings cite this result to guarantee distinct sequences before adding adjacency properties. The proof is by induction on d: the base case exploits that Fin 1 is a subsingleton, while the successor case splits the path into left and right halves, establishes injectivity and disjointness of each half, and invokes the Fin-
Claim. For every natural number $d$, the map $brgcPath_d : Fin(2^d) → Pattern_d$ is injective, where $brgcPath_d$ is defined recursively by $brgcPath_0$ sending the unique element to the zero pattern and $brgcPath_{d+1}(i)$ obtained by appending a false bit to $brgcPath_d$ on the first half and a true bit to the reversed $brgcPath_d$ on the second half.
background
The GrayCycleBRGC module constructs Gray cycles axiom-free via the standard recursive BRGC rule: BRGC(0) consists of the single zero pattern and BRGC(d+1) concatenates the previous level with a false appended bit to the direct path and a true appended bit to the reversed path. Pattern d is the type of binary strings of length d, realized concretely as maps Fin d → Bool. The function brgcPath d : Fin(2^d) → Pattern d implements this recursion directly, using the auxiliary snocBit to append a single bit and Fin.rev to reverse the index range.
proof idea
Proof by induction on d. The d = 0 case reduces to the fact that Fin 1 is a subsingleton, so any two indices are equal. In the successor case the path is rewritten as Fin.append left right where left appends false to brgcPath d and right appends true to the reversed brgcPath d. Injectivity of left follows from the inductive hypothesis by projecting the first d coordinates; injectivity of right follows similarly after applying Fin.rev_injective. The halves are shown disjoint by inspecting the final bit. These three facts feed Fin.append_injective_iff to obtain injectivity of the append map, which is then transported back by casting along the equality 2^(d+1) = T + T.
why it matters
The theorem supplies the injectivity hypothesis required by the downstream definitions brgcGrayCycle and brgcGrayCover in the same module; those packaged objects are in turn imported by GrayCycleGeneral to obtain GrayCycle and GrayCover instances for arbitrary dimension. It therefore completes the injectivity leg of the axiom-free recursive BRGC construction described in the module documentation. Within Recognition Science the result supports discrete combinatorial scaffolding that can feed higher-level pattern models, though it remains independent of the phi-ladder or forcing-chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.