Encyclopedia Foundation Foundation Recurrence Bridge Closure Generation Tick Insufficient
ARTICLE 3 claims 3 theorems
Foundation Recurrence Bridge Closure Generation Tick Insufficient
A simple counting ladder shows why the golden ratio's recurrence needs a stronger premise than the framework's basic machinery.
The integer ladder countermodel
The golden ratio φ satisfies the recurrence r² = r + 1, and a sequence whose adjacent terms obey s(n+2) = s(n+1) + s(n) has ratios converging to φ. The Recognition Science framework asks what structural conditions force that recurrence. One candidate set of conditions is closure, generation, and an absolute minimum step. The declaration closure_generation_tick_insufficient shows these three conditions, even together, do not suffice: it exhibits a concrete countermodel, the integer ladder s(n) = n + 1, that satisfies all three yet violates the recurrence.
The integer ladder is the simplest possible strictly increasing sequence of positive numbers: 1, 2, 3, 4, and so on. It satisfies closure: the composition of any two adjacent rungs, meaning their sum, is always another rung (for instance, 3 + 4 = 7, which appears later in the ladder). It satisfies generation: every rung beyond the first two is the sum of two smaller rungs. It also has an absolute minimum step of 1, the form the framework's banked tick takes. Yet the ladder fails the recurrence: s(n+2) = n+3 is never equal to s(n+1) + s(n) = 2n+3 for n ≥ 1. The countermodel also admits no ratio floor above 1: the ratio of successive terms, (n+2)/(n+1), approaches 1 and never stays above any fixed bound greater than 1.
The countermodel therefore refutes the naive route that the banked tick alone gives the recurrence. It isolates what the recurrence genuinely requires: a per-rung ratio floor above the plastic constant ρ, where ρ³ = ρ + 1 (approximately 1.3247). The framework's forcing theorem, recurrence_of_floor_above_plastic, proves that if every step multiplies size by at least ρ with strict inequality ρ³ > ρ + 1, and adjacent closure holds, then the recurrence follows. The integer ladder lacks exactly this ratio floor, which is why it escapes the theorem. The plastic constant is the sharp threshold: at ρ³ = ρ + 1 exactly, the plastic ladder satisfies closure but skips rung n+2, violating the recurrence.
In Recognition Science, the framework models this as a precise boundary on its own machinery. The declaration does not claim that the golden ratio is unattainable, nor that the framework's physical premises are false. It claims only that closure, generation, and an absolute tick are jointly insufficient, and that the ratio floor is genuine extra content. The framework's T6 assembly, phi_of_floor_above_plastic, thus stands conditional on two named premises: the ratio floor and adjacent closure. Whether the kernel's tick plus the RCL deliver a per-rung cost floor above J(plastic) remains an open target, not a settled fact.
THEOREM closure_generation_tick_insufficient · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- 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⟩
THEOREM recurrence_of_floor_above_plastic · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- **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]
THEOREM plastic_sharpness · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- The threshold is exact: at ρ = plastic (ρ³ = ρ + 1, the non-strict
boundary), the plastic ladder satisfies the ratio floor with equality,
satisfies adjacent closure (its composition lands at rung n+3, skipping
rung n+2), and violates the adjacent recurrence. The strict inequality
ρ³ > ρ + 1 in the bridge theorem cannot be relaxed to ≥. -/
theorem plastic_sharpness :
∃ (s : ℕ → ℝ) (ρ : ℝ), (∀ n, 0 < s n) ∧ 1 < ρ ∧ ρ ^ 3 = ρ + 1 ∧
(∀ n, ρ * s n ≤ s (n + 1)) ∧
(∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) ∧
¬ (∀ n, s (n + 2) = s (n + 1) + s n) := by
obtain ⟨r, hr1, hr3⟩ := PhiClosureSelection.plastic_ladder_exists
have hr0 : 0 < r := by linarith
refine ⟨fun n => r ^ n, r, (fun n => pow_pos hr0 n), hr1, by linarith [hr3],
?_, ?_, ?_⟩
· intro n
exact le_of_eq (pow_succ' r n).symm
· intro n
refine ⟨n + 3, by omega, ?_⟩
show r ^ (n + 3) = r ^ n + r ^ (n + 1)
rw [pow_add, mul_comm, ← hr3, pow_succ']
ring
· intro hall
have h0 := hall 0
dsimp only at h0
norm_num at h0
have e : r ^ 3 = 2 * r + 1 := by
calc r ^ 3 = r ^ 2 * r := by ring
_ = (r + 1) * r := by rw [h0]
_ = r ^ 2 + r := by ring
_ = 2 * r + 1 := by rw [h0]; ring
linarith [e, hr3, hr1]
What this page does not claim
The integer ladder is a physical model of any real system. The golden ratio is unattainable within the framework. Closure and generation alone are sufficient for the 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/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:
- What physical mechanism, if any, supplies the per-rung ratio floor above the plastic constant?
- Does the framework's kernel tick, combined with the RCL, actually deliver a cost floor above J(plastic) for physical ladders?
- What other countermodels exist that satisfy the ratio floor but fail closure?
- How does the integer ladder's failure relate to the framework's existing obstruction, HierarchyRealizationObstruction?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM closure_generation_tick_insufficient · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- 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 declaration closure_generation_tick_insufficient shows these three conditions, even together, do not suffice: it exhibits a concrete countermodel, the integer ladder s(n) = n + 1, that satisfies all three yet violates the recurrence. closure_generation_tick_insufficient · IndisputableMonolith/Foundation/RecurrenceBridge.leanTHEOREM recurrence_of_floor_above_plastic · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- **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]The framework's forcing theorem, recurrence_of_floor_above_plastic, proves that if every step multiplies size by at least ρ with strict inequality ρ³ > ρ + 1, and adjacent closure holds, then the recurrence follows. recurrence_of_floor_above_plastic · IndisputableMonolith/Foundation/RecurrenceBridge.leanTHEOREM plastic_sharpness · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- The threshold is exact: at ρ = plastic (ρ³ = ρ + 1, the non-strict boundary), the plastic ladder satisfies the ratio floor with equality, satisfies adjacent closure (its composition lands at rung n+3, skipping rung n+2), and violates the adjacent recurrence. The strict inequality ρ³ > ρ + 1 in the bridge theorem cannot be relaxed to ≥. -/ theorem plastic_sharpness : ∃ (s : ℕ → ℝ) (ρ : ℝ), (∀ n, 0 < s n) ∧ 1 < ρ ∧ ρ ^ 3 = ρ + 1 ∧ (∀ n, ρ * s n ≤ s (n + 1)) ∧ (∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) ∧ ¬ (∀ n, s (n + 2) = s (n + 1) + s n) := by obtain ⟨r, hr1, hr3⟩ := PhiClosureSelection.plastic_ladder_exists have hr0 : 0 < r := by linarith refine ⟨fun n => r ^ n, r, (fun n => pow_pos hr0 n), hr1, by linarith [hr3], ?_, ?_, ?_⟩ · intro n exact le_of_eq (pow_succ' r n).symm · intro n refine ⟨n + 3, by omega, ?_⟩ show r ^ (n + 3) = r ^ n + r ^ (n + 1) rw [pow_add, mul_comm, ← hr3, pow_succ'] ring · intro hall have h0 := hall 0 dsimp only at h0 norm_num at h0 have e : r ^ 3 = 2 * r + 1 := by calc r ^ 3 = r ^ 2 * r := by ring _ = (r + 1) * r := by rw [h0] _ = r ^ 2 + r := by ring _ = 2 * r + 1 := by rw [h0]; ring linarith [e, hr3, hr1]The plastic constant is the sharp threshold: at ρ³ = ρ + 1 exactly, the plastic ladder satisfies closure but skips rung n+2, violating the recurrence. plastic_sharpness · IndisputableMonolith/Foundation/RecurrenceBridge.lean