Foundation Recurrence Bridge Recurrence Of Adjacent Generation Additive

The recurrence bridge

The Fibonacci sequence is the best-known example of a recurrence where each term is the sum of the two before it. This declaration, recurrence_of_adjacent_generation_additive, proves a precise statement about when such a recurrence must appear. It concerns a ladder of rungs, each with a size, where each new rung is created by combining the two rungs below it. The theorem says: if that combination is ordinary addition, then the sizes of the rungs obey the adjacent recurrence, meaning each rung's size is exactly the sum of the two preceding rung sizes.

The proof is immediate from the two assumptions. The ledger, a discrete record of events, is modeled by this ladder. The first assumption, posting locality, states that each new rung is the composition of its two immediate predecessors. The second, ledger additivity, states that the size of a composition is the sum of the sizes of its parts. Together they force the recurrence, and from that recurrence a separate theorem shows the ratio of consecutive rung sizes tends to the golden ratio φ. This is the bridge that connects the ledger's structure to the golden ratio.

This declaration is a theorem in the framework's machine-checked library of formal theorems. It is a conditional result: it does not claim that the recurrence always holds, only that it holds when the two named premises are true. A companion theorem, recurrence_of_floor_above_plastic, shows that the recurrence is also forced by a different pair of conditions: a ratio floor above the plastic constant and adjacent closure. The declaration here is the simpler, more direct route.

The theorem does not claim that the recurrence is inevitable. A separate countermodel, the integer ladder where s(n) = n + 1, satisfies posting locality, ledger additivity, and even an absolute minimum step of 1, yet the recurrence fails. The ratio of consecutive terms tends to 1, not φ. This shows that the recurrence is not a consequence of the ledger alone; it requires the specific premises stated. The theorem also does not claim that the golden ratio itself is derived here; it only establishes the recurrence, which is a step toward that result.

/-- The recurrence decomposes into the posting operation's locality (each new
rung is the composition of its two immediate predecessors) and ledger
additivity (composition size is the sum). This names the two premises
exactly. -/
theorem recurrence_of_adjacent_generation_additive (s : ℕ → ℝ) (comp : ℝ → ℝ → ℝ)
    (hgen : ∀ n, s (n + 2) = comp (s (n + 1)) (s n))
    (hadd : ∀ x y, comp x y = x + y) :
    ∀ n, s (n + 2) = s (n + 1) + s n := fun n => by rw [hgen n, hadd]

/-- Posting locality plus ledger additivity suffice for the φ rhythm. -/
theorem phi_of_posting_locality_additivity (s : ℕ → ℝ) (comp : ℝ → ℝ → ℝ)
    (hpos : ∀ n, 0 < s n)
    (hgen : ∀ n, s (n + 2) = comp (s (n + 1)) (s n))
    (hadd : ∀ x y, comp x y = x + y) :
    Tendsto (fun n => s (n + 1) / s n) atTop (nhds phi) :=
  ratio_tendsto_phi hpos (recurrence_of_adjacent_generation_additive s comp hgen hadd)

/-- 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

This theorem does not claim the adjacent recurrence holds without its two premises. This theorem does not claim the golden ratio is derived directly from the ledger alone. This theorem does not claim the integer ladder is a valid model of physical recognition.

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: