pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Patterns

show as:
view Lean formalization →

The Patterns module establishes existence of a complete cover of exact length 2^d for d-dimensional patterns. Researchers on the T7 eight-tick octave cite it to anchor discrete periodicity in Recognition Science. The module achieves this via inductive definitions of the Pattern type together with cardinality arguments that force the cover length to a pure power of two.

claimThere exists a complete cover of the space of $d$-dimensional patterns whose length is exactly $2^d$.

background

This module belongs to the Patterns domain and introduces the inductive type Pattern together with the CompleteCover predicate. Pattern encodes finite d-dimensional configurations whose cardinality is controlled by the power-of-two law. The local setting is the T7 step of the forcing chain, where self-similar fixed points produce an eight-tick octave of period 2^3.

proof idea

This is a definition module that introduces the Pattern type, the CompleteCover predicate, and supporting theorems on cardinality and covering. Results such as cover_exact_pow are obtained by induction on dimension together with finiteness lemmas from Mathlib.

why it matters in Recognition Science

The module supplies the exact-cover result imported by ConstantsAndPatterns, SimplicialLedger, EightTickDynamics, WindowNeutrality, and VolcanicForcingAsJCostImpulse. It fills the T7 position in the forcing chain by guaranteeing covers of length 2^d, which matches the octave period and enables gap-weight derivations for alpha inverse.

scope and limits

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (10)