pattern3_injective
plain-language theorem explainer
The map sending each index in Fin 8 to its 3-bit pattern is injective. Researchers constructing explicit Hamiltonian cycles on the 3-cube cite it to guarantee that the eight codewords remain distinct before imposing adjacency. The proof reduces injectivity to the identity property of the composition with the binary decoder toNat3.
Claim. The function that sends each $k$ in the set of integers from 0 to 7 to the 3-bit Boolean vector whose $j$-th coordinate is true precisely when the $j$-th bit of $k$ is set is injective.
background
In the GrayCycle module, a pattern of dimension $d$ is a function from Fin $d$ to Bool, i.e., a vertex of the $d$-dimensional hypercube. The definition pattern3 converts an element of Fin 8 into a 3-bit pattern by explicit case analysis on the index, equivalent to setting bits via the binary representation. The function toNat3 recovers the natural number from any 3-bit pattern by summing the appropriate powers of two. The supporting lemma toNat3_pattern3 states that toNat3 composed with pattern3 recovers the original index exactly.
proof idea
Assume pattern3 a equals pattern3 b. Apply toNat3 to both sides to obtain toNat3 (pattern3 a) equals toNat3 (pattern3 b) by congruence. The lemma toNat3_pattern3 then forces the underlying natural numbers to be equal. Fin.ext concludes that a equals b.
why it matters
The result is invoked directly inside grayCycle3_injective to transfer injectivity from the pattern map to the full cycle path grayCycle3Path. It supplies the distinctness step required for the eight-tick octave (T7) in the forcing chain, confirming that the 2^3 patterns are realized without repetition before adjacency is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.