tick_ratio_value
plain-language theorem explainer
The declaration fixes the tick ratio at exactly 5/3 for the stellar assembly model. Researchers deriving mass-to-light ratios from recognition cost differentials would cite it to anchor the base scaling tier before applying the phi-ladder. The eight-tick octave partitions into five mass ticks and three light ticks. The proof is a direct reflexivity step on the definition of tick_ratio as their quotient.
Claim. The ratio of mass storage ticks to light emission ticks equals $5/3$.
background
Stellar assembly derives the mass-to-light ratio from the recognition cost differential between photon emission (cost J(r_emit)) and mass storage (cost J(r_store)), where J(x) = ½(x + 1/x) - 1 is the unique convex cost function. The tick ratio is defined as mass_ticks / light_ticks, with each tick the fundamental RS time quantum τ₀ = 1. This ratio fixes the base scaling tier that places M/L on the phi-ladder with values φ^n for integer n in [0, 3].
proof idea
The proof is a one-line reflexivity wrapper. It equates the definition tick_ratio := mass_ticks / light_ticks directly to the constant 5/3 that arises from the eight-tick partition (five mass ticks, three light ticks). No further lemmas are invoked beyond the definition and the partition structure.
why it matters
This anchors the integer n in the eight-tick structure that determines the cost differential Δδ and therefore the M/L value on the phi-ladder. It connects to the T7 octave and supplies the concrete ratio 5/3 ≈ 1.667 whose proximity to φ ≈ 1.618 contributes to the observed cost spread. The module doc-comment states that the integer n is fixed by the eight-tick structure, making this the concrete numerical step that closes the derivation for typical stellar populations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.