gray8At_injective
plain-language theorem explainer
The map gray8At, sending each index in Fin 8 to the corresponding entry in the sequence [0,1,3,2,6,7,5,4], is injective. Pattern enumeration work in Recognition Science cites the result when building uniqueness for 3-bit Gray cycles. The proof is an exhaustive case split over the finite domain of eight inputs.
Claim. The function $f : Fin 8 → Fin 8$ defined by the 3-bit Gray sequence $f(0)=0$, $f(1)=1$, $f(2)=3$, $f(3)=2$, $f(4)=6$, $f(5)=7$, $f(6)=5$, $f(7)=4$ is injective.
background
The GrayCycle module equips the state space Pattern d := Fin d → Bool with one-bit-flip adjacency and requires a closed walk of length exactly 2^d that visits every pattern once. The function gray8At supplies the explicit ordering [0,1,3,2,6,7,5,4] that realizes this cycle for d=3. The module is self-contained and does not invoke external Gray-code axioms; it relies only on the standard recursive BRGC construction.
proof idea
The term proof opens with intro i j h, then applies fin_cases to both i and j. Each of the resulting 64 branches reduces the equality hypothesis by cases and closes by rfl.
why it matters
The result is invoked inside grayCycle3_injective to transfer injectivity from gray8At to the path grayCycle3Path. It therefore supplies the uniqueness step required for the Hamiltonian-cycle formulation that aligns ledger adjacency with the eight-tick octave (T7) and D=3 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.