Encyclopedia Foundation Foundation Cost Floor Boundary Phi Ladder Ratio Tendsto

ARTICLE 5 claims 5 theorems

Foundation Cost Floor Boundary Phi Ladder Ratio Tendsto

A simple ratio fact about a specific sequence, and the precise boundary of what the Recognition Science framework's core theorems can and cannot force.

Verify this page

The φ-ladder's ratio

The golden ratio φ, approximately 1.618, is the unique positive solution to the equation r² = r + 1. A sequence whose successive terms grow by this factor, such as 1, φ, φ², φ³, and so on, has the property that the ratio of any term to the one before it is always exactly φ. The declaration phiLadder_ratio_tendsto states this elementary fact about the specific sequence called the φ-ladder: its consecutive ratios form a constant sequence, and therefore converge to φ in the limit.

The Recognition Science framework models scale as a discrete record of events, a ledger, where each entry is a rung on a ladder. The framework's machine-checked library of formal theorems has proved that any such ladder satisfying certain basic structural conditions must have ratios converging to φ, provided it also grows faster than a particular threshold. The φ-ladder is the canonical example that meets all these conditions, and this declaration confirms that its ratios indeed converge to φ, serving as a consistent instance of the framework's general result.

The same library also proves that the integer ladder, the sequence of natural numbers 1, 2, 3, 4, and so on, satisfies all the same basic structural conditions. Its consecutive ratios converge to 1, not φ. This pair of examples demonstrates a logical boundary: the framework's core axioms about scale ladders are not strong enough, by themselves, to force the golden ratio. The growth floor, the requirement that each rung increase by at least a certain factor, is a separate premise that must be added from outside the abstract kernel.

The declaration does not claim that the φ-ladder is the only possible scale ladder, nor that the framework's basic axioms alone force the golden ratio. It does not claim that the growth floor itself is derived within the framework. The floor is a residual premise, and its certified value is tied to the plastic constant, whose cost is bounded between about 3.3 and 4.1 percent of the framework's calibrated cost unit. Any future derivation of this floor would have to come from additional physical structure, not from the abstract kernel alone.

THEOREM phiLadder_ratio_tendsto · IndisputableMonolith/Foundation/CostFloorBoundary.lean
phiLadder_ratio_tendsto · IndisputableMonolith/Foundation/CostFloorBoundary.lean:138 
/-- The φ-ladder's ratios are constantly φ. -/
theorem phiLadder_ratio_tendsto :
    Tendsto (fun n => phiLadderBanked.s (n + 1) / phiLadderBanked.s n)
      atTop (nhds phi) := by
  have e : (fun n => phiLadderBanked.s (n + 1) / phiLadderBanked.s n)
      = fun _ => phi := by
    ext n
    show phi ^ (n + 1) / phi ^ n = phi
    rw [pow_succ']
    field_simp [pow_ne_zero n phi_pos.ne']
  rw [e]
  exact tendsto_const_nhds
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 integerLadderBanked · IndisputableMonolith/Foundation/CostFloorBoundary.lean
integerLadderBanked · IndisputableMonolith/Foundation/CostFloorBoundary.lean:115 
/-- The integer ladder is banked: it too satisfies every premise the kernel
has forced (this is the countermodel content of RecurrenceBridge). -/
def integerLadderBanked : BankedLadder where
  s := intLadder
  pos := by
    intro n
    show 0 < intLadder n
    simp only [intLadder]
    positivity
  mono := intLadder_strictMono
  closure := intLadder_adjacent_closure
  generation := intLadder_generation
  tick := ⟨1, one_pos, fun n => le_of_eq (intLadder_tick n).symm⟩
THEOREM integerLadder_ratio_tendsto · IndisputableMonolith/Foundation/CostFloorBoundary.lean
integerLadder_ratio_tendsto · IndisputableMonolith/Foundation/CostFloorBoundary.lean:151 
/-- The integer ladder's ratios converge to 1. -/
theorem integerLadder_ratio_tendsto :
    Tendsto (fun n => integerLadderBanked.s (n + 1) / integerLadderBanked.s n)
      atTop (nhds 1) := by
  have key : Tendsto (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1)) atTop (nhds 0) := by
    have hc : Tendsto (fun n : ℕ => (n : ℝ) + 1) atTop atTop :=
      tendsto_atTop_mono (l := atTop) (f := fun n : ℕ => (n : ℝ))
        (g := fun n : ℕ => (n : ℝ) + 1)
        (fun n : ℕ => le_add_of_nonneg_right zero_le_one)
        tendsto_natCast_atTop_atTop
    have hinv : Tendsto (fun x : ℝ => x⁻¹) atTop (nhds 0) :=
      tendsto_inv_atTop_zero
    exact Filter.Tendsto.congr
      (f₁ := fun n : ℕ => (((n : ℝ) + 1))⁻¹)
      (f₂ := fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1))
      (fun n : ℕ => by
        show ((n : ℝ) + 1)⁻¹ = 1 / ((n : ℝ) + 1)
        rw [← one_div])
      (hinv.comp hc)
  have hsum : Tendsto (fun n : ℕ => (1 : ℝ) + 1 / ((n : ℝ) + 1)) atTop
      (nhds ((1 : ℝ) + 0)) :=
    tendsto_const_nhds.add key
  rw [add_zero] at hsum
  exact Filter.Tendsto.congr
    (f₁ := fun n : ℕ => (1 : ℝ) + 1 / ((n : ℝ) + 1))
    (f₂ := fun n : ℕ => integerLadderBanked.s (n + 1) / integerLadderBanked.s n)
    (fun n : ℕ => by
      show (1 : ℝ) + 1 / ((n : ℝ) + 1) = intLadder (n + 1) / intLadder n
      simp only [intLadder]
      push_cast
      have hn : ((n : ℝ) + 1) ≠ 0 := by positivity
      field_simp [hn])
    hsum
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⟩

What this page does not claim

The declaration does not claim that the φ-ladder is the only possible scale ladder. The declaration does not claim that the framework's basic axioms alone force the golden ratio. The declaration does not claim that the growth floor is derived within the framework's kernel.

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