phi_bounds
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 in Recognition Science
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)).
scope and limits
- Does not tighten the interval beyond 1 < φ < 2.
- Does not derive the value of φ from the Recognition Composition Law.
- Does not incorporate observational error bars on M/L.
- Does not extend to composite stellar populations.
Lean usage
have hphi := phi_boundsformal statement (Lean)
133theorem phi_bounds : 1 < φ ∧ φ < 2 := by
proof body
Tactic-mode proof.
134 constructor
135 · -- 1 < φ: Since √5 > 1, we have (1 + √5)/2 > 1
136 unfold φ Constants.phi
137 have h_sqrt5_gt_1 : 1 < Real.sqrt 5 := by
138 rw [show (1 : ℝ) = Real.sqrt 1 by norm_num]
139 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
140 linarith
141 · -- φ < 2: Since √5 < 3, we have (1 + √5)/2 < 2
142 unfold φ Constants.phi
143 have h_sqrt5_lt_3 : Real.sqrt 5 < 3 := by
144 rw [show (3 : ℝ) = Real.sqrt 9 by norm_num]
145 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
146 linarith
147
148/-- The derived M/L is in the observed range [0.5, 5] solar units.
149 Proof depends on the axiom ml_derived_value : ml_derived = φ. -/