Pith. sign in
module module high

IndisputableMonolith.Patterns

show as:
view Lean formalization →

Foundational combinatorics of d-dimensional binary patterns on the hypercube. Defines Pattern d as maps Fin d → Bool, proves that a complete cover has exact length 2^d, and derives the eight-tick minimum together with the T7 Nyquist obstruction. Cited by Gray-cycle constructions, window neutrality, and the simplicial ledger. Arguments are finite-cardinality counting plus non-surjectivity of shorter maps.

claimA $d$-dimensional pattern is a map $\{0,\ldots,d-1\}\to\{0,1\}$. The set of all such patterns has cardinality $2^d$. A complete cover is a sequence of length exactly $2^d$ that hits every pattern; no shorter sequence can be surjective. In particular the minimal cover length for $d=3$ is eight (the eight-tick octave), and the T7 Nyquist obstruction follows.

background

Recognition Science forces an eight-tick fundamental period (T7) once spatial dimension is three (T8). The combinatorial substrate is the $d$-cube of binary patterns: each coordinate is a Boolean degree of freedom, so the state space is $\mathrm{Pattern},d:=\mathrm{Fin},d\to\mathrm{Bool}$ with $2^d$ points.

This module introduces that type, its finite cardinality, and the notion of a complete cover (a walk or listing that visits every pattern). The counting lemmas establish that any cover has length at least $2^d$ and that length exactly $2^d$ is achievable. Specializing to $d=3$ yields the eight-tick minimum and the associated Nyquist-type obstruction used later in the forcing chain.

Downstream Gray-code modules upgrade the pure counting facts to explicit Hamiltonian cycles (adjacent flips, closed walks). Window-neutrality and the simplicial ledger import the same cardinality backbone when they reason about eight-tick windows and coordinate-free ledgers.

proof idea

The module is a mix of definitions and elementary finite-set arguments. Pattern is introduced as Fin d → Bool; Fintype and card_pattern give |Pattern d| = 2^d by the usual product formula. CompleteCover packages a surjective map from a finite index set onto Pattern d. cover_exact_pow and no_surj_small show that surjectivity forces the index cardinality to be at least 2^d, with equality attainable. min_ticks_cover and eight_tick_min specialize to d = 3. T7_nyquist_obstruction and T7_threshold_bijection package the same counting into the language of the forcing chain (period below 8 cannot biject onto the 3-cube).

why it matters in Recognition Science

Supplies the discrete state space and the 2^d lower bound that underwrite T7 (eight-tick octave) in the unified forcing chain. GrayCycle, GrayCycleBRGC, and GrayCycleGeneral import it to promote bare covers to adjacent Hamiltonian cycles on the hypercube; GrayCode and GrayCodeAxioms sit on the same foundation. Measurement.WindowNeutrality uses the eight-tick minimum when linking window-8 neutrality to ledger exactness and the gap weight w₈ that enters α⁻¹. Foundation.SimplicialLedger and RecogSpec.Spec consume the pattern vocabulary for coordinate-free ledger topology and specification-level statements. Without the exact-power cover theorems the eight-tick and Nyquist claims would be floating axioms.

scope and limits

used by (12)

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

declarations in this module (10)