grayCover3
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish GrayCover for dimensions other than 3.
- Does not prove that period 8 is minimal.
- Does not connect to the Recognition Composition Law.
- Does not address mass formulas or phi-ladder.
- Does not provide a general construction for arbitrary d.
formal statement (Lean)
212def grayCover3 : GrayCover 3 8 :=
proof body
Definition body.
213{ path := grayCycle3Path
214, complete := grayCycle3_surjective
215, oneBit_step := grayCycle3_oneBit_step
216}
217
218end Patterns
219end IndisputableMonolith