Tick
plain-language theorem explainer
Tick defines the eight-element finite set that supplies the discrete clock for ribbon mass models. Researchers deriving nucleosynthesis tiers or stellar mass-luminosity relations cite it to enforce eight-tick periodicity in their calculations. The declaration is a direct abbreviation to Fin 8 that carries no additional proof obligations.
Claim. Let $Tick$ denote the eight-tick clock, realized as the finite set $Fin 8$.
background
The Masses.Ribbons module supplies auxiliary tick helpers for narrative ribbon constructions that illustrate mass relations. These helpers are explicitly categorized as Model and are not yet invoked inside any proven theorems. Upstream, Foundation.TimeEmergence.Tick supplies the underlying atomic discrete time unit as a structure carrying a natural-number index with no background manifold.
proof idea
The declaration is a direct abbreviation that equates Tick to Fin 8.
why it matters
This abbreviation realizes the eight-tick octave (period 2^3) from the forcing chain and supplies the discrete clock used by ml_nucleosynthesis_eq_phi, which contains an explicit Eight-Tick Quantization section, and by ml_is_phi_power in StellarAssembly. It also appears in downstream chemistry results on crystal symmetry and ferromagnetism. The module documentation notes that these ribbon helpers remain outside the core theorem set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.