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

Tick

show as:
view Lean formalization →

The declaration introduces the eight-tick clock as the discrete temporal unit for mass-ribbon constructions. Astrophysicists working on nucleosynthesis tiers and stellar mass-luminosity relations cite it when discretizing phi-ladder calculations into octaves. It is supplied by a direct abbreviation to the finite set Fin 8, inheriting decidable equality and ordering from the ledger-tick structure.

claimThe eight-tick clock is the finite set $Fin 8 = {0,1,2,3,4,5,6,7}$.

background

In Recognition Science the atomic unit of temporal progression is the ledger tick, a structure carrying a natural-number index where time advances discretely rather than along a continuous manifold. The present module specialises this to an eight-element cycle to support the phi-ladder ribbon model for masses. The local theoretical setting is explicitly a placeholder narrative scaffold; downstream code consumes these definitions as demo inputs while the RS derivations remain unformalised.

proof idea

This is a direct abbreviation to Fin 8. No lemmas or tactics are invoked beyond the standard construction of the finite set with eight elements.

why it matters in Recognition Science

The definition supplies the eight-tick quantization required by parent results such as ml_nucleosynthesis_eq_phi and ml_is_phi_power in astrophysics, and by crystal-symmetry theorems in chemistry. It realises the T7 eight-tick octave of the forcing chain inside the mass domain. The module remains a model scaffold, leaving open the formal derivation of the period-8 cycle from J-uniqueness and the self-similar fixed point.

scope and limits

formal statement (Lean)

  15abbrev Tick := Fin 8

used by (40)

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

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.