brgcPath_injective
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-
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove one-bit adjacency of consecutive elements.
- Does not establish surjectivity onto all of Pattern d.
- Does not rely on or prove any bitwise Gray-code formula.
- Does not impose an upper bound on d.
- Does not address computational complexity of the path.
Lean usage
noncomputable def brgcGrayCycle (d : Nat) (hdpos : 0 < d) : GrayCycle d := { path := brgcPath d, inj := brgcPath_injective d, oneBit_step := brgc_oneBit_step d hdpos }formal statement (Lean)
72theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
73 | 0 => by
74 intro i j _
75 -- `Fin 1` is a subsingleton (only `0`)
76 simpa [Fin.eq_zero i, Fin.eq_zero j]
77 | (d + 1) => by
78 intro i j hij
79 -- unfold the `d+1` definition and reduce to injectivity of the appended halves
80 classical
81 let T : Nat := 2 ^ d
proof body
Tactic-mode proof.
82 have hTT : 2 ^ (d + 1) = T + T := by
83 simpa [T, twoPow_succ_eq_add d]
84 let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
85 let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
86 have hij' :
87 Fin.append left right (i.cast hTT) = Fin.append left right (j.cast hTT) := by
88 simpa [brgcPath, T, hTT, left, right] using hij
89
90 have hleft_inj : Function.Injective left := by
91 intro a b hab
92 have hab' : brgcPath d a = brgcPath d b := by
93 funext k
94 have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
95 simpa [left, snocBit] using this
96 exact (brgcPath_injective d) hab'
97
98 have hright_inj : Function.Injective right := by
99 intro a b hab
100 have hab' : brgcPath d (Fin.rev a) = brgcPath d (Fin.rev b) := by
101 funext k
102 have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
103 simpa [right, snocBit] using this
104 have : Fin.rev a = Fin.rev b := (brgcPath_injective d) hab'
105 exact Fin.rev_injective this
106
107 have hdis : ∀ a b : Fin T, left a ≠ right b := by
108 intro a b hab
109 have := congrArg (fun p : Pattern (d + 1) => p (Fin.last d)) hab
110 -- last coordinate is the appended bit: false on left, true on right
111 simpa [left, right] using this
112
113 have happ_inj : Function.Injective (Fin.append left right) :=
114 (Fin.append_injective_iff (xs := left) (ys := right)).2 ⟨hleft_inj, hright_inj, hdis⟩
115
116 have hcast : i.cast hTT = j.cast hTT := happ_inj hij'
117 -- cast back along the inverse equality
118 have := congrArg (Fin.cast hTT.symm) hcast
119 simpa [hTT] using this
120
121/-! ## One-bit adjacency -/
122