Foundation Recurrence Bridge Int Ladder Recurrence Fails

The integer counterexample

Consider the ladder of whole numbers: 1, 2, 3, 4, and so on. Each rung is exactly one more than the last. This is the most basic strictly increasing sequence there is, and it has a striking property: every rung after the first two is the sum of two smaller rungs (for instance, 5 = 2 + 3), and the sum of any two adjacent rungs is always another rung further up the ladder (1 + 2 = 3, 2 + 3 = 5, 3 + 4 = 7, and so on). Yet it does not satisfy the famous adjacent recurrence where each rung is the sum of the two immediately before it: 3 is not 2 + 1, and 4 is not 3 + 2. The simplest ladder breaks the pattern.

This is not a curiosity. In the Recognition Science framework, the question of what forces the golden ratio to appear comes down to what forces that adjacent recurrence. A machine-checked library of formal theorems proves that if a ladder grows by at least a certain ratio at each step, and if the sum of two adjacent rungs is always a rung, then the recurrence is forced. The threshold ratio is the plastic constant, about 1.3247, the number solving r³ = r + 1. The integer ladder, growing by a fixed step of 1, has no such ratio floor: for any ratio above 1, eventually the next rung is less than that ratio times the current one. The theorem intLadder_recurrence_fails records this failure formally.

The integer ladder also satisfies several other tempting conditions. It is strictly increasing, every rung is a sum of two smaller rungs, the composition of adjacent rungs is always a rung, and its step size is exactly 1, an absolute minimum. The framework's library proves all of these hold, and yet the recurrence still fails. This is the packaged countermodel: closure, generation, and an absolute tick are not enough. The ratio floor is genuine extra content, and it is precisely what the integer ladder lacks.

In Recognition Science, this result sharpens the foundation for the golden ratio. The recurrence is not free; it requires a named extra hypothesis, a per-rung cost floor above the plastic constant. The integer ladder shows why that hypothesis is not optional. The framework models the ladder as a ledger of recognition events, and the recurrence as the posting operation's completeness for adjacent rungs, but the integer example proves that these alone do not force the golden ratio rhythm.

The consequence is a cleaner conditional theorem. The framework proves that a ratio floor above the plastic constant, together with adjacent closure, forces the recurrence and hence the asymptotic ratio φ. The integer ladder marks the sharp boundary: relax the floor, and the golden ratio is no longer forced. What remains open is whether the framework's cost structure delivers such a floor in the physical setting, a question the library names as an open target.

theorem intLadder_recurrence_fails :
    ¬ (∀ n, intLadder (n + 2) = intLadder (n + 1) + intLadder n) := by
  intro h
  have h1 := h 1
  simp only [intLadder] at h1
  norm_num at h1

theorem intLadder_strictMono : StrictMono intLadder := by
  intro a b h
  simp only [intLadder]
  have hcast : (a : ℝ) < (b : ℝ) := Nat.cast_lt.mpr h
  linarith

theorem intLadder_adjacent_closure :
    ∀ n, ∃ m, m ≥ n + 2 ∧ intLadder m = intLadder n + intLadder (n + 1) := by
  intro n
  refine ⟨2 * n + 2, by omega, ?_⟩
  simp only [intLadder]
  push_cast
  ring

theorem intLadder_generation :
    ∀ n, n ≥ 2 → ∃ a b, a ≤ b ∧ b < n ∧
      intLadder n = intLadder a + intLadder b := by
  intro n hn
  refine ⟨0, n - 1, by omega, by omega, ?_⟩
  simp only [intLadder]
  have h : ((n - 1 : ℕ) : ℝ) = (n : ℝ) - 1 := by
    rw [Nat.cast_sub (by omega : 1 ≤ n), Nat.cast_one]
  rw [h]
  push_cast
  ring

theorem intLadder_tick : ∀ n, intLadder (n + 1) - intLadder n = 1 := by
  intro n
  simp only [intLadder]
  push_cast
  ring

theorem intLadder_no_ratio_floor :
    ∀ ρ : ℝ, 1 < ρ → ∃ n, intLadder (n + 1) < ρ * intLadder n := by
  intro ρ hρ
  obtain ⟨N, hN⟩ := exists_nat_gt (1 / (ρ - 1))
  refine ⟨N, ?_⟩
  simp only [intLadder]
  push_cast
  have hρ1 : 0 < ρ - 1 := by linarith
  have h1 : 1 / (ρ - 1) * (ρ - 1) = 1 := by field_simp [ne_of_gt hρ1]
  have hN' : (1 : ℝ) < (N : ℝ) * (ρ - 1) := by nlinarith [hN, hρ1, h1]
  have hN'' : ρ * (N : ℝ) > (N : ℝ) + 1 := by
    have e : (N : ℝ) * (ρ - 1) = ρ * (N : ℝ) - (N : ℝ) := by ring
    rw [e] at hN'
    linarith [hN']
  nlinarith [hN'', 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⟩

What this page does not claim

The integer ladder is a model of physical reality; it is a counterexample showing a missing premise. The recurrence is false for all ladders; it is forced under the named extra hypothesis of a ratio floor above the plastic constant. The plastic constant itself is derived from the integer ladder; it is the exact threshold for the forcing theorem.

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: