ml_from_cost_diff
plain-language theorem explainer
The definition computes the stellar mass-to-light ratio as the exponential of the recognition cost differential Δδ. Astrophysicists modeling equilibrium partitions during stellar collapse via J-minimization would cite this when placing M/L on the phi ladder. It is a direct one-line assignment to Real.exp that converts the differential into a ratio, which downstream theorems then identify with integer powers of phi under the condition Δδ = n · J_bit.
Claim. The equilibrium mass-to-light ratio is defined by $M/L = e^{Δδ}$, where $Δδ$ is the recognition cost difference between photon emission and mass storage.
background
Recognition Science defines the cost function J(x) = ½(x + 1/x) - 1, minimized at x = 1 with J(1) = 0. The elementary ledger bit is J_bit = ln φ. This module treats stellar collapse as a recognition-weighted process in which photon emission carries cost δ_emit = J(r_emit) and bound mass storage carries δ_store = J(r_store). The equilibrium partition minimizes total J-cost, so the ratio M/L follows from the differential Δδ = δ_emit - δ_store via exponential weighting exp(-J).
proof idea
This is a direct definition that assigns the mass-to-light ratio to the real exponential of the input cost differential Δδ. No lemmas or tactics are invoked; it is a one-line wrapper around Real.exp.
why it matters
This definition supplies the core mapping used by the theorems ml_is_phi_power and ml_is_phi_power', which establish M/L = φ^n when Δδ equals n times J_bit. It fills the derivation step in the stellar assembly strategy, connecting J-minimization to the phi-ladder result M/L ∈ {φ^n : n ∈ [0,3]}. The eight-tick structure fixes the integer n, placing typical stellar M/L near φ^1 ≈ 1.618 in solar units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.