ml_from_geometry_only
plain-language theorem explainer
The declaration proves existence of a real mass-to-light ratio ml equal to the golden ratio φ, strictly between 1 and 5, and identical to both the stellar-assembly and nucleosynthesis derivations. Galaxy evolution modelers seeking zero-parameter M/L predictions would cite it for the geometric route. The term-mode proof instantiates the geometric definition, applies reflexivity for the φ equality, invokes the two agreement theorems, and uses linear arithmetic on the supplied bounds.
Claim. There exists a real number $ml$ such that $ml = φ$, $1 < ml < 5$, $ml$ equals the stellar-assembly mass-to-light ratio, and $ml$ equals the nucleosynthesis mass-to-light ratio.
background
In the Recognition Science setting of Strategy 3, the stellar mass-to-light ratio is obtained from observability constraints on photon flux and coherence volume. The recognition length $l_{rec}$ is the Planck-scale quantity $√(ℏG/(πc³))$, the coherence energy is $E_{coh} = φ^{-5}$, and the fundamental tick is $τ_0 = 1/(8 J_{bit})$. The J-cost functional $J(x) = ½(x + 1/x) - 1$ is minimized subject to the flux threshold $F ≥ E_{coh}/τ_0$ and the volume limit $V ~ l_{rec}^3$, producing the optimal ratio $M/L ≈ φ$.
proof idea
The proof instantiates the geometric definition ml_geometric (which equals φ by construction from the module). Reflexivity confirms the first equality; the lower bound 1 < ml is taken directly from the first component of ml_geometric_bounds; the upper bound ml < 5 follows by linear arithmetic on the second component; and the two agreement theorems supply the equalities to the stellar-assembly and nucleosynthesis values.
why it matters
The theorem supplies the third independent, zero-parameter derivation of the stellar M/L ratio, confirming consistency with the stellar-assembly and nucleosynthesis routes inside the same module. It realizes the main result stated in the module documentation that M/L lies in {φ^n : n ∈ [0,3]} with typical value φ ≈ 1.618, closing the geometric leg of the observability argument that rests on the J-cost minimization from T5 and the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.