Foundation Recurrence Bridge Closure Gives Recurrence Upper Bound

The upper bound from closure

Consider a ladder of positive numbers, each rung larger than the last. The classical Fibonacci sequence is the familiar example: 1, 1, 2, 3, 5, 8, where each number is the sum of the two previous ones. This page concerns a more general question: what if we only know that each new rung is the sum of the two immediately below it, but we do not yet know that this sum is exactly the next rung? The answer is a simple inequality: the next rung cannot be larger than the sum of the two below it. This is the upper bound.

In the Recognition Science framework, this fact is a proved theorem named closure_gives_recurrence_upper_bound. The framework models a ledger, a discrete record of events, where each rung represents the size of a recognized object. The relevant operation is adjacent closure, the rule that combining two neighboring rungs always produces another rung somewhere higher on the ladder. The theorem states that if the ladder is monotone (each rung is at least as large as the one before) and adjacent closure holds, then the rung at position n+2 is at most the sum of the rungs at n and n+1. The proof is a short argument: the composition of rungs n and n+1 is some rung m at or above n+2; since the ladder is monotone, rung n+2 is no larger than rung m, which equals the sum.

This upper bound is one half of the full recurrence. The other half, the lower bound, requires an additional premise: a per-rung ratio floor above the plastic constant. The plastic constant, about 1.3247, is the solution to the equation x³ = x + 1. The framework proves that if each step multiplies size by at least this ratio, then adjacent closure forces the exact recurrence s(n+2) = s(n+1) + s(n). The sharpness is exact: at the plastic constant itself, a ladder exists that satisfies the floor with equality and closure but violates the recurrence. The strict inequality cannot be relaxed.

What the upper-bound theorem does not do is establish the recurrence on its own. The framework provides a concrete counterexample: the integer ladder s(n) = n + 1. This ladder is strictly increasing, satisfies adjacent closure, and even has a constant step of 1, yet it fails the recurrence. It also admits no ratio floor above 1. This shows that closure plus generation plus an absolute minimum step, the form of a banked tick, do not force the recurrence. The ratio floor is genuine extra content, and it is exactly what the integer ladder lacks.

The practical consequence is a clean decomposition. The full recurrence splits into two named premises: the posting operation's locality (each new rung is the composition of its two immediate predecessors) and ledger additivity (composition size is the sum). When both hold, the framework proves the ratio of successive rungs converges to the golden ratio φ, about 1.618. This is the bridge that connects the abstract ledger to the appearance of φ in the framework's structure.

/-- Closure alone gives the recurrence's upper half for free: the next rung
never exceeds the composition of the two below it. -/
theorem closure_gives_recurrence_upper_bound
    (hmono : Monotone s)
    (hclosure : ∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) :
    ∀ n, s (n + 2) ≤ s (n + 1) + s n := by
  intro n
  obtain ⟨m, hm, hsm⟩ := hclosure n
  have h := hmono (by omega : n + 2 ≤ m)
  linarith [hsm, h]

/-- The countermodel, packaged: strict monotonicity, adjacent closure, full
generation, ledger additivity (composition is addition), and an absolute
minimum step of 1 all hold for the integer ladder, yet the adjacent
recurrence fails and no ratio floor above 1 exists. Closure + generation +
absolute tick (the banked tick's form) do not force the recurrence. -/
theorem closure_generation_tick_insufficient :
    ∃ s : ℕ → ℝ, StrictMono s ∧
      (∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) ∧
      (∀ n, n ≥ 2 → ∃ a b, a ≤ b ∧ b < n ∧ s n = s a + s b) ∧
      (∀ n, s (n + 1) - s n = 1) ∧
      ¬ (∀ n, s (n + 2) = s (n + 1) + s n) ∧
      (∀ ρ : ℝ, 1 < ρ → ∃ n, s (n + 1) < ρ * s n) :=
  ⟨intLadder, intLadder_strictMono, intLadder_adjacent_closure,
    intLadder_generation, intLadder_tick, intLadder_recurrence_fails,
    intLadder_no_ratio_floor⟩

/-- **The recurrence bridge.** A ratio floor ρ above the plastic constant
(ρ³ > ρ + 1), together with adjacent closure (the composition of rungs n and
n+1 is always a rung), forces the adjacent recurrence: the composition
cannot reach rung n+3, so it is rung n+2. -/
theorem recurrence_of_floor_above_plastic (hpos : ∀ n, 0 < s n)
    {ρ : ℝ} (hρ : 1 < ρ) (hρ3 : ρ + 1 < ρ ^ 3)
    (hfloor : ∀ n, ρ * s n ≤ s (n + 1))
    (hclosure : ∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) :
    ∀ n, s (n + 2) = s (n + 1) + s n := by
  have hmono := monotone_of_floor hpos hρ hfloor
  have hρpos : 0 < ρ := by linarith
  intro n
  obtain ⟨m, hm, hsm⟩ := hclosure n
  have hmle : m ≤ n + 2 := by
    by_contra h
    push_neg at h
    have hm3 : n + 3 ≤ m := by omega
    have hs3 : s (n + 3) ≤ s m := hmono hm3
    have hf2 : ρ ^ 2 * s (n + 1) ≤ s (n + 3) :=
      calc ρ ^ 2 * s (n + 1) = ρ * (ρ * s (n + 1)) := by ring
        _ ≤ ρ * s (n + 2) :=
          mul_le_mul_of_nonneg_left (hfloor (n + 1)) (le_of_lt hρpos)
        _ ≤ s (n + 3) := hfloor (n + 2)
    have hsn : s n ≤ s (n + 1) / ρ := by
      rw [le_div_iff₀ hρpos, mul_comm]
      exact hfloor n
    have hsp : 0 < s (n + 1) := hpos (n + 1)
    have h1 : ρ ^ 2 * s (n + 1) ≤ s n + s (n + 1) := by
      linarith [hs3, hf2, hsm]
    have h2 : s n + s (n + 1) ≤ s (n + 1) / ρ + s (n + 1) := by
      linarith [hsn]
    have h3 : ρ ^ 2 * s (n + 1) ≤ (1 / ρ + 1) * s (n + 1) := by
      have e : s (n + 1) / ρ + s (n + 1) = (1 / ρ + 1) * s (n + 1) := by ring
      rw [e] at h2
      exact le_trans h1 h2
    have h4 : ρ ^ 2 ≤ 1 / ρ + 1 := le_of_mul_le_mul_right h3 hsp
    have h5 : ρ ^ 2 * ρ ≤ (1 / ρ + 1) * ρ :=
      mul_le_mul_of_nonneg_right h4 (le_of_lt hρpos)
    have h6 : (1 / ρ + 1) * ρ = 1 + ρ := by field_simp [hρpos.ne']
    have h7 : ρ ^ 2 * ρ = ρ ^ 3 := by ring
    rw [h7] at h5
    rw [h6] at h5
    linarith [h5, hρ3]
  have hmeq : m = n + 2 := by omega
  subst hmeq
  linarith [hsm]

/-- **T6 assembly, bridge form.** A ratio floor above the plastic constant
plus adjacent closure forces the recurrence (this module), hence the
asymptotic inter-level ratio is φ (PhiForcingUnconditional). No geometric
ladder, no uniform ratio, no minimality posture. -/
theorem phi_of_floor_above_plastic (hpos : ∀ n, 0 < s n)
    {ρ : ℝ} (hρ : 1 < ρ) (hρ3 : ρ + 1 < ρ ^ 3)
    (hfloor : ∀ n, ρ * s n ≤ s (n + 1))
    (hclosure : ∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) :
    Tendsto (fun n => s (n + 1) / s n) atTop (nhds phi) :=
  ratio_tendsto_phi hpos
    (recurrence_of_floor_above_plastic hpos hρ hρ3 hfloor hclosure)

What this page does not claim

The upper-bound theorem alone does not force the full recurrence. The integer ladder is a counterexample to closure plus generation plus an absolute tick, not to the full theorem with a ratio floor. The framework does not derive the physical existence of a ratio floor from the kernel alone.

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/RecurrenceBridge.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: