Encyclopedia Foundation Foundation Cost Floor Boundary Jcost Strict Mono One Lt

ARTICLE 5 claims 5 theorems

Foundation Cost Floor Boundary Jcost Strict Mono One Lt

The golden ratio emerges only if each rung of a scale ladder costs more than a fixed threshold; the kernel alone does not set that floor.

Verify this page

The cost floor boundary

The golden ratio φ, about 1.618, is the unique ratio at which a sequence grows by adding its two previous terms. Recognition Science asks when such a ratio is forced rather than chosen. Its machine-checked library of formal theorems shows that a scale ladder, a sequence of positive steps where each step is the sum of two earlier ones, converges to φ exactly when each step costs more than a fixed floor. The declaration jcost_strictMono_one_lt pins down the cost function's behavior above 1: for any two ratios a and b with 1 ≤ a < b, the cost of b is strictly greater than the cost of a. This monotonicity is what lets a ratio floor translate into a cost floor.

The cost function itself, written J(x) = (x + 1/x)/2 − 1, measures the recognition cost of a ratio in calibrated units where J(e) = 1. It is strictly increasing for ratios above 1, which is exactly what the theorem states. The plastic constant ρ, about 1.3247, solves ρ³ = ρ + 1. Its cost J(ρ) lies between 1/30 and 41/1000, roughly 3 to 4 percent of the cost unit. The floor the golden ratio needs is: each rung step costs more than this value. The theorem certifies that the cost function respects this threshold ordering.

What the theorem does not claim is that the floor itself is forced. The library proves independence: the banked ladder structure, which packages positivity, strict growth, adjacent closure, full generation, and an absolute tick, admits two ladders with different asymptotic ratios, φ and 1. The integer ladder has per-step costs 1/(2(n+1)(n+2)), which tend to zero, so no positive floor follows from the banked structure alone. The ratio floor above plastic is a residual premise, not a derived conclusion. The monotonicity theorem is the bridge that makes the premise precise, not the source of the premise.

In plain terms: the golden ratio is forced for any ladder that grows faster than plastic, and the cost reading of that growth condition is exact because J is strictly increasing above 1. The kernel does not fix the growth rate. The floor is the single remaining assumption, with a certified cost value of roughly 3 to 4 percent of the cost unit. Any future derivation of that floor must come from structure outside the abstract kernel, such as mass-spectrum stability physics, not from the monotonicity theorem itself.

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

What this page does not claim

The theorem does not prove that any ladder must grow faster than plastic. The theorem does not derive the golden ratio from the banked structure alone. The theorem does not establish a minimal posting quantum for the banked structure.

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