pith. machine review for the scientific record. sign in
theorem proved tactic proof high

cLag_lt_one_tenth

show as:
view Lean formalization →

The theorem shows that the lag coupling derived from the golden ratio satisfies phi to the negative fifth power less than one tenth. Researchers establishing perturbative validity for Recognition Science gravity models cite this bound to control the coupling product. The proof works by establishing phi at least 8/5, applying monotonicity of the negative power map, and verifying the numerical fact that (8/5) to the fifth exceeds 10.

claim$phi^{-5} < 1/10$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.

background

The module proves bounds on the ILG parameters alpha and C_lag that arise from Recognition Science. C_lag equals phi to the negative fifth power and originates from the coherence energy scale in the eight-tick resonance construction. The Constants structure supplies the numerical value of phi as the positive root of x squared minus x minus one equals zero. This lemma sits inside the parameter limits section that connects the Recognition Science spine to general relativity limits. Upstream, the definition cLag_from_phi pulls the constant from the Constants structure, while positivity facts come from rs_params_positive.

proof idea

The tactic script unfolds the definition of cLag_from_phi. It proves phi is at least 8/5 by showing that the standard expression for phi exceeds 8/5, using a contradiction argument on the square root of five. Real.rpow_le_rpow_of_nonpos then gives the power inequality for the negative exponent. The right side is rewritten as the reciprocal of (8/5) to the fifth, and norm_num confirms that this fifth power equals 32768/3125 which is greater than 10. Transitivity of less-than closes the claim.

why it matters in Recognition Science

This bound is invoked by cLag_lt_one to reach C_lag less than one and by rs_params_perturbative_proven to establish that the absolute value of the product alpha times C_lag is less than 0.1. It directly supports the module claim that the parameters are small enough for perturbative treatment. The result rests on the eight-tick resonance definition of the lag constant and the forcing chain's fixation of phi. It leaves the tighter product bound below 0.02 open, as noted in the downstream coupling_product_small_proven.

scope and limits

Lean usage

have hC_lt : cLag_from_phi < 1 / 10 := cLag_lt_one_tenth

formal statement (Lean)

  93theorem cLag_lt_one_tenth : cLag_from_phi < 1 / 10 := by

proof body

Tactic-mode proof.

  94  -- Use φ ≥ 8/5 and negative exponent monotonicity: φ^(−5) ≤ (8/5)^(−5) = 3125/32768 < 1/10
  95  unfold cLag_from_phi
  96  have hphi_ge : (8 : ℝ) / 5 ≤ Constants.phi := le_of_lt (by
  97    -- φ > 8/5
  98    unfold Constants.phi
  99    have hy : 0 ≤ (11 : ℝ) / 5 := by norm_num
 100    have hnot_le : ¬ (Real.sqrt 5 ≤ (11 : ℝ) / 5) := by
 101      have hcontra : ¬ (5 : ℝ) ≤ ((11 : ℝ) / 5) ^ 2 := by norm_num
 102      exact fun hle => hcontra ((Real.sqrt_le_left hy).mp hle)
 103    have h11lt : (11 : ℝ) / 5 < Real.sqrt 5 := lt_of_not_ge hnot_le
 104    have hsum : 1 + (11 : ℝ) / 5 < 1 + Real.sqrt 5 := by linarith
 105    have hdiv : (1 + (11 : ℝ) / 5) / 2 < (1 + Real.sqrt 5) / 2 :=
 106      div_lt_div_of_pos_right hsum (by norm_num)
 107    have h8over5 : (8 : ℝ) / 5 = (1 + (11 : ℝ) / 5) / 2 := by norm_num
 108    have hphi : (1 + Real.sqrt 5) / 2 = Constants.phi := by simp [Constants.phi]
 109    simpa [h8over5, hphi] using hdiv)
 110  have hxpos : 0 < (8 : ℝ) / 5 := by norm_num
 111  have hmon : Constants.phi ^ ((-5) : ℝ) ≤ ((8 : ℝ) / 5) ^ ((-5) : ℝ) :=
 112    Real.rpow_le_rpow_of_nonpos hxpos hphi_ge (by norm_num)
 113  have hrpow : ((8 : ℝ) / 5) ^ ((-5) : ℝ) = 1 / ((8 : ℝ) / 5) ^ 5 := by
 114    rw [Real.rpow_neg (le_of_lt hxpos)]
 115    simp
 116  have hlt : 1 / ((8 : ℝ) / 5) ^ 5 < 1 / 10 := by
 117    -- since (8/5)^5 = 32768/3125 > 10
 118    have hpow : ((8 : ℝ) / 5) ^ 5 = (32768 : ℝ) / 3125 := by norm_num
 119    have hgt : ((8 : ℝ) / 5) ^ 5 > 10 := by simpa [hpow] using (by norm_num : (32768 : ℝ) / 3125 > 10)
 120    exact (div_lt_div_of_pos_left (by norm_num) (by norm_num) hgt)
 121  have : ((8 : ℝ) / 5) ^ ((-5) : ℝ) < 1 / 10 := by simpa [hrpow] using hlt
 122  exact lt_of_le_of_lt hmon this
 123
 124/-- PROVEN: C_lag < 1 (from φ^5 > 10 ⇒ φ^(−5) < 1/10 < 1). -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.