CompleteCover
The complete cover structure for dimension d consists of a period together with a surjective path through all boolean patterns on d bits. Researchers working on discrete eight-tick dynamics cite this object when stating the existence of minimal periodic coverings in three dimensions. It is introduced as a direct record definition carrying the surjectivity condition as a field.
claimA complete cover in dimension $d$ is a structure comprising a natural number $p$ (the period), a function from the finite set of size $p$ to the set of all maps from $d$ coordinates to booleans, and a proof that the function is surjective.
background
Pattern d denotes the finite type of all functions from a d-element set to the booleans, hence containing exactly 2^d elements. The complete cover structure assembles a finite sequence of these patterns together with the requirement that the sequence visits every element of the type. This construction appears in the Patterns module to support statements about exhaustive periodic traversals of pattern spaces.
proof idea
As a structure definition the declaration simply declares the three fields period, path and complete. No tactics or lemmas are invoked; the surjectivity condition is recorded directly as a field.
why it matters in Recognition Science
This structure is the type appearing in the statement that an eight-tick cycle exists for three-dimensional patterns and in the construction of exact-length covers whose period equals 2 to the power d. It thereby realizes the T7 eight-tick octave of the unified forcing chain by furnishing the periodic object that covers the full pattern space at the threshold 2^D. The same object is referenced when establishing the bijection at that threshold and when defining the eight-beat property in the URC adapter.
scope and limits
- Does not assert existence of any cover.
- Does not require minimality of the period.
- Does not specify dynamics or transitions between successive patterns.
- Does not link the cover to continuous physics or constants such as the fine-structure constant.
formal statement (Lean)
15structure CompleteCover (d : Nat) where
16 period : ℕ
17 path : Fin period → Pattern d
18 complete : Function.Surjective path
19
20/-- There exists a complete cover of exact length `2^d` for d‑dimensional patterns. -/