Encyclopedia Foundation Foundation Cost Floor Boundary No Kernel Minimal Posting Cost

ARTICLE 5 claims 5 theorems

Foundation Cost Floor Boundary No Kernel Minimal Posting Cost

A machine-checked theorem shows the framework's core assumptions allow costs to shrink without limit, so the golden ratio needs one extra premise.

Verify this page

The missing floor

A ledger, a discrete record of events in the Recognition Science framework, assigns a cost to each step between adjacent rungs of a scale ladder. One might expect that these costs have a built-in minimum, a smallest possible posting. The declaration no_kernel_minimal_posting_cost proves otherwise: for any positive number you name, no matter how small, there is a ladder in the framework's banked structure where some adjacent step costs less than that number. The costs can sink toward zero.

The proof exhibits a concrete example, the integer ladder. On that ladder, the cost of step n is exactly 1/(2(n+1)(n+2)), a fraction that shrinks to zero as n grows. The integer ladder satisfies every property the framework's kernel has forced: positivity, strict growth, adjacent closure, full generation, and a positive lower bound on the absolute step. So the absence of a floor is not a gap in the definitions; it is a proved fact about them.

The consequence is precise. The framework's cost function J, which measures the price of recognition, is fixed by theorem, but its calibration pins the unit (J(e) = 1), not a floor. The golden ratio φ emerges only when an extra condition is added: a ratio floor above the plastic constant, meaning each rung step costs more than about 4 percent of the cost unit. That floor is not derived from the kernel. It is the single residual premise, logically independent of everything banked, and any future derivation must come from structure outside the abstract kernel, such as mass-spectrum stability physics.

What the declaration does not claim is equally important. It does not say the framework is broken or incomplete. It does not say the golden ratio is unattainable; rather, it sharpens the status: φ is forced for any ladder growing faster than plastic, and the growth floor is the one open question. It also does not claim that a minimal posting cost exists in some other structure; it claims only that the banked structure, the one the kernel has forced, does not imply one.

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 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 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 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]

What this page does not claim

The framework is incomplete or inconsistent because it lacks a minimal posting cost. The golden ratio is unattainable; it is forced for any ladder growing faster than plastic. A minimal posting cost exists in some other structure beyond the banked one.

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