Encyclopedia Foundation Foundation Cost Floor Boundary Ratio Floor Gives Cost Floor

ARTICLE 5 claims 5 theorems

Foundation Cost Floor Boundary Ratio Floor Gives Cost Floor

A growth condition on a ladder of costs translates exactly into a floor on each step's recognition cost, and that translation is what the kernel proves.

Verify this page

The cost floor

A recognition cost is the price, in a discrete record of events, of registering one event next to another. The framework's cost function J(x) = (x + 1/x)/2 - 1 measures that price in calibrated units where J(e) = 1. The declaration ratio_floor_gives_cost_floor establishes a precise bridge: if every step in a ladder of positive values grows by at least a fixed ratio ρ (with ρ > 1), then every step's recognition cost is at least J(ρ). In plain language, a guarantee that each rung is at least ρ times the previous one is exactly a guarantee that each rung costs at least J(ρ) to recognize.

The theorem is a boundary result, not a derivation of the golden ratio. It takes a ratio floor as an assumption and converts it into a cost floor. The conversion relies on the fact that J is strictly increasing above 1: larger ratios mean larger costs, so a lower bound on ratios becomes a lower bound on costs. The proof is elementary, using the definition of J and the monotonicity property, and it is machine-checked in the framework's library of formal theorems.

What the theorem does not claim is that any ladder must have such a floor. The banked structure, which packages everything the kernel has forced about scale ladders, admits two different ladders: the φ-ladder with ratios constantly φ, and the integer ladder with ratios converging to 1. The integer ladder's per-step costs are 1/(2(n+1)(n+2)), which tend to zero, so no positive cost floor holds for it. The kernel alone therefore does not force a floor; the floor is a separate premise, and the theorem only states what that premise means in cost terms.

The certified threshold makes the premise concrete. The plastic constant, the root of r³ = r + 1, lies between 13/10 and 133/100, and its J-cost lies between 1/30 and 41/1000, roughly 3 to 4 percent of the cost unit. So the floor the framework's golden-ratio theorem needs is: each rung step costs more than about 4 percent of the unit cost. Any future derivation of that floor must come from structure outside the banked ladder, such as mass-spectrum stability physics, not from the abstract kernel.

The practical upshot is a sharpened division of labor. The framework proves that any ladder growing faster than plastic must converge to φ, and it proves that a ratio floor is equivalent to a cost floor. What remains open is whether the physical world supplies that floor. The theorem turns a vague growth condition into a measurable cost threshold, and it names exactly where the missing premise lives.

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_strictMono_one_lt · IndisputableMonolith/Foundation/CostFloorBoundary.lean
jcost_strictMono_one_lt · IndisputableMonolith/Foundation/CostFloorBoundary.lean:219 
/-- J is strictly increasing above 1 (elementary, from the definition). -/
theorem jcost_strictMono_one_lt {a b : ℝ} (ha : 1 ≤ a) (hab : a < b) :
    Cost.Jcost a < Cost.Jcost b := by
  have hab' : 0 < a := by linarith
  have hb : 0 < b := by linarith
  have hab1 : 1 < a * b := by nlinarith [ha, hab, hb]
  have e : Cost.Jcost b - Cost.Jcost a = (b - a) * (1 - 1 / (a * b)) / 2 := by
    unfold Cost.Jcost
    field_simp [hab'.ne', hb.ne', ne_of_gt (by positivity : (0 : ℝ) < a * b)]
    ring
  have hpos : 0 < (b - a) * (1 - 1 / (a * b)) / 2 := by
    have h1 : 0 < 1 - 1 / (a * b) := by
      rw [sub_pos, div_lt_one (by positivity : (0 : ℝ) < a * b)]
      exact hab1
    exact div_pos (mul_pos (by linarith) h1) two_pos
  rw [← e] at hpos
  linarith [hpos]
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 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]
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]

What this page does not claim

The kernel forces any ladder to have a ratio floor above plastic. The theorem derives the golden ratio from the banked structure alone. The cost floor J(ρ) is a minimal posting quantum that every ladder must respect.

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