grayCover3
The declaration assembles the 3-bit Gray cycle into a Gray cover structure of period 8. Researchers working on hypercube Hamiltonian paths or adjacent pattern coverage in Recognition Science would cite this object to certify both full visitation and single-bit transitions. The definition is a direct record that bundles a pre-built path, a surjectivity result, and an explicit one-bit step lemma.
claimA Gray cover for dimension 3 and period 8 is the record whose path is the standard 3-bit Gray-code sequence from Fin 8 to the 3-bit pattern space, whose image is the entire pattern space, and whose consecutive states differ in exactly one coordinate.
background
Gray cover is the structure that records a path of length T through the d-dimensional pattern space (maps from Fin d to Bool), requires the path to be surjective, and demands that each step changes exactly one coordinate. For d = 3 the natural period is 8, matching the hypercube vertex count and the eight-tick octave of the framework.
proof idea
The definition is a one-line record constructor. It supplies the path component from the 3-bit Gray cycle path definition, the completeness component from the surjectivity theorem on that path, and the adjacency component from the one-bit transition theorem that checks each of the eight steps.
why it matters in Recognition Science
This supplies the concrete adjacent-cycle instance for the 3-bit patterns, upgrading the earlier cardinality coverage fact to the stronger Hamiltonian requirement needed for ledger-compatible adjacency. It realizes the eight-tick octave for D = 3 inside the Recognition framework and stands ready for any downstream argument that needs both full coverage and single-bit steps, though the module lists no immediate parent theorem.
scope and limits
- Does not establish Gray covers for any dimension other than 3.
- Does not prove minimality of period 8 beyond the general remark attached to the Gray cover structure.
- Does not contain the recursive construction of the Gray code.
- Does not reference the forcing chain steps T0-T8 or the Recognition Composition Law.
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