ml_is_phi_power
plain-language theorem explainer
When the recognition cost differential equals an integer multiple of the elementary bit cost ln φ, the equilibrium mass-to-light ratio equals φ to that power. Stellar modelers using Recognition Science would cite this to place M/L ratios on the discrete phi-ladder. The proof substitutes the hypothesis into the exponential definition of the cost-derived ratio and reduces via real exponentiation identities.
Claim. If the cost differential satisfies $Δδ = n · ln φ$ for integer $n$, then the equilibrium mass-to-light ratio obtained from J-minimization equals $φ^n$.
background
The StellarAssembly module derives stellar M/L ratios from the recognition cost differential between photon emission and mass storage under J-minimization. J_bit is the elementary ledger bit cost defined as ln φ. The definition ml_from_cost_diff returns exp(Δδ) as the equilibrium partition minimizing total J-cost. This sits inside the recognition-weighted collapse strategy, where the eight-tick cycle separates mass accumulation (ticks 1-5) from light emission (ticks 6-8). Upstream results include the nuclear density structure from NucleosynthesisTiers.of and the fundamental tick from Constants.
proof idea
The proof is a term-mode reduction. It simplifies using the definitions of ml_from_cost_diff and J_bit, substitutes the hypothesis, invokes positivity of φ from Constants.phi_pos, applies the real power identity Real.rpow_intCast together with rpow_def_of_pos, and finishes with ring normalization.
why it matters
This supplies the explicit power form consumed by the main theorem in Derivations.MassToLight.ml_is_phi_power, which places observed ratios near phi powers. It implements the module claim that M/L lies on the phi-ladder for n in [0,3], linking directly to the eight-tick octave (T7) and the Recognition Composition Law. The result closes the path from cost minimization to observable stellar scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.