Tick
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.