Encyclopedia Foundation Foundation Cost Floor Boundary Banked Plus Floor Gives Phi

ARTICLE 5 claims 5 theorems

Foundation Cost Floor Boundary Banked Plus Floor Gives Phi

A machine-checked theorem shows that a simple growth condition on a ladder of values forces the golden ratio, but only if that condition is assumed.

Verify this page

The growth floor

The golden ratio, often written φ, is the number that solves r² = r + 1, roughly 1.618. It appears throughout geometry and nature, from the pentagon to the spiral growth of shells. In mathematics, one way to see it is through a ladder of numbers where each term is the sum of the two before it, like 1, 1, 2, 3, 5, 8. The ratios of consecutive terms in that ladder settle down to φ. A natural question is whether this behavior is inevitable, or whether it depends on a hidden assumption.

A machine-checked library of formal theorems, called the framework's library, examines this question in a general setting. It defines a ledger, a discrete record of values that grows step by step. The library proves that if a ledger's values are positive, strictly increasing, and each new value is a sum of two earlier ones, then the ratios of consecutive values can converge to φ. But it also proves the opposite: the ratios can converge to 1 instead, as with the ladder 1, 2, 3, 4, 5. So the sum rule alone does not force φ.

The missing ingredient is a growth floor. The theorem banked_plus_floor_gives_phi states that if a ledger also has each step at least ρ times the previous one, where ρ is a number above the plastic constant (about 1.3247), then the ratios must converge to φ. The plastic constant is the real number solving r³ = r + 1. The floor condition means each rung grows by a fixed minimum factor, and that factor is enough to rule out the slow integer ladder.

The theorem also gives a cost reading. Each ratio step carries a cost, measured by a function J that is zero when the ratio is 1 and grows as the ratio moves away from 1. A ratio floor ρ is exactly a per-step cost floor J(ρ). The library certifies that this cost floor lies between about 3.3 and 4.1 percent of the unit cost, where the unit is set by J(e) = 1. So the floor needed is: each rung step costs more than about 4 percent of the cost unit.

In Recognition Science, this result sharpens an earlier chain of theorems. It shows that the golden ratio is forced for any ledger that grows faster than the plastic constant, but the growth rate itself is not fixed by the kernel. The growth floor remains a single residual premise, with a certified cost value. The library also proves that no theorem about the banked ledger structure alone can force that floor: the integer ladder is a counterexample whose per-step costs go below any positive bound. Any future derivation of the floor must come from structure outside the banked ledger, such as mass-spectrum stability physics.

THEOREM banked_plus_floor_gives_phi · IndisputableMonolith/Foundation/CostFloorBoundary.lean
banked_plus_floor_gives_phi · IndisputableMonolith/Foundation/CostFloorBoundary.lean:129 
/-- **The positive assembly.** A banked ladder with a ratio floor above the
plastic constant has ratio converging to φ. The floor is exactly the
residual premise: everything else is banked. -/
theorem banked_plus_floor_gives_phi (L : BankedLadder)
    {ρ : ℝ} (hρ : 1 < ρ) (hρ3 : ρ + 1 < ρ ^ 3)
    (hfloor : ∀ n, ρ * L.s n ≤ L.s (n + 1)) :
    Tendsto (fun n => L.s (n + 1) / L.s n) atTop (nhds phi) :=
  phi_of_floor_above_plastic L.pos hρ hρ3 hfloor L.closure
THEOREM banked_independence · IndisputableMonolith/Foundation/CostFloorBoundary.lean
banked_independence · IndisputableMonolith/Foundation/CostFloorBoundary.lean:185 
/-- **The boundary theorem.** The banked structure admits two ladders with
different asymptotic ratios (φ and 1). Hence the ratio floor above plastic —
and a fortiori the per-rung cost floor — is logically independent of
everything the kernel has forced about scale ladders. -/
theorem banked_independence :
    ∃ L₁ L₂ : BankedLadder,
      Tendsto (fun n => L₁.s (n + 1) / L₁.s n) atTop (nhds phi) ∧
      Tendsto (fun n => L₂.s (n + 1) / L₂.s n) atTop (nhds 1) ∧ phi ≠ 1 :=
  ⟨phiLadderBanked, integerLadderBanked, phiLadder_ratio_tendsto,
    integerLadder_ratio_tendsto, ne_of_gt one_lt_phi⟩
THEOREM ratio_floor_gives_cost_floor · IndisputableMonolith/Foundation/CostFloorBoundary.lean
ratio_floor_gives_cost_floor · IndisputableMonolith/Foundation/CostFloorBoundary.lean:203 
/-- A ratio floor ρ is exactly a per-rung J-cost floor J(ρ): the cost reading
of the recurrence's residual premise. -/
theorem ratio_floor_gives_cost_floor {s : ℕ → ℝ} (hpos : ∀ n, 0 < s n)
    {ρ : ℝ} (hρ : 1 < ρ) (hfloor : ∀ n, ρ * s n ≤ s (n + 1)) :
    ∀ n, Cost.Jcost ρ ≤ Cost.Jcost (s (n + 1) / s n) := by
  intro n
  have hratio : ρ ≤ s (n + 1) / s n := by
    rw [le_div_iff₀ (hpos n)]
    exact hfloor n
  have hlog : Real.log ρ ≤ Real.log (s (n + 1) / s n) :=
    Real.log_le_log (by linarith [hρ]) hratio
  rw [Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (by linarith [hρ] : (0 : ℝ) < ρ),
    Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (div_pos (hpos (n + 1)) (hpos n))]
  exact sub_le_sub_right
    (Cost.GeometricRoot.cosh_mono_on_nonneg (Real.log_nonneg (le_of_lt hρ)) hlog) 1
THEOREM jcost_plastic_certified_bounds · IndisputableMonolith/Foundation/CostFloorBoundary.lean
jcost_plastic_certified_bounds · IndisputableMonolith/Foundation/CostFloorBoundary.lean:237 
/-- **The certified threshold.** The plastic constant lies in
(13/10, 133/100), and its J-cost lies in (1/30, 41/1000) — about 3 to 4
percent of the calibrated cost unit (J(e) = 1). The floor T6 needs is:
each rung step costs more than this. -/
theorem jcost_plastic_certified_bounds :
    ∃ r : ℝ, 1 < r ∧ 1 + r = r ^ 3 ∧
      (1 / 30 < Cost.Jcost r ∧ Cost.Jcost r < 41 / 1000) := by
  have hcont : ContinuousOn (fun x : ℝ => x ^ 3 - x - 1)
      (Set.Icc (13 / 10) (133 / 100)) :=
    ((continuous_pow 3).sub continuous_id |>.sub continuous_const).continuousOn
  have hmem : (0 : ℝ) ∈
      Set.Ioo ((13 / 10 : ℝ) ^ 3 - 13 / 10 - 1)
        ((133 / 100 : ℝ) ^ 3 - 133 / 100 - 1) := by
    constructor <;> norm_num
  have hivt := intermediate_value_Ioo
    (by norm_num : (13 / 10 : ℝ) ≤ 133 / 100) hcont hmem
  obtain ⟨r, hr, hfr⟩ := hivt
  have hr3 : 1 + r = r ^ 3 := by
    have h0 : r ^ 3 - r - 1 = 0 := hfr
    linarith
  have hr1 : 1 < r := by linarith [hr.1]
  refine ⟨r, hr1, hr3, ?_, ?_⟩
  · have hmono := jcost_strictMono_one_lt (a := (13 : ℝ) / 10) (b := r)
      (by norm_num) hr.1
    have hval : Cost.Jcost (13 / 10 : ℝ) = 9 / 260 := by norm_num [Cost.Jcost]
    linarith [hmono, hval]
  · have hmono := jcost_strictMono_one_lt (a := r) (b := (133 : ℝ) / 100)
      (le_of_lt hr1) hr.2
    have hval : Cost.Jcost (133 / 100 : ℝ) = 1089 / 26600 := by
      norm_num [Cost.Jcost]
    linarith [hmono, hval]
THEOREM cost_floor_independent · IndisputableMonolith/Foundation/CostFloorBoundary.lean
cost_floor_independent · IndisputableMonolith/Foundation/CostFloorBoundary.lean:196 
/-- The banked structure does not imply a uniform ratio floor, and does not
imply the recurrence: the integer ladder is the witness for both. -/
theorem cost_floor_independent :
    ∃ L : BankedLadder, (∀ ρ : ℝ, 1 < ρ → ∃ n, L.s (n + 1) < ρ * L.s n) ∧
      ¬ (∀ n, L.s (n + 2) = L.s (n + 1) + L.s n) :=
  ⟨integerLadderBanked, intLadder_no_ratio_floor, intLadder_recurrence_fails⟩

What this page does not claim

The growth floor itself is not derived; it is assumed as a premise. The integer ladder is not a counterexample to the theorem banked_plus_floor_gives_phi, since it does not satisfy the floor condition. No claim is made that the golden ratio is the only possible limit for all ledgers.

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/CostFloorBoundary.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND