ml_stellar_value
plain-language theorem explainer
Stellar mass-to-light ratio equals the golden ratio φ in Recognition Science units. Astrophysicists comparing derived M/L values to observations in stellar populations would cite this result. The proof is a one-line wrapper that unfolds the definition of ml_stellar as φ raised to the characteristic tier scaffold of 1, followed by zpow simplification.
Claim. The stellar mass-to-light ratio equals the golden ratio $\phi$, where the ratio is obtained from the recognition cost differential between photon emission and mass storage at equilibrium.
background
The module derives M/L from the recognition cost differential during stellar collapse. Photon emission carries cost δ_emit = J(r_emit) and mass storage carries δ_store = J(r_store), with the convex cost function J(x) = ½(x + 1/x) - 1. At equilibrium the ratio M/L minimizes total ledger cost and lands on the φ-ladder.
characteristic_tier_scaffold is the integer tier level fixed by the 5:3 partition of the eight-tick cycle and equals 1. ml_stellar is then defined as the noncomputable real φ raised to that tier. The upstream NucleosynthesisTiers.of structure supplies the discrete φ-tier occupation for nuclear densities and photon fluxes.
The local setting is the Recognition Science derivation of stellar assembly via recognition-weighted collapse, with M/L ∈ {φ^n : n ∈ ℤ, n ∈ [0, 3]} and the typical value φ^1 ≈ 1.618 solar units.
proof idea
The term proof is a one-line wrapper. It unfolds ml_stellar and characteristic_tier_scaffold, then applies simp only on zpow_one to reduce φ^1 directly to φ.
why it matters
This theorem supplies the stellar-assembly value of M/L that is required by the three downstream consistency results: three_strategies_agree (which equates StellarAssembly, NucleosynthesisTiers and geometric derivations), strategies_agree, and agrees_with_stellar_assembly. It fills the stellar-assembly step of the M/L derivation in the module doc-comment and anchors the φ-ladder result to the eight-tick structure (T7) and D = 3 spatial dimensions (T8) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.