grayCover3
plain-language theorem explainer
The definition assembles a GrayCover structure for three-bit patterns over eight steps. It supplies the explicit Gray-cycle path together with proofs of surjectivity and single-bit adjacency. Pattern theorists and hypercube researchers cite it to certify an adjacent Hamiltonian cycle on the three-dimensional cube. The construction is a direct record literal that invokes the path definition, the surjectivity theorem, and the one-bit step theorem.
Claim. Let $P$ be the 3-bit Gray-code path $P: Fin 8 → {0,1}^3$. Then $P$ is a Gray cover: $P$ is surjective onto all 3-bit patterns and consecutive values differ in exactly one coordinate.
background
GrayCover is the structure requiring a path from Fin T to Pattern d, a surjection onto all 2^d patterns, and the one-bit difference condition between consecutive steps. Pattern d denotes functions from Fin d to Bool. The module upgrades earlier cardinality coverage results to explicit adjacency using the binary-reflected Gray code. Upstream results include the path definition via pattern3 and gray8At, the surjectivity theorem derived from bijectivity, and the one-bit step theorem proved by eight explicit case splits.
proof idea
The definition is a one-line wrapper that populates the GrayCover record with three components: the path from grayCycle3Path, the completeness proof from grayCycle3_surjective, and the adjacency proof from grayCycle3_oneBit_step. No additional tactics are applied beyond record construction.
why it matters
This supplies the concrete 8-tick adjacent cycle for dimension 3, realizing the eight-tick octave and D=3 from the forcing chain. It strengthens the period_exactly_8 cardinality fact by adding the one-bit adjacency required for ledger-compatible stories. No downstream uses appear yet, but the construction closes the explicit cycle for the base case d=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.