ml_consistent_with_observation
The theorem shows there exists an integer n between 10 and 13 such that phi raised to n lies strictly between 100 and 550. Recognition Science cosmologists cite it to confirm that the derived mass-to-light ratio matches galaxy cluster observations without external tuning. The proof selects n=10 explicitly, invokes the pre-established bounds on phi^10 and phi^13, and chains them via order transitivity.
claimThere exists an integer $n$ satisfying $10 ≤ n ≤ 13$ such that $100 < φ^n < 550$, where $φ$ is the golden ratio and $φ^n$ denotes its integer power.
background
The module derives the mass-to-light ratio from recognition-weighted stellar assembly on the ledger, showing it equals a power of phi rather than an external input. phi_power is the definition that maps each integer n to the real number phi raised to n, supplying the candidate M/L values. The local setting addresses the objection that observed M/L ≈ 100-500 must be inserted by hand; instead the phi-ladder produces exactly the interval phi^10 to phi^13. Upstream, phi_10_bounds states phi^10 > 100 and phi_13_bounds states phi^13 < 550, both obtained by comparing phi to 1.6 and 1.62 and applying elementary power inequalities.
proof idea
The tactic proof begins by supplying the witness 10. It then splits the conjunction, confirms membership in the closed interval [10,13] by simplification, and applies the theorem phi_10_bounds directly. For the upper bound it introduces the auxiliary inequality phi_power 10 < phi_power 13 via zpow_lt_zpow_of_one_lt (using phi_gt_one), then chains this with phi_13_bounds through the lemma lt_trans.
why it matters in Recognition Science
This result closes the empirical-consistency step in the Gap 10 derivation, confirming that the phi-ladder values sit inside the observed M/L window 100-550. It supports the broader claim that all dimensionless ratios in Recognition Science are algebraic in phi, analogous to the fine-structure constant and the particle mass ladder. No downstream theorems yet depend on it, leaving open the question of whether a unique n is selected by further ledger constraints.
scope and limits
- Does not prove that M/L equals exactly phi^10 rather than another power in the interval.
- Does not derive the numerical value of M/L from first principles; only shows numerical consistency.
- Does not address scatter or redshift dependence in observed M/L ratios.
- Does not rule out other functional forms that might also fit the same interval.
formal statement (Lean)
204theorem ml_consistent_with_observation :
205 ∃ n : ℤ, n ∈ Set.Icc 10 13 ∧
206 -- The derived value φⁿ falls within observed range (100-550)
207 (phi_power n > 100) ∧ (phi_power n < 550) := by
proof body
Tactic-mode proof.
208 use 10
209 constructor
210 · simp [Set.mem_Icc]
211 constructor
212 · exact phi_10_bounds
213 · -- phi^10 < phi^13 < 550
214 have h : phi_power 10 < phi_power 13 := by
215 unfold phi_power
216 apply zpow_lt_zpow_of_one_lt phi_gt_one (by norm_num)
217 exact lt_trans h phi_13_bounds
218
219/-! ## Main Theorem: M/L is Derived, Not Input -/
220