mass_ticks
plain-language theorem explainer
The definition sets the mass accumulation phase to five ticks inside each eight-tick recognition cycle. Astrophysicists computing stellar mass-to-light ratios from recognition-cost differentials would cite this constant when placing M/L on the phi-ladder. It is introduced by direct numerical assignment with no lemmas or proof obligations.
Claim. Let $m$ denote the number of mass-accumulation ticks in the eight-tick cycle. Then $m=5$.
background
The module derives stellar M/L ratios by minimizing total ledger cost during collapse, using the convex cost $J(x)=½(x+1/x)-1$ that obeys the Recognition Composition Law. Recognition events are partitioned by the eight-tick octave into a mass-storage phase (ticks 1-5) and a light-emission phase (ticks 6-8), fixing the integer $n$ such that M/L lies on the phi-ladder at values $φ^n$ for $n∈[0,3]$.
proof idea
Direct numerical definition; no lemmas or tactics are applied.
why it matters
The constant supplies the mass-phase length required by the downstream tick_partition theorem (mass_ticks + light_ticks = total_ticks) and the tick_ratio definition. It encodes the eight-tick octave (T7) inside the stellar-assembly derivation, determining the base scaling tier for M/L ≈ φ^1 that the module documentation states matches observed stellar populations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.