brgcPath_injective
plain-language theorem explainer
The binary-reflected Gray code path map is shown to be injective from the set of d-bit indices to d-bit patterns, for dimensions d between 1 and 64 inclusive. Researchers constructing discrete Gray cycles within the Recognition Science framework cite this to ensure distinct representatives. The proof equates the Gray code bit strings via componentwise inspection and recovers the indices through inversion under the 64-bit bound.
Claim. For each natural number $d$ satisfying $0 < d ≤ 64$, the binary-reflected Gray code path function from the finite set of size $2^d$ to the set of length-$d$ patterns is injective.
background
Patterns are finite windows of length n, serving as the discrete bit-vector objects in the information and complexity structures. The module develops a bounded construction of Gray covers and cycles for general dimension d via the BRGC formula gray(n) = n XOR (n >>> 1), packaged as GrayCover d (2^d) and GrayCycle d. This is the Workstream A generalization that remains definitional but routes the 64-bit inverse through GrayCodeAxioms, in contrast to the axiom-free recursive version elsewhere.
proof idea
Assume the paths at indices i and j agree. For each bit position k < d the pattern components match by congruence, so the test bits of the underlying Gray codes agree. For k ≥ d both test bits are false by the lemma natToGray_testBit_false_of_ge. The Gray codes are therefore identical by Nat.eq_of_testBit_eq. The bound d ≤ 64 places both indices below 2^64, so GrayCodeFacts.grayToNat_inverts_natToGray recovers the original values and Fin.ext finishes the argument.
why it matters
The result supplies the injectivity field required by brgcGrayCycle and brgcGrayCover in this module and in GrayCycleBRGC. It thereby completes the bounded BRGC-based Gray cycle packaging for general d under the module's stated assumptions. The construction supports the discrete pattern layer that feeds the physics complexity structure, while the primary D=3 case avoids the 64-bit bound entirely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.