Encyclopedia Foundation Foundation Recurrence Bridge Recurrence Of Floor Above Plastic
ARTICLE 4 claims 4 theorems
Foundation Recurrence Bridge Recurrence Of Floor Above Plastic
A simple rule about how fast a sequence grows, combined with a closure property, forces the sequence to obey the Fibonacci-like recurrence s(n+2) = s(n+1) + s(n).
The recurrence bridge
The Fibonacci sequence is defined by the rule that each term is the sum of the two before it. The declaration recurrence_of_floor_above_plastic proves a condition under which any positive sequence must follow this same rule. The condition has two parts. First, the sequence must grow by at least a fixed factor ρ on every step, where ρ is greater than the plastic constant (about 1.3247), the unique real number satisfying ρ³ = ρ + 1. Second, the sequence must have adjacent closure: the sum of any two consecutive terms must itself be a term of the sequence, appearing at some later position.
Under these two hypotheses, the theorem forces the exact recurrence s(n+2) = s(n+1) + s(n) for every n. The proof is a short argument about positions. Since the sequence grows by at least ρ each step, the sum s(n) + s(n+1) is at most (1 + 1/ρ)·s(n+1). Because ρ³ > ρ + 1, this quantity is strictly less than ρ²·s(n+1), which is at most s(n+3). So the sum cannot be as large as the term at position n+3. By adjacent closure, the sum must be some later term, and the only position left is n+2. Hence the sum equals s(n+2), which is precisely the recurrence.
The plastic constant is not an arbitrary cutoff. A companion theorem, plastic_sharpness, shows the threshold is exact. If ρ equals the plastic constant, the growth condition holds with equality, adjacent closure still holds, but the recurrence fails: the sum of two consecutive terms lands at position n+3, skipping n+2. The strict inequality ρ³ > ρ + 1 cannot be relaxed to ≥. This sharpness result is what makes the plastic constant the precise boundary between sequences that obey the Fibonacci-like rule and those that do not.
The theorem also clarifies what does not force the recurrence. A separate counterexample, the integer ladder s(n) = n + 1, is strictly increasing, satisfies adjacent closure, has every term expressible as a sum of two smaller terms, and has a constant step size of 1. Yet it violates the recurrence and admits no growth factor above 1. This shows that closure, generation, and a fixed minimum step together are insufficient; the growth floor above the plastic constant is genuine extra content. The theorem therefore isolates exactly which additional premise is needed to derive the Fibonacci-like rhythm from the framework's structural assumptions.
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]
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 phi_of_floor_above_plastic · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- **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 theorem does not claim that the growth floor and adjacent closure hold for any actual physical ladder. The theorem does not claim that the plastic constant itself satisfies the recurrence; the sharpness result shows it does not. The theorem does not claim that closure and a fixed minimum step alone force the recurrence, as the integer ladder demonstrates.
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:
- Does the framework's physical posting operation satisfy adjacent closure for all rungs?
- What physical mechanism guarantees a per-rung cost floor above J(plastic)?
- How does the integer ladder counterexample constrain the interpretation of the banked tick?
- Does the recurrence bridge extend to sequences that are not strictly positive?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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]If a positive sequence grows by at least a factor ρ > 1 on every step, where ρ³ > ρ + 1, and the sum of any two consecutive terms is itself a term, then the sequence obeys s(n+2) = s(n+1) + s(n) for all n. 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 exact threshold: at ρ = plastic, the growth condition holds with equality and adjacent closure holds, but the recurrence fails. plastic_sharpness · IndisputableMonolith/Foundation/RecurrenceBridge.leanTHEOREM 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 integer ladder s(n) = n + 1 satisfies closure, generation, and a constant step of 1, yet violates the recurrence and has no ratio floor above 1. closure_generation_tick_insufficient · IndisputableMonolith/Foundation/RecurrenceBridge.leanTHEOREM phi_of_floor_above_plastic · IndisputableMonolith/Foundation/RecurrenceBridge.lean
/-- **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)A ratio floor above the plastic constant plus adjacent closure forces the recurrence, and hence the asymptotic ratio of consecutive terms is the golden ratio φ. phi_of_floor_above_plastic · IndisputableMonolith/Foundation/RecurrenceBridge.lean