CompleteCover
plain-language theorem explainer
CompleteCover d packages a natural number N with a surjective map from a set of size N into the space of all 2^d binary patterns on d coordinates. Results on the eight-tick cycle and the T7 threshold bijection cite this structure to state covering periods. The declaration is introduced directly as a structure definition with three fields.
Claim. A complete cover of dimension $d$ consists of a natural number $N$, a function $p$ from the set of size $N$ to the set of all maps from a $d$-element index set to the two-element set, and a proof that $p$ is surjective.
background
Pattern d is defined as the type of all functions Fin d → Bool, hence the discrete space containing exactly 2^d distinct d-bit patterns. The structure CompleteCover d assembles a finite interval, a path through this space, and the surjectivity condition that every pattern appears at least once.
proof idea
The declaration is a structure definition that directly encodes the three required fields: period, path, and the surjectivity predicate.
why it matters
It supplies the type used by eight_tick_cycle_exists to assert an 8-period cover in D=3, by cover_exact_pow to construct a cover of length exactly 2^d, and by T7_threshold_bijection to obtain a bijection at the threshold. This places the definition at the interface between pattern enumeration and the eight-tick octave (T7) forced in the Unified Forcing Chain for spatial dimension 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.