Encyclopedia Numerics Numerics Interval W8 Bounds Phi Lt 16180340

ARTICLE 4 claims 4 theorems

Numerics Interval W8 Bounds Phi Lt 16180340

A machine-checked proof pins the golden ratio below 1.6180340, a decimal bound that later numerical work depends on.

Verify this page

The upper bound for phi

The golden ratio, usually written φ, is the positive solution of the equation r² = r + 1, which gives φ = (1 + √5)/2 ≈ 1.6180339887. The declaration phi_lt_16180340 in the framework's machine-checked library of formal theorems establishes that φ is strictly less than the decimal number 1.6180340. This is a rigorous upper bound, not a rounding convention: the proof verifies that the square of 2.236068 exceeds 5, so √5 lies below 2.236068, and therefore (1 + √5)/2 falls under 1.6180340.

The bound is one of a pair of interval constraints on φ. A companion theorem phi_gt_161803395 proves φ is greater than 1.61803395, so together they confine φ to a narrow window of width 0.00000005. The framework uses these tight bounds as inputs for further numerical work, such as computing the gap weight w8_from_eight_tick, a parameter-free closed form approximately equal to 2.490569. That weight appears in the framework's eight-tick recognition cycle, where the cost of recognition is forced by a proved functional equation.

In Recognition Science, the golden ratio is not merely a classical constant; the framework proves it is the unique self-similar scaling forced by the cost function J(x) = (x + 1/x)/2 - 1. The bound phi_lt_16180340 supports that structural role by giving a precise decimal handle on φ for interval arithmetic. What the declaration does not claim is any physical measurement, any new property of φ, or any statement about the fine-structure constant. It is purely a numerical inequality about a real number, established by elementary algebra in the machine-checked library.

THEOREM phi_lt_16180340 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
phi_lt_16180340 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:47 
/-- Upper decimal bound for φ. -/
theorem phi_lt_16180340 : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := by
  have hx : (0 : ℝ) ≤ (5 : ℝ) := by norm_num
  have hy : (0 : ℝ) ≤ (2.236068 : ℝ) := by norm_num
  have hsq : (5 : ℝ) < (2.236068 : ℝ) ^ 2 := by norm_num
  have hsqrt : Real.sqrt 5 < (2.236068 : ℝ) := by
    exact (Real.sqrt_lt hx hy).2 hsq
  unfold IndisputableMonolith.Constants.phi
  linarith
THEOREM phi_lt_16180340 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
phi_lt_16180340 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:47 
/-- Upper decimal bound for φ. -/
theorem phi_lt_16180340 : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := by
  have hx : (0 : ℝ) ≤ (5 : ℝ) := by norm_num
  have hy : (0 : ℝ) ≤ (2.236068 : ℝ) := by norm_num
  have hsq : (5 : ℝ) < (2.236068 : ℝ) ^ 2 := by norm_num
  have hsqrt : Real.sqrt 5 < (2.236068 : ℝ) := by
    exact (Real.sqrt_lt hx hy).2 hsq
  unfold IndisputableMonolith.Constants.phi
  linarith
THEOREM phi_gt_161803395 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
phi_gt_161803395 · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:38 
/-- Lower decimal bound for φ. -/
theorem phi_gt_161803395 : (1.61803395 : ℝ) < IndisputableMonolith.Constants.phi := by
  have hx : (0 : ℝ) ≤ (2.2360679 : ℝ) := by norm_num
  have hsq : (2.2360679 : ℝ) ^ 2 < (5 : ℝ) := by norm_num
  have hsqrt : (2.2360679 : ℝ) < Real.sqrt 5 := by
    exact (Real.lt_sqrt hx).2 hsq
  unfold IndisputableMonolith.Constants.phi
  linarith
THEOREM w8_computed_gt · IndisputableMonolith/Numerics/Interval/W8Bounds.lean
w8_computed_gt · IndisputableMonolith/Numerics/Interval/W8Bounds.lean:57 
/-- The gap weight is greater than 2.490564399. -/
theorem w8_computed_gt : (2.490564399 : ℝ) < IndisputableMonolith.Constants.w8_from_eight_tick := by
  -- w8 = (348 + 210√2 - (204 + 130√2)φ)/7
  have hs2_hi : Real.sqrt 2 ≤ (1.4143 : ℝ) := le_of_lt sqrt2_lt_14143
  have hφ_hi : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := phi_lt_16180340

  -- Step 1: replace φ by its upper bound (expression decreases as φ increases).
  have h_phi_step :
      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) / 7
        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7 := by
    have hA : 0 ≤ (204 : ℝ) + 130 * Real.sqrt 2 := by
      have : (0 : ℝ) ≤ Real.sqrt 2 := Real.sqrt_nonneg 2
      nlinarith
    have hmul :
        -((204 : ℝ) + 130 * Real.sqrt 2) * (1.6180340 : ℝ)
          ≤ -((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi := by
      have hnegA : -((204 : ℝ) + 130 * Real.sqrt 2) ≤ 0 := by linarith
      -- phi ≤ 1.6180340 and the coefficient is nonpositive, so inequality flips.
      exact mul_le_mul_of_nonpos_left hφ_hi.le hnegA
    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
    have hnum :
        (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * (1.6180340 : ℝ)
          ≤ (348 : ℝ) + 210 * Real.sqrt 2 - ((204 : ℝ) + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi := by
      linarith [hmul]
    exact (div_le_div_of_nonneg_right hnum (le_of_lt h7))

  -- Step 2: with φ fixed at its max, the expression decreases in √2 because (210 - 130φ) < 0.
  have hcoeff_neg : (210 : ℝ) - 130 * (1.6180340 : ℝ) < 0 := by norm_num
  have h_s2_step :
      (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7
        ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) / 7 := by
    have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
    -- Rewrite numerator as `A + √2 * B` where `B < 0`, so replacing √2 by its upper bound
    -- gives a *lower* value (hence a lower corner bound).
    set B : ℝ := (210 : ℝ) - 130 * (1.6180340 : ℝ)
    have hB : B ≤ 0 := by
      have : B < 0 := by simpa [B] using hcoeff_neg
      exact le_of_lt this
    have hs2_term : (1.4143 : ℝ) * B ≤ Real.sqrt 2 * B := by
      have hs : Real.sqrt 2 ≤ (1.4143 : ℝ) := hs2_hi
      exact mul_le_mul_of_nonpos_right hs hB
    have hnum_raw :
        (348 : ℝ) - 204 * (1.6180340 : ℝ) + (1.4143 : ℝ) * B
          ≤ (348 : ℝ) - 204 * (1.6180340 : ℝ) + Real.sqrt 2 * B := by
      linarith [hs2_term]
    have hrewL :
        (348 : ℝ) - 204 * (1.6180340 : ℝ) + (1.4143 : ℝ) * B
          = (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) := by
      simp [B]
      ring
    have hrewR :
        (348 : ℝ) - 204 * (1.6180340 : ℝ) + Real.sqrt 2 * B
          = (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) := by
      simp [B]
      ring
    have hnum' :
        (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ))
          ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * (1.6180340 : ℝ)) := by
      simpa [hrewL, hrewR] using hnum_raw
    exact (div_le_div_of_nonneg_right hnum' (le_of_lt h7))

  -- Combine the steps.
  have hw8_corner :
      (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7
        ≥ (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7 :=
    -- corner ≤ (φ_hi,sqrt2) ≤ (φ,sqrt2)
    show (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7
          ≤ (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * IndisputableMonolith.Constants.phi) / 7 from
      le_trans h_s2_step h_phi_step

  -- Now the numeric corner value is > 2.490564399.
  have hcorner_gt :
      (2.490564399 : ℝ) <
        (348 + 210 * (1.4143 : ℝ) - (204 + 130 * (1.4143 : ℝ)) * (1.6180340 : ℝ)) / 7 := by
    norm_num

  -- Finish by unfolding w8 and chaining inequalities.
  unfold IndisputableMonolith.Constants.w8_from_eight_tick
  exact lt_of_lt_of_le hcorner_gt hw8_corner

What this page does not claim

The declaration does not claim any physical measurement or empirical value for φ. The declaration does not establish any new mathematical property of φ beyond the numerical inequality. The declaration does not state anything about the fine-structure constant α.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Numerics/Interval/W8Bounds.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND