Foundation Recurrence Bridge Int Ladder Adjacent Closure

The integer counterexample

The integer ladder is the sequence 1, 2, 3, 4, 5, and so on. Its rungs, the individual entries, grow by exactly one each step. The declaration intLadder_adjacent_closure proves a precise property of this ladder: the sum of any two neighboring rungs is always itself a rung, and that rung sits at least two positions further along. For example, the rungs 2 and 3 sum to 5, which appears two places later; the rungs 3 and 4 sum to 7, which appears three places later.

This property matters because it is a candidate explanation for the golden ratio. In the framework's account, a ledger, a discrete record of events, builds each new rung by combining two earlier ones. If combining two adjacent rungs always yields another rung, one might hope this closure rule alone forces the rungs to grow like the Fibonacci numbers, whose ratios approach the golden ratio φ ≈ 1.618. The integer ladder shows why that hope fails.

The integer ladder satisfies adjacent closure, yet its rungs grow linearly, not like Fibonacci numbers. Its ratios of successive rungs approach 1, not φ. The machine-checked theorem intLadder_recurrence_fails confirms that the Fibonacci recurrence, where each rung equals the sum of the two before it, does not hold for this ladder. The integer ladder also has no ratio floor above 1: for any growth factor ρ greater than 1, some step will grow by less than ρ. This absence is the key difference from the golden-ratio case.

In Recognition Science, the integer ladder is a countermodel. The theorem closure_generation_tick_insufficient packages it: a sequence can be strictly increasing, satisfy adjacent closure, have every rung be a sum of two smaller rungs, and have a constant step size of 1, yet still fail to follow the Fibonacci recurrence. This refutes the naive idea that the framework's basic posting operation, combined with a minimum step size, automatically produces the golden ratio. The recurrence requires an additional, explicit premise: a per-rung growth floor above the plastic constant, about 1.3247.

What the declaration does not claim is just as important. It does not say the integer ladder is the only sequence with adjacent closure, nor that adjacent closure alone determines the golden ratio. It does not claim the integer ladder is a physically realized ledger in the framework. It is a mathematical example, a tool for showing which premises are genuinely needed and which are not.

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_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_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 the only sequence with adjacent closure. Adjacent closure alone forces the golden ratio. The integer ladder is a physically realized ledger in the framework.

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: