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

eight_tick

show as:
view Lean formalization →

The declaration defines the eight-tick period as the constant natural number 8, which serves as the fundamental time unit τ₀ in Recognition Science. Researchers in dimension forcing or finite-temperature thermodynamics cite it to fix the IR cutoff at f₀ = 1/(8 τ₀) and to enforce 2^3 periodicity. It is introduced by direct constant assignment with no computation or proof obligations.

claimThe eight-tick period is the natural number $8$, which equals $2^3$ and supplies the fundamental time unit τ₀ for recognition dynamics.

background

The Recognition Thermodynamics module extends J-cost minimization to finite Recognition Temperature TR, defining the Gibbs measure p(x) ∝ exp(-J(x)/TR) with J(x) = ½(x + 1/x) - 1. The module doc states that the 8-tick cycle provides the fundamental time unit τ₀ and sets the natural frequency scale f₀ = 1/(8 τ₀). Upstream results from DimensionForcing, Gap45, and RRF.Constants each introduce the same constant 8 as the period arising from ledger coverage of 2^D at D = 3.

proof idea

The definition is a direct constant assignment eight_tick := 8. It functions as a one-line wrapper that supplies the numerical value required by downstream theorems such as eight_tick_is_2_cubed and D3_compatible.

why it matters in Recognition Science

This supplies the concrete value for the eight-tick period that forces D = 3, as used in theorems eight_tick_forces_D3, eight_tick_is_2_cubed, and the structure RSCompatibleDimension. It realizes the T7 landmark (eight-tick octave of period 2^3) in the forcing chain and appears in 30 downstream declarations that close the D = 3 compatibility argument. No open scaffolding questions are attached to this definition.

scope and limits

Lean usage

theorem eight_tick_is_2_cubed : eight_tick = 2^3 := rfl

formal statement (Lean)

 283def eight_tick : ℕ := 8

proof body

Definition body.

 284
 285/-- The natural frequency scale: f_0 = 1 / (8 * τ₀).
 286    This sets the IR cutoff for recognition dynamics. -/

used by (30)

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

depends on (5)

Lean names referenced from this declaration's body.