effective_tier
plain-language theorem explainer
The definition computes the effective φ-tier for stellar mass-to-light ratios as ln(tick_ratio) divided by the elementary bit cost J_bit = ln φ. Astrophysicists modeling recognition-weighted stellar collapse would cite this quantity to place M/L on the φ-ladder. It is a direct normalization of the logarithmic scaling from the mass-to-light tick partition.
Claim. The effective tier is defined by $n = {ln(r)} / {ln φ}$, where $r$ is the ratio of mass ticks to light ticks obtained from the eight-tick partition.
background
The StellarAssembly module models stellar collapse as minimization of total recognition cost between photon emission (cost J(r_emit)) and mass storage (cost J(r_store)). The convex cost J(x) = ½(x + 1/x) - 1 produces differentials measured in units of J_bit = ln φ. tick_ratio is defined as mass_ticks / light_ticks and encodes the 5:3 partition of the eight-tick cycle. Upstream, tick is the fundamental RS time quantum fixed at 1, and J_bit is the positive elementary ledger cost established in the PhiSupport lemmas.
proof idea
This is a direct definition that normalizes the natural logarithm of tick_ratio by J_bit. No lemmas are applied beyond the referenced definitions of tick_ratio and J_bit.
why it matters
This definition supplies the characteristic φ-tier that realizes the module's main result: stellar M/L lies on the φ-ladder with typical value ≈ φ¹. It implements the eight-tick octave (T7) and the cost-differential partition described in the module doc-comment. The 5/3 ratio approximates φ, with the residual absorbed into Δδ. No downstream declarations yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.