Encyclopedia Foundation Foundation Cost Floor Boundary

ARTICLE 5 claims 5 theorems

Foundation Cost Floor Boundary

A machine-checked result shows exactly where the golden ratio comes from, and what the framework must add to force it.

Verify this page

The cost floor boundary

The golden ratio φ ≈ 1.618 is famous for appearing in pentagons and Fibonacci numbers. In Recognition Science, the framework asks a sharper question: can the golden ratio be forced to appear as the natural scaling of a discrete growth process? The answer, now proved in the framework's machine-checked library of formal theorems, is that the kernel alone cannot force it. The framework proves that φ appears exactly when one additional premise holds: each step of the growth ladder must cost more than a certified threshold. This boundary result, called the cost floor boundary, separates what the framework derives from what it must take as input.

The framework models a ledger, a discrete record of events, as a ladder of positive numbers that strictly grows. Each rung is a sum of two smaller rungs, a property called adjacent closure. The kernel has forced several properties of any such ladder: positivity, strict growth, closure, full generation, and a positive lower bound on the absolute step, called the tick. These properties are packaged together as a structure called BankedLadder. Two concrete ladders satisfy all of them: the φ-ladder, whose ratios are constantly φ, and the integer ladder, whose ratios converge to 1. The library proves both are banked, and therefore no theorem about BankedLadder alone can force the φ rhythm.

The boundary theorem is precise: the banked structure admits two ladders with different asymptotic ratios, φ and 1, so the ratio floor above the plastic constant is logically independent of everything the kernel has forced. The integer ladder is the witness: its adjacent-step costs are exactly 1/(2(n+1)(n+2)), which tend to zero, so there is no minimal posting quantum in the banked structure. Calibration pins the cost unit (J(e) = 1), not a floor, and the tick caps refinement of a fixed comparison, never rung ratios. This kills the hope that the kernel alone derives a per-rung cost floor.

The positive face is equally sharp. The library proves that a banked ladder with a ratio floor above the plastic constant has ratio converging to φ. A ratio floor ρ is precisely a per-rung J-cost floor J(ρ), where J is the framework's forced cost function. 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. The floor T6 needs is: each rung step costs more than this. Any future derivation of that floor must come from structure outside BankedLadder, such as mass-spectrum stability physics, not from the abstract kernel, by the independence theorems here.

What this changes is the shape of the framework's claim. The golden ratio is not an accident of the kernel; it is forced for any ladder growing faster than plastic, provided that growth floor holds. The kernel alone does not fix the growth rate. The growth floor is the single residual premise, with a certified cost value. The framework now knows exactly what it must borrow from physics, and what it has already proved.

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 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 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 no_kernel_minimal_posting_cost · IndisputableMonolith/Foundation/CostFloorBoundary.lean
no_kernel_minimal_posting_cost · IndisputableMonolith/Foundation/CostFloorBoundary.lean:269 
/-- **Route (i) is killed as a theorem.** The banked package contains a
ladder whose per-rung adjacent-step costs go below any positive floor:
on the integer ladder the cost of step n is exactly
1/(2(n+1)(n+2)), which tends to zero. There is no minimal posting quantum
in the banked structure. -/
theorem no_kernel_minimal_posting_cost {c : ℝ} (hc : 0 < c) :
    ∃ n, Cost.Jcost (intLadder (n + 1) / intLadder n) < c := by
  obtain ⟨N, hN⟩ := exists_nat_gt (1 / (2 * c))
  refine ⟨N, ?_⟩
  have hN1 : (0 : ℝ) < (N : ℝ) + 1 := by positivity
  have hN2 : (0 : ℝ) < (N : ℝ) + 2 := by positivity
  have e : Cost.Jcost (intLadder (N + 1) / intLadder N)
      = 1 / (2 * ((N : ℝ) + 1) * ((N : ℝ) + 2)) := by
    simp only [intLadder]
    push_cast
    unfold Cost.Jcost
    field_simp [hN1.ne', hN2.ne']
    ring
  rw [e]
  have h1 : 1 / (2 * ((N : ℝ) + 1) * ((N : ℝ) + 2))
      < 1 / (2 * ((N : ℝ) + 1)) := by
    apply one_div_lt_one_div_of_lt (by positivity : (0 : ℝ) < 2 * ((N : ℝ) + 1))
    nlinarith [hN1, hN2]
  have h2 : 1 / (2 * ((N : ℝ) + 1)) < c := by
    rw [div_lt_iff₀ (by positivity : (0 : ℝ) < 2 * ((N : ℝ) + 1))]
    have hc2 : (0 : ℝ) < 2 * c := by positivity
    have hw : 1 / (2 * c) * (2 * c) = 1 := by field_simp [ne_of_gt hc2]
    nlinarith [hN, hc2, hw, hN1]
  linarith [h1, h2]

What this page does not claim

The framework does not claim the kernel alone forces the golden ratio; the cost floor is a residual premise. The framework does not claim the integer ladder is physically meaningful, only that it satisfies all banked premises. The framework does not claim a derivation of the cost floor from mass-spectrum stability; that remains a future target.

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