grayCycle3_injective
plain-language theorem explainer
The composition of the canonical 3-bit Gray ordering with the pattern encoding map yields an injective function from a set of eight elements to the vertices of the 3-cube. Researchers constructing explicit Hamiltonian cycles on hypercubes or the 8-tick structure in Recognition Science cite this result. The proof is a short reduction that first applies the injectivity of the pattern encoding and then the injectivity of the Gray ordering.
Claim. Let $g : {0,1,2,3,4,5,6,7} / {8} {0,1}^3$ be the map sending each index $i$ to the binary pattern whose natural-number value is the $i$-th entry in the sequence $0,1,3,2,6,7,5,4$. Then $g$ is injective.
background
The GrayCycle module upgrades cardinality facts about 3-bit patterns to an explicit adjacent cycle on the hypercube whose vertices are maps Fin 3 to Bool, with adjacency defined by differing in exactly one coordinate. The canonical 3-bit Gray order is the function that enumerates the indices 0 through 7 as the sequence 0,1,3,2,6,7,5,4. The path in question is obtained by feeding each index through this ordering and then through the pattern encoding map. Upstream results establish that the pattern encoding is injective by reducing pattern equality to equality of the associated natural numbers, and that the Gray ordering itself is injective by exhaustive case analysis on the eight inputs.
proof idea
Assume the path images of two indices $i$ and $j$ coincide. Apply the injectivity of the pattern encoding to recover equality of the underlying Gray indices. Then invoke the injectivity of the Gray ordering function to conclude that $i$ equals $j$.
why it matters
This injectivity supplies the required field in the definition of the GrayCycle 3 object that realizes the explicit 8-tick cycle for three spatial dimensions. It is used immediately to obtain bijectivity of the same path function. In the Recognition Science framework the result supports the eight-tick octave (period $2^3$) that appears at step T7 of the forcing chain and is needed for the ledger-compatible adjacency story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.