total_ticks
plain-language theorem explainer
The declaration defines the total tick count in the eight-tick octave as the constant 8. Astrophysicists deriving stellar mass-to-light ratios from recognition cost differentials would cite this when fixing the base scaling tier for emission versus storage partitions. The definition is a direct constant assignment requiring no lemmas or computation.
Claim. Define the total number of ticks $N$ in the octave structure by $N := 8$.
background
The StellarAssembly module derives stellar M/L ratios from the recognition cost differential between photon emission and mass storage during collapse. It employs the convex cost J(x) = ½(x + 1/x) - 1 together with the phi-ladder scaling, where the integer exponent n is fixed by the eight-tick octave structure (period 2^3). This definition supplies the constant total tick count that appears in the partition relation.
proof idea
The definition is a direct constant assignment total_ticks := 8 with no lemmas applied.
why it matters
This constant anchors the tick_partition theorem (mass_ticks + light_ticks = total_ticks) that fixes the base scaling tier. It implements the eight-tick octave landmark (T7) from the forcing chain, ensuring M/L ratios lie on the phi-ladder in {φ^n : n ∈ [0,3]} as stated in the module documentation. It closes the integer n required for the recognition-weighted collapse model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.