Encyclopedia Foundation Foundation Phi Forcing Unconditional Ratio Sub Phi

ARTICLE 3 claims 3 theorems

Foundation Phi Forcing Unconditional Ratio Sub Phi

A single algebraic identity shows why the golden ratio emerges from any sequence built by adding consecutive terms, no matter how it starts.

Verify this page

The contraction step

The golden ratio φ, about 1.618, is the number that solves r² = r + 1, or equivalently r = 1 + 1/r. It appears throughout mathematics, from the regular pentagon to the Fibonacci sequence 1, 1, 2, 3, 5, 8, where each term is the sum of the previous two. The ratios of consecutive Fibonacci numbers, 1, 2, 1.5, 1.667, are not constant, but they settle down: they approach φ. This is not a special property of the Fibonacci seeds. Any positive sequence that follows the same rule, s(n+2) = s(n+1) + s(n), has consecutive ratios that converge to φ, regardless of the two starting values.

The proof rests on a single algebraic step. Write r_n for the ratio s(n+1)/s(n). The recurrence gives r_{n+1} = 1 + 1/r_n. Since φ itself satisfies φ = 1 + 1/φ, subtracting the two equations yields r_{n+1} − φ = 1/r_n − 1/φ = (φ − r_n)/(r_n·φ). For n ≥ 1, every ratio r_n is at least 1, so the error contracts by a factor of 1/φ, about 0.618, at each step. Repeating this contraction forces the ratios toward φ exponentially fast.

In Recognition Science, this result carries the name ratio_sub_phi. The framework models reality as a ledger, a discrete record of events, and the theorem belongs to a chain that derives the golden ratio as the asymptotic ratio of any additive posting ladder. The key point is that the uniform ratio assumption, once a premise, is now a corollary: the ladder need not be geometric for φ to emerge. The recurrence alone, with positivity, forces the limit.

The theorem is machine-checked in the framework's library of formal theorems. Its assumptions are exactly two: every term is positive, and each term is the sum of the two before it. It does not claim that the recurrence itself is derived from more basic principles, nor that the golden ratio appears at any finite level. It establishes only the asymptotic behavior, the limit toward which the ratios tend, not the value of any particular ratio.

THEOREM ratio_tendsto_phi · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
ratio_tendsto_phi · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean:166 
/-- **T6, promoted: the golden ratio is the asymptotic ratio of every additive
posting ladder.** Any positive sequence obeying the adjacent additive
recurrence s(n+2) = s(n+1) + s(n) has inter-level ratio converging to φ.
No geometric ladder, no uniform ratio, and no closure hypothesis is assumed:
geometricity is demoted from premise to asymptotic corollary. -/
theorem ratio_tendsto_phi (hpos : ∀ n, 0 < s n)
    (hrec : ∀ n, s (n + 2) = s (n + 1) + s n) :
    Tendsto (fun n => s (n + 1) / s n) atTop (nhds phi) := by
  have hp : 0 < phi := by linarith [one_lt_phi]
  have hq0 : 0 ≤ (1:ℝ) / phi := by positivity
  have hq1 : (1:ℝ) / phi < 1 := by
    rw [div_lt_one hp]; exact one_lt_phi
  set C := phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) with hC
  have hbound : ∀ n, |s (n + 1) / s n - phi| ≤ C * (1 / phi) ^ n := fun n =>
    ratio_bound_all hpos hrec n
  have htend : Tendsto (fun n => C * (1 / phi) ^ n) atTop (nhds 0) := by
    have h := (tendsto_pow_atTop_nhds_zero_of_lt_one hq0 hq1).const_mul C
    simpa using h
  have habs : Tendsto (fun n => |s (n + 1) / s n - phi|) atTop (nhds 0) :=
    squeeze_zero (fun n => abs_nonneg _) hbound htend
  have hsub : Tendsto (fun n => s (n + 1) / s n - phi) atTop (nhds 0) := by
    have hneg : Tendsto (fun n => -|s (n + 1) / s n - phi|) atTop (nhds 0) := by
      have h := habs.neg
      simpa using h
    exact tendsto_of_tendsto_of_tendsto_of_le_of_le hneg habs
      (fun n => neg_abs_le _) (fun n => le_abs_self _)
  have h : Tendsto (fun n => (s (n + 1) / s n - phi) + phi) atTop (nhds (0 + phi)) :=
    hsub.add tendsto_const_nhds
  simpa using h
THEOREM ratio_contract · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
ratio_contract · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean:88 
/-- Contraction: |r_{n+1} − φ| ≤ |r_n − φ| / φ for n ≥ 1 (since r_n ≥ 1). -/
private theorem ratio_contract (hpos : ∀ n, 0 < s n) (hrec : ∀ n, s (n + 2) = s (n + 1) + s n)
    (n : ℕ) (hn : 1 ≤ n) :
    |s (n + 2) / s (n + 1) - phi| ≤ |s (n + 1) / s n - phi| / phi := by
  have hr : 0 < s (n + 1) / s n := div_pos (hpos _) (hpos _)
  have hp : 0 < phi := by linarith [one_lt_phi]
  have h1 : s (n + 1) / s n ≠ 0 := ne_of_gt hr
  have h2 : phi ≠ 0 := ne_of_gt hp
  rw [ratio_sub_phi hpos hrec n]
  have hident : 1 / (s (n + 1) / s n) - 1 / phi
      = (phi - s (n + 1) / s n) / ((s (n + 1) / s n) * phi) := by
    have hn1 : s (n + 1) ≠ 0 := ne_of_gt (hpos _)
    have hn0 : s n ≠ 0 := ne_of_gt (hpos _)
    field_simp [h1, h2, hn1, hn0]
  rw [hident, abs_div, abs_mul, abs_of_pos hr, abs_of_pos hp,
    show phi - s (n + 1) / s n = -(s (n + 1) / s n - phi) from by ring, abs_neg]
  gcongr
  have hn1 : 1 ≤ s (n + 1) / s n := by
    obtain ⟨k, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
    simpa using ratio_ge_one hpos hrec k
  nlinarith [hn1, hp]
THEOREM ratio_sub_phi · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
ratio_sub_phi · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean:80 
/-- The key identity: r_{n+1} − φ = 1/r_n − 1/φ. -/
private theorem ratio_sub_phi (hpos : ∀ n, 0 < s n) (hrec : ∀ n, s (n + 2) = s (n + 1) + s n)
    (n : ℕ) :
    s (n + 2) / s (n + 1) - phi = 1 / (s (n + 1) / s n) - 1 / phi := by
  have h : (1 : ℝ) - phi = -(1 / phi) := by linarith [phi_fixed]
  rw [ratio_succ hpos hrec n]
  linarith [h]

What this page does not claim

The recurrence itself is not derived within this theorem; it is taken as a premise. The golden ratio is not claimed to appear at any finite level, only as a limit. The theorem does not require or assume a geometric ladder with a uniform ratio.

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/Foundation/PhiForcingUnconditional.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