cover_exact_pow
plain-language theorem explainer
Existence of a complete cover for d-dimensional patterns with exact period 2^d. Researchers deriving the T7 threshold bijection in Recognition Science cite this to obtain the eight-tick octave for three-dimensional patterns. The proof constructs the cover explicitly from the symmetric Fintype equivalence on the pattern space and confirms the period equals the cardinality via direct simplification.
Claim. There exists a complete cover $w$ of $d$-dimensional patterns such that the period of $w$ equals $2^d$. A complete cover consists of a period $p$, a path map from Fin$(p)$ to the pattern space, and a surjectivity condition ensuring the path visits every pattern.
background
The Patterns module works with the finite space of $d$-dimensional patterns, whose cardinality is $2^d$ by the product structure over $d$ binary choices. A CompleteCover is the structure with fields period (a natural number), path (a function from Fin(period) into the pattern space), and complete (a proof that the path is surjective). This construction sits inside the Recognition Science forcing chain at the T7 step, where the eight-tick octave (period $2^3$) appears for $d=3$. Upstream results supply the fundamental tick as the discrete time quantum and the ledger factorization that calibrates the underlying J-cost.
proof idea
The tactic proof opens with classical, lets e be the symmetric of Fintype.equivFin on the pattern space, then refines a CompleteCover whose period is the cardinality, whose path is e, and whose completeness is the surjectivity of e. A separate have block proves the cardinality equals $2^d$ by simp on the pattern definition together with card_bool and card_fin, then applies that equality to finish.
why it matters
This theorem supplies the exact-period cover used by T7_threshold_bijection to obtain a bijection at threshold $T=2^D$ with no aliasing. It fills the T7 eight-tick octave step in the T0-T8 forcing chain, where $D=3$ spatial dimensions and the fundamental evolution period of one octave are forced. The result closes the discrete covering requirement that supports the phi-ladder mass formula and the alpha band calibration in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.