ml_geometric_bounds
plain-language theorem explainer
The geometric mass-to-light ratio, obtained from recognition length and coherence volume constraints, equals the golden ratio and therefore satisfies 1 < M/L < 2. Astrophysicists working on stellar observability limits cite the bound to confirm consistency with the J-cost fixed point. The proof is a direct unfolding of the definition followed by application of the two standard inequalities for phi.
Claim. Let $ml$ denote the geometric mass-to-light ratio defined as the golden ratio $phi$. Then $1 < ml < 2$.
background
The ObservabilityLimits module develops Strategy 3 for recognition-bounded observability. Observable flux must exceed the coherence threshold $E_{coh}/tau_0$ while mass assembles inside coherence volumes of size $l_{rec}^3$. The definition ml_geometric sets the ratio exactly to $phi$, the unique fixed point of the J-cost recursion. Upstream, the structure of nuclear densities and photon fluxes appears in NucleosynthesisTiers.of, while one_lt_phi and phi_lt_two establish the bounds on $phi$ by direct comparison of square roots.
proof idea
Unfold ml_geometric to replace it by $phi$. Apply constructor to split the conjunction. Discharge the left conjunct with the lemma one_lt_phi and the right conjunct with phi_lt_two.
why it matters
This bound is invoked by the main theorem ml_from_geometry_only, which equates the geometric ratio to the values obtained from StellarAssembly and NucleosynthesisTiers while tightening the interval to 1 < ml < 5. It realizes the module claim that M/L lies in the set of phi powers for exponents in [0,3] and anchors the geometric route in the three-strategy agreement. The result uses the self-similar fixed point property of phi from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.