phi_bounds
plain-language theorem explainer
Golden ratio bounds 1 < φ < 2 anchor the mass-to-light derivation at φ solar units. Stellar astrophysicists and gap calculators in electron mass cite it for interval arithmetic on the phi-ladder. The tactic proof splits the conjunction and reduces each side to sqrt(5) comparisons via linarith.
Claim. $1 < φ ∧ φ < 2$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The MassToLight module unifies three derivations of the stellar mass-to-light ratio M/L from Recognition Science. Strategy 1 weights photon emission against mass storage by J-cost differentials, yielding M/L = φ^n. Strategy 2 uses discrete φ-tiers in nucleosynthesis. Strategy 3 invokes geometric observability limits from λ_rec, τ_0, E_coh. All converge on M/L = φ ≈ 1.618 solar units, with discrete range {1, φ, φ², φ³} inside the observed [0.5, 5].
proof idea
Constructor splits the conjunction. The lower bound unfolds φ, invokes sqrt(5) > 1 by comparing squares of 1 and 5, then linarith. The upper bound repeats the pattern with sqrt(5) < 3. No external lemmas beyond Real.sqrt_lt_sqrt and norm_num are required.
why it matters
Downstream lemmas gap_1332_bounds and log_phi_bounds in ElectronMass.Necessity import this bound to control gap(1332) and log(φ) intervals. GapProperties in RSBridge likewise depends on it for gap(24) and gap(276). The module doc states that with M/L derived, Recognition Science reaches true zero-parameter status. It realizes the phi-ladder step in the mass formula yardstick * φ^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.