pith. machine review for the scientific record. sign in
def definition def or abbrev high

eightbeat_prop

show as:
view Lean formalization →

The definition asserts the existence of a complete cover of three-dimensional patterns with period exactly eight. Researchers studying the eight-tick octave in Recognition Science cite this as the concrete statement of T7 for spatial dimension three. It is a direct definition packaging the existential claim from the complete cover structure for downstream adapter lemmas.

claimThere exists a complete cover $w$ of three-dimensional patterns such that the period of $w$ equals 8.

background

A complete cover in dimension $d$ is a structure containing a natural number period, a function assigning a $d$-dimensional pattern to each position in a finite set of that length, and a surjectivity condition ensuring every pattern appears. The documentation for this structure states that there exists a complete cover of exact length $2^d$ for $d$-dimensional patterns. This definition resides in the eight-beat adapter module, which specializes the eight-tick octave of period $2^3$ to the case of three spatial dimensions required by the forcing chain at T7.

proof idea

This declaration is a direct definition of the proposition. It asserts the existence by applying the complete cover constructor to dimension three and equating the period field to eight. No lemmas or tactics are applied in the body.

why it matters in Recognition Science

The proposition feeds directly into the lemma establishing the eight-beat property, which applies period_exactly_8 from the patterns module. It realizes the eight-tick octave (T7) in the unified forcing chain, where the period $2^3$ aligns with three spatial dimensions and connects to the phi-ladder and recognition composition law.

scope and limits

formal statement (Lean)

   8def eightbeat_prop : Prop := ∃ w : IndisputableMonolith.Patterns.CompleteCover 3, w.period = 8

proof body

Definition body.

   9

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.