Encyclopedia Foundation Foundation Phi Forcing Unconditional Ratio Bound All
ARTICLE 3 claims 3 theorems
Foundation Phi Forcing Unconditional Ratio Bound All
A theorem about the golden ratio that holds for any positive sequence following a simple additive rule, with no extra assumptions.
The universal ratio bound
The golden ratio φ, approximately 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. A classical fact about such additive sequences is that the ratio of consecutive terms, 1/1, 2/1, 3/2, 5/3, 8/5, does not stay constant but settles down, approaching φ as the sequence grows. This behavior is generic: it happens for any starting pair of positive numbers, not just 1 and 1.
The theorem ratio_bound_all in the machine-checked library of formal theorems makes this convergence quantitative. It states that for any positive sequence s satisfying the adjacent additive recurrence s(n+2) = s(n+1) + s(n), the absolute difference between the ratio s(n+1)/s(n) and φ is bounded by a constant times (1/φ)ⁿ. The constant depends only on the first two ratios, not on n. Since 1/φ is about 0.618, this bound shrinks exponentially fast, giving a precise rate at which the ratios approach φ. The proof works by a contraction argument: the error at one step is at most the previous error divided by φ, so after n steps the error is at most the initial error times (1/φ)ⁿ.
This result matters because it removes a hidden assumption. Earlier derivations in the framework required the ladder of levels to be geometric, meaning all ratios exactly equal. The new theorem shows that geometricity is not a premise but a consequence: any additive ladder, geometric or not, has ratios that asymptotically become geometric with ratio φ. The Fibonacci ladder itself is not geometric, its ratios oscillate above and below φ, yet the bound still applies. This is the generic behavior of every additive posting ladder, for any positive seeds.
In Recognition Science, the sequence models a ledger, a discrete record of events, where each posted level composes its two predecessors. The recurrence expresses that composed work is the sum of posted work. The theorem proves that any such ledger, regardless of its starting values, has inter-level ratios converging to φ. This is the promoted version of the framework's T6 result: the golden ratio is the asymptotic ratio of every additive posting ladder, with no geometric-ladder input and no closure hypothesis.
The theorem does not claim that the recurrence itself is derived from the framework's kernel axioms. That derivation, from locality and binarity of the posting operation to the additive recurrence, remains a stated residual premise. The result here takes the recurrence as given and proves the convergence of ratios. It also does not claim that any particular sequence, such as the Fibonacci numbers, is the unique ladder; the bound applies to all positive sequences satisfying the recurrence. Finally, it does not assert that the ratios ever equal φ exactly, only that they approach it with the stated exponential bound.
THEOREM ratio_bound_all · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- All-n bound with a seed-covering constant: |r_n − φ| ≤ C·(1/φ)^n. -/
private theorem ratio_bound_all (hpos : ∀ n, 0 < s n) (hrec : ∀ n, s (n + 2) = s (n + 1) + s n)
(n : ℕ) :
|s (n + 1) / s n - phi|
≤ phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ n := by
have hp : 0 < phi := by linarith [one_lt_phi]
have hq : 0 ≤ (1:ℝ)/phi := by positivity
have hge1 : (1:ℝ) ≤ phi := by linarith [one_lt_phi]
rcases n with _ | k
· rw [pow_zero, mul_one]
calc |s 1 / s 0 - phi|
≤ |s 1 / s 0 - phi| + |s 2 / s 1 - phi| := by
linarith [abs_nonneg (s 2 / s 1 - phi)]
_ ≤ phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) := by
nth_rewrite 1 [← one_mul (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|)]
exact mul_le_mul_of_nonneg_right hge1 (by positivity)
· calc |s (k + 1 + 1) / s (k + 1) - phi|
≤ (1 / phi) ^ k * |s 2 / s 1 - phi| := ratio_bound hpos hrec k
_ ≤ phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ (k + 1) := by
rw [pow_succ']
have hφ : phi * (1 / phi) = 1 := by field_simp [ne_of_gt hp]
have e : phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * ((1 / phi) * (1 / phi) ^ k)
= (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ k := by
calc phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * ((1 / phi) * (1 / phi) ^ k)
= (phi * (1 / phi))
* ((|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ k) := by ring
_ = (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ k := by
rw [hφ, one_mul]
rw [e]
have hle : |s 2 / s 1 - phi|
≤ |s 1 / s 0 - phi| + |s 2 / s 1 - phi| := by
linarith [abs_nonneg (s 1 / s 0 - phi)]
rw [mul_comm ((1 / phi) ^ k) |s 2 / s 1 - phi|]
exact mul_le_mul_of_nonneg_right hle (pow_nonneg hq k)
THEOREM ratio_contract · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- 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_tendsto_phi · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- **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
What this page does not claim
The theorem does not derive the recurrence s(n+2) = s(n+1) + s(n) from the framework's kernel axioms. It does not claim that any particular sequence is the unique additive ladder. It does not assert that ratios ever equal φ exactly, only that they converge with the stated bound.
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:
- How does the framework derive the adjacent additive recurrence from its kernel axioms?
- What is the exact constant in the bound for a given starting pair of seeds?
- How does this asymptotic result relate to the exact golden-ratio rung in the T6 chain?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM ratio_bound_all · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- All-n bound with a seed-covering constant: |r_n − φ| ≤ C·(1/φ)^n. -/ private theorem ratio_bound_all (hpos : ∀ n, 0 < s n) (hrec : ∀ n, s (n + 2) = s (n + 1) + s n) (n : ℕ) : |s (n + 1) / s n - phi| ≤ phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ n := by have hp : 0 < phi := by linarith [one_lt_phi] have hq : 0 ≤ (1:ℝ)/phi := by positivity have hge1 : (1:ℝ) ≤ phi := by linarith [one_lt_phi] rcases n with _ | k · rw [pow_zero, mul_one] calc |s 1 / s 0 - phi| ≤ |s 1 / s 0 - phi| + |s 2 / s 1 - phi| := by linarith [abs_nonneg (s 2 / s 1 - phi)] _ ≤ phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) := by nth_rewrite 1 [← one_mul (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|)] exact mul_le_mul_of_nonneg_right hge1 (by positivity) · calc |s (k + 1 + 1) / s (k + 1) - phi| ≤ (1 / phi) ^ k * |s 2 / s 1 - phi| := ratio_bound hpos hrec k _ ≤ phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ (k + 1) := by rw [pow_succ'] have hφ : phi * (1 / phi) = 1 := by field_simp [ne_of_gt hp] have e : phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * ((1 / phi) * (1 / phi) ^ k) = (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ k := by calc phi * (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * ((1 / phi) * (1 / phi) ^ k) = (phi * (1 / phi)) * ((|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ k) := by ring _ = (|s 1 / s 0 - phi| + |s 2 / s 1 - phi|) * (1 / phi) ^ k := by rw [hφ, one_mul] rw [e] have hle : |s 2 / s 1 - phi| ≤ |s 1 / s 0 - phi| + |s 2 / s 1 - phi| := by linarith [abs_nonneg (s 1 / s 0 - phi)] rw [mul_comm ((1 / phi) ^ k) |s 2 / s 1 - phi|] exact mul_le_mul_of_nonneg_right hle (pow_nonneg hq k)For any positive sequence satisfying the adjacent additive recurrence s(n+2) = s(n+1) + s(n), the absolute difference between the ratio s(n+1)/s(n) and φ is bounded by a constant times (1/φ)ⁿ. ratio_bound_all · IndisputableMonolith/Foundation/PhiForcingUnconditional.leanTHEOREM ratio_contract · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- 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]The error at one step is at most the previous error divided by φ, giving a contraction factor of about 0.618 per step. ratio_contract · IndisputableMonolith/Foundation/PhiForcingUnconditional.leanTHEOREM ratio_tendsto_phi · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- **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 hAny positive sequence obeying the adjacent additive recurrence has inter-level ratio converging to φ, with no geometric ladder assumed. ratio_tendsto_phi · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean