ml_falsifiable
plain-language theorem explainer
The declaration shows that the stellar mass-to-light hypothesis forces the ratio to equal the golden ratio, supplying an immediate contradiction test for the recognition collapse model. Galaxy evolution modelers would cite it when confronting predicted M/L values with survey data. The proof is a one-line term contradiction that applies the hypothesis equality directly to the negation assumption.
Claim. Assume the hypothesis $H$ that the characteristic stellar mass-to-light ratio equals the golden ratio $φ$. Then the stellar mass-to-light ratio cannot differ from $φ$.
background
The module derives stellar mass-to-light ratios from the recognition cost difference between photon emission and bound-mass storage during collapse. The cost function is the unique convex J(x) = ½(x + 1/x) - 1, and equilibrium partitions yield values on the φ-ladder fixed by the eight-tick structure. H_StellarML is the empirical hypothesis that the characteristic ratio ml_stellar equals φ, with an explicit falsifier given by any stable population whose ratio lies off the φ^n rungs. The sibling definition ml_stellar is the noncomputable real φ raised to a tier scaffold that the module notes has already been shown equal to φ.
proof idea
Term-mode proof. The tactic intro binds the negation assumption ml_stellar ≠ φ; exact then feeds the equality supplied by H_StellarML into that assumption to obtain False.
why it matters
The theorem supplies the falsifiability gate for the main stellar-assembly claim that M/L lies on the φ-ladder with typical value ≈ φ. It directly implements the module’s stated test protocol (galactic M/L surveys across age and metallicity) and closes the loop on the Recognition Composition Law applied to emission versus storage events. No downstream theorems yet depend on it; the open empirical question remains whether observed ratios remain inside the predicted [0.5, 5] solar-unit band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.