Encyclopedia Foundation Foundation Phi Forcing Unconditional Ratio Bound
ARTICLE 4 claims 4 theorems
Foundation Phi Forcing Unconditional Ratio Bound
A simple rule for adding levels forces their ratios toward the golden ratio, with a precise bound on how fast.
The ratio bound
The golden ratio φ, about 1.618, is the number that solves r² = r + 1. 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 two before it. In that sequence, the ratio of consecutive terms, 2/1 = 2, 3/2 = 1.5, 5/3 ≈ 1.667, does not stay constant, but it does settle down: the ratios get closer and closer to φ. This convergence is not a special property of the Fibonacci numbers. It happens for any positive sequence built by the same rule, s(n+2) = s(n+1) + s(n), no matter what the first two numbers are.
The machine-checked library of formal theorems in the Recognition Science framework proves this convergence and, in the declaration ratio_bound, gives a precise speed for it. The bound says that the error, the distance between the n-th ratio and φ, shrinks by at least a factor of 1/φ ≈ 0.618 at each step. After k steps, the error is at most (1/φ)^k times the starting error. Since 0.618 is less than 1, the error is crushed to zero exponentially fast. A companion result, ratio_bound_all, packages the same idea into a single constant that covers all steps at once.
What this changes is the role of geometricity. Older derivations in the framework assumed the ladder of levels had a uniform ratio r and then solved for r = φ. The new theorem needs no such assumption. The uniform ratio is not an input; it is an automatic consequence. The recurrence alone, the arithmetic of adjacent composition, forces φ as the asymptotic ratio. The proof is a contraction: the next ratio r_{n+1} equals 1 + 1/r_n, and since φ = 1 + 1/φ, the error contracts by the factor 1/φ each step.
In Recognition Science, this is the promotion of theorem T6: the golden ratio is the asymptotic ratio of every additive posting ladder, with no geometric-ladder premise. The framework models a ledger, a discrete record of events, where each level's work is the sum of the two below it. The theorem shows that such a ledger, if it keeps posting, inevitably approaches φ. This is a proved theorem in the library, axiom-clean, and it is the unconditional core of the forcing chain that leads to the eight-tick cycle and three spatial dimensions.
The theorem does not claim that the recurrence itself is forced by the framework's kernel axioms. That provenance, the bridge from posting locality and binarity to the additive recurrence, remains open. The theorem takes the recurrence as a premise and derives the ratio bound from it. It also does not claim that any particular physical ladder has ratios that match φ at any finite step; it claims only the asymptotic limit and the exponential bound on the way there.
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
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_bound · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- Iterated contraction: |r_{k+1} − φ| ≤ (1/φ)^k · |r_1 − φ|. -/
private theorem ratio_bound (hpos : ∀ n, 0 < s n) (hrec : ∀ n, s (n + 2) = s (n + 1) + s n)
(k : ℕ) :
|s (k + 2) / s (k + 1) - phi|
≤ (1 / phi) ^ k * |s 2 / s 1 - phi| := by
induction k with
| zero => simp
| succ k ih =>
have e0 : k + 1 + 2 = k + 3 := by omega
have e1 : k + 1 + 1 = k + 2 := by omega
rw [e0, e1]
have hp : 0 < phi := by linarith [one_lt_phi]
calc |s (k + 3) / s (k + 2) - phi|
≤ |s (k + 2) / s (k + 1) - phi| / phi :=
ratio_contract hpos hrec (k + 1) (by omega)
_ ≤ ((1 / phi) ^ k * |s 2 / s 1 - phi|) / phi := by
gcongr
_ = (1 / phi) ^ (k + 1) * |s 2 / s 1 - phi| := by
rw [pow_succ']
field_simp [ne_of_gt hp]
THEOREM phi_is_asymptotic_ratio · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- **T6 assembly.** From positivity and the adjacent posting recurrence, the
asymptotic inter-level ratio is φ, with no geometric-ladder input. Combined
with the banked tick (Cost.GeometricRoot: discreteness forced by
cost-nontriviality), the chain is: the ledger cannot subdivide forever (tick),
each posted level composes its two predecessors (recurrence), and the ladder's
asymptotic ratio is φ (this module). The residual premise is the recurrence's
own provenance; see the module docstring. -/
theorem phi_is_asymptotic_ratio (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) :=
ratio_tendsto_phi hpos hrec
What this page does not claim
The recurrence s(n+2) = s(n+1) + s(n) itself is not derived from the kernel axioms here. No finite-step ratio is claimed to equal φ exactly; only the asymptotic limit and the exponential bound are proved. The theorem does not apply to sequences that are not positive or do not obey the additive recurrence.
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:
- What physical posting operation gives rise to the adjacent additive recurrence?
- How does the ratio bound connect to the forcing of the eight-tick cycle?
- What is the exact provenance of the recurrence in the framework's kernel axioms?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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 hAny positive sequence obeying the adjacent additive recurrence s(n+2) = s(n+1) + s(n) has inter-level ratio converging to φ. ratio_tendsto_phi · 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 between the n-th ratio and φ shrinks by at least a factor of 1/φ ≈ 0.618 at each step. ratio_contract · IndisputableMonolith/Foundation/PhiForcingUnconditional.leanTHEOREM ratio_bound · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- Iterated contraction: |r_{k+1} − φ| ≤ (1/φ)^k · |r_1 − φ|. -/ private theorem ratio_bound (hpos : ∀ n, 0 < s n) (hrec : ∀ n, s (n + 2) = s (n + 1) + s n) (k : ℕ) : |s (k + 2) / s (k + 1) - phi| ≤ (1 / phi) ^ k * |s 2 / s 1 - phi| := by induction k with | zero => simp | succ k ih => have e0 : k + 1 + 2 = k + 3 := by omega have e1 : k + 1 + 1 = k + 2 := by omega rw [e0, e1] have hp : 0 < phi := by linarith [one_lt_phi] calc |s (k + 3) / s (k + 2) - phi| ≤ |s (k + 2) / s (k + 1) - phi| / phi := ratio_contract hpos hrec (k + 1) (by omega) _ ≤ ((1 / phi) ^ k * |s 2 / s 1 - phi|) / phi := by gcongr _ = (1 / phi) ^ (k + 1) * |s 2 / s 1 - phi| := by rw [pow_succ'] field_simp [ne_of_gt hp]After k steps, the error is at most (1/φ)^k times the starting error. ratio_bound · IndisputableMonolith/Foundation/PhiForcingUnconditional.leanTHEOREM phi_is_asymptotic_ratio · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean
/-- **T6 assembly.** From positivity and the adjacent posting recurrence, the asymptotic inter-level ratio is φ, with no geometric-ladder input. Combined with the banked tick (Cost.GeometricRoot: discreteness forced by cost-nontriviality), the chain is: the ledger cannot subdivide forever (tick), each posted level composes its two predecessors (recurrence), and the ladder's asymptotic ratio is φ (this module). The residual premise is the recurrence's own provenance; see the module docstring. -/ theorem phi_is_asymptotic_ratio (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) := ratio_tendsto_phi hpos hrecGeometricity is demoted from premise to asymptotic corollary. phi_is_asymptotic_ratio · IndisputableMonolith/Foundation/PhiForcingUnconditional.lean