grayCycle3_surjective
plain-language theorem explainer
The map from the cyclic index set of order 8 to the 3-dimensional pattern space via the reflected Gray code construction is surjective. Researchers formalizing Hamiltonian cycles on hypercubes or the eight-tick structures in Recognition Science cite this to certify full coverage of all 2^3 patterns. The proof is a one-line extraction of the surjectivity component from the bijectivity theorem on the same map.
Claim. Let $P_3$ denote the set of functions from a 3-element index set to the booleans (i.e., the vertices of the 3-dimensional hypercube). Let $g: C_8 → P_3$ be the path function realizing the standard 3-bit reflected Gray code. Then $g$ is surjective.
background
A Pattern d is defined as a function from Fin d to Bool, so Pattern 3 is the set of all 3-bit strings with cardinality 8. Two patterns are adjacent when they differ in exactly one coordinate, turning the state space into the 3-cube graph. A Gray cycle is a Hamiltonian cycle on this graph: a closed walk of length 8 that visits every pattern once.
proof idea
The proof is a one-line wrapper that applies the second projection of the bijectivity theorem grayCycle3_bijective, which already establishes that the path function grayCycle3Path is both injective and surjective.
why it matters
This result supplies the completeness axiom for the GrayCover 3 8 object, which packages the explicit path, its surjectivity, and the one-bit step property. It directly supports the eight-tick octave (period 2^3) required by the T7 step of the forcing chain and the D = 3 spatial dimension, bridging pure cardinality coverage to an adjacency-respecting cycle usable in downstream pattern theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.