pith. sign in
module module high

IndisputableMonolith.Patterns

show as:
view Lean formalization →

Patterns establishes that a complete cover of exact length 2^d exists for any d-dimensional pattern. Modules on simplicial ledgers, eight-tick dynamics, and volcanic forcing cite it to secure exactness in discrete structures. The argument rests on finitary type definitions followed by surjectivity and cardinality lemmas.

claimThere exists a complete cover of exact length $2^d$ for $d$-dimensional patterns.

background

The module introduces Pattern as a finite type whose cardinality encodes d-dimensional binary configurations. CompleteCover is defined as a surjective function from a domain of size 2^d onto the pattern space, with supporting results on minimal covers and obstructions. The local setting supplies the combinatorial substrate for the eight-tick octave (T7) and window neutrality used in downstream ledger and dynamics modules.

proof idea

This is a definition module. It supplies the Pattern type, the Fintype instance, and the CompleteCover predicate, then proves covering lemmas (cover_exact_pow, eight_tick_min, T7_nyquist_obstruction) via direct cardinality calculations and bijection constructions.

why it matters in Recognition Science

The module feeds SimplicialLedger (coordinate-free sheaf representation), EightTickDynamics (8-step stability unit), WindowNeutrality (gap weight w8), and VolcanicForcingAsJCostImpulse (exponent derivation). It supplies the T7 combinatorial step that enables exact ledger covers and the alpha band derivation.

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)