phi_13_bounds
The bound φ¹³ < 550 shows that the thirteenth power of the golden ratio lies below the upper limit of observed galaxy mass-to-light ratios. Researchers deriving M/L from recognition costs would cite this result to place φ-powers inside the empirical window 100-550. The proof reduces the claim via unfolding, bounds φ below 1.62 using a square-root estimate, lifts the inequality by monotonicity of exponentiation, and closes with direct numerical comparison plus order transitivity.
claim$φ^{13} < 550$, where $φ$ is the golden ratio arising as the self-similar fixed point.
background
In the Mass-to-Light module the ratio M/L is obtained as a power of the golden ratio φ that emerges from the forcing chain. The auxiliary definition phi_power(n) simply returns φ raised to the integer n and supplies the candidate values checked against observations. This construction sits inside the ledger-based derivation that treats M/L as an output of recognition-cost minimization rather than an external parameter.
proof idea
The tactic proof first unfolds phi_power to obtain the concrete inequality φ¹³ < 550. It then proves φ < 1.62 by unfolding the definition of φ, applying norm_num, and inserting a verified bound on √5. The base inequality is raised to the thirteenth power by the monotonicity lemma for positive exponents. Direct norm_num evaluation shows 1.62¹³ < 550, after which order transitivity finishes the argument.
why it matters in Recognition Science
The bound feeds the parent results ml_consistent_with_observation and ml_is_derived_not_input, which assert existence of an integer n in [10,13] such that the derived M/L lies inside the observed interval. It closes the Gap 10 derivation by confirming that φ¹³ remains below 550, thereby supporting the claim that all dimensionless ratios in the framework are algebraic in φ and consistent with the eight-tick octave and phi-ladder structure.
scope and limits
- Does not fix the exact integer n realized by any particular galaxy.
- Does not derive the numerical value of φ from more primitive axioms.
- Does not supply the matching lower bound φ¹⁰ > 100.
- Does not incorporate measurement error or selection effects in the M/L data.
formal statement (Lean)
107theorem phi_13_bounds : phi_power 13 < 550 := by
proof body
Tactic-mode proof.
108 unfold phi_power
109 have h : phi < 1.62 := by
110 unfold phi
111 norm_num
112 have : Real.sqrt 5 < 2.24 := by
113 rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.24)]
114 apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
115 linarith
116 have h13 : phi ^ 13 < 1.62 ^ 13 := pow_lt_pow_left h (by norm_num) (by norm_num)
117 have : (1.62 : ℝ) ^ 13 < 550 := by norm_num
118 exact lt_trans h13 this
119
120/-! ## Recognition Cost Derivation -/
121
122/-- M/L from recognition cost is a power of φ. -/