phi_gt_three_halves
The golden ratio exceeds 3/2. This bound is invoked to confirm that the lag coupling C_lag equals phi to the minus five stays below one tenth, permitting perturbative expansions in the GR limit of Recognition Science. Researchers deriving alpha and C_lag from the phi-ladder would cite the result to justify small-coupling approximations. The tactic proof first obtains sqrt(5) greater than 11/5 by contradiction on the square, then chains three rational inequalities to reach 3/2 less than 8/5 less than phi.
claim$phi > 3/2$ where $phi = (1 + sqrt(5))/2$ is the golden ratio appearing in the Constants bundle.
background
The module proves that RS-derived parameters alpha equals (1 minus 1 over phi) over 2 and C_lag equals phi to the minus five remain small enough for perturbative GR limits. The Constants structure collects the core CPM quantities Knet, Cproj, Ceng, Cdisp with non-negativity on Knet. C_lag is defined directly as phi inverse to the fifth power and is stated to approximate 0.09. The local setting is the explicit verification that both alpha and C_lag lie below 1 and that their product lies below 0.1, as required by the source derivation of coherence energy.
proof idea
The tactic proof proceeds by contradiction: assume sqrt(5) is at most 11/5, derive that 5 is at most (11/5) squared, and obtain an immediate numerical falsehood. From the negation it extracts 11/5 less than sqrt(5) via lt_of_not_ge. Adding 1 to both sides, dividing by 2, and rewriting 8/5 as the left-hand side produces 8/5 less than phi. The final step applies lt_trans to the already-proven 3/2 less than 8/5.
why it matters in Recognition Science
The inequality supplies the elementary lower bound needed to discharge the claim that phi to the minus five is less than 1/10, which the module documentation lists as proven. It therefore feeds the sibling results rs_params_perturbative_proven and coupling_product_small_proven. Within the Recognition Science framework the bound anchors the self-similar fixed point phi (T6) before the eight-tick octave and the derivation of three spatial dimensions can be treated perturbatively.
scope and limits
- Does not establish any upper bound on phi.
- Does not address the J-cost function or the full forcing chain T0-T8.
- Does not prove the tighter product bound alpha times C_lag less than 0.02.
- Does not extend the inequality to complex or matrix-valued extensions of phi.
formal statement (Lean)
68theorem phi_gt_three_halves : Constants.phi > 3 / 2 := by
proof body
Tactic-mode proof.
69 -- First show √5 > 11/5, hence φ = (1+√5)/2 > (1+11/5)/2 = 8/5 > 3/2
70 have hy : 0 ≤ (11 : ℝ) / 5 := by norm_num
71 have hnot_le : ¬ (Real.sqrt 5 ≤ (11 : ℝ) / 5) := by
72 -- If √5 ≤ 11/5 then 5 ≤ (11/5)^2, contradiction
73 have hcontra : ¬ (5 : ℝ) ≤ ((11 : ℝ) / 5) ^ 2 := by norm_num
74 exact fun hle => hcontra ((Real.sqrt_le_left hy).mp hle)
75 have h11lt : (11 : ℝ) / 5 < Real.sqrt 5 := lt_of_not_ge hnot_le
76 have hsum : 1 + (11 : ℝ) / 5 < 1 + Real.sqrt 5 := by linarith
77 have hdiv : (1 + (11 : ℝ) / 5) / 2 < (1 + Real.sqrt 5) / 2 :=
78 div_lt_div_of_pos_right hsum (by norm_num)
79 have h8over5 : (8 : ℝ) / 5 = (1 + (11 : ℝ) / 5) / 2 := by norm_num
80 have hphi : (1 + Real.sqrt 5) / 2 = Constants.phi := by simp [Constants.phi]
81 have h8ltphi : (8 : ℝ) / 5 < Constants.phi := by
82 simpa [h8over5, hphi] using hdiv
83 have : (3 : ℝ) / 2 < (8 : ℝ) / 5 := by norm_num
84 exact lt_trans this h8ltphi
85
86-- φ^2 = φ + 1 (reference)
87
88-- φ^5 = 5φ + 3 (reference)
89
90-- φ^5 > 10 (reference); not needed since we bound C_lag via rpow monotonicity
91
92/-- PROVEN: φ^(-5) < 1/10. -/