Encyclopedia Cost Cost Cosh Quadratic Lower Bound

ARTICLE 3 claims 3 theorems

Cost Cosh Quadratic Lower Bound

The hyperbolic cosine grows at least as fast as a parabola, a fact the framework's cost function inherits.

Verify this page

The quadratic floor

The hyperbolic cosine, written cosh x, is the average of e^x and e^-x. It is the curve a hanging chain forms, and it appears whenever a quantity grows faster than linearly in both directions. The theorem cosh_quadratic_lower_bound states a simple inequality: for every real number x, cosh x is at least 1 + x^2/2. The right side is the start of the Taylor series of cosh x, so the inequality says the true curve never dips below its own quadratic approximation. At x = 0 both sides equal 1; away from zero the gap widens.

The inequality is a standard fact of classical analysis, provable from the series definition of cosh or from convexity. In the framework's machine-checked library of formal theorems, it is recorded as a theorem with a complete proof. The framework's central object is the cost function, a measure of how far a positive number sits from 1, defined as J(x) = (x + 1/x)/2 - 1. When x is written as e^t, the cost becomes cosh t - 1. The quadratic lower bound on cosh therefore translates directly: the cost of a small step away from 1 grows at least quadratically in the step size, never more slowly.

That translation matters for the framework's picture of recognition. The cost function is meant to charge a forced price for any deviation from unity, and the quadratic floor says the price cannot be artificially gentle near the origin. The bound is sharp in the sense that the quadratic term is the exact leading behavior: a separate lemma, Jcost_one_plus_eps_quadratic, shows that for small epsilon the cost equals epsilon^2/2 plus a cubic correction. The lower bound is the coarse statement; the quadratic lemma is the refined one.

What the declaration does not claim is just as important. It does not say the cost function equals the quadratic expression; it only bounds it from below. It does not assert that the bound is tight for large x, where cosh grows exponentially and the parabola is a poor approximation. It says nothing about the uniqueness of the cost function itself, which is a separate theorem resting on the five forcing conditions. The quadratic floor is one supporting beam in the framework's edifice, not the load-bearing wall.

THEOREM cosh_quadratic_lower_bound · IndisputableMonolith/Cost.lean
cosh_quadratic_lower_bound · IndisputableMonolith/Cost.lean:376 
/-- **THEOREM: Quadratic Lower Bound for cosh**
    cosh x ≥ 1 + x²/2 for all x.

    Proof: From the definition cosh x = (e^x + e^(-x)) / 2 and the Taylor series,
    we have cosh x = 1 + x²/2 + x⁴/24 + ... where all terms are non-negative.

    Alternative proof via convexity: cosh is convex (cosh'' = cosh > 0), and
    the tangent line at 0 gives cosh x ≥ cosh 0 + cosh'(0) * x = 1 + 0 = 1.
    The quadratic bound follows from cosh'' = cosh ≥ 1. -/
theorem cosh_quadratic_lower_bound (x : ℝ) : Real.cosh x ≥ 1 + x^2 / 2 := by
  -- Use the Taylor series expansion
  -- cosh x = ∑' n, x ^ (2 * n) / (2 * n)!
  -- The first two partial sums are: n=0 → 1, n=1 → 1 + x²/2
  -- Since all terms are non-negative, cosh x ≥ 1 + x²/2
  have h := Real.hasSum_cosh x
  -- Extract first two terms and show tail is non-negative
  have h_term0 : (fun n => x ^ (2 * n) / ↑(2 * n).factorial) 0 = 1 := by simp
  have h_term1 : (fun n => x ^ (2 * n) / ↑(2 * n).factorial) 1 = x^2 / 2 := by simp
  -- Each term x^(2n)/(2n)! is non-negative because even powers are non-negative
  have h_nn : ∀ n, 0 ≤ x ^ (2 * n) / ↑(2 * n).factorial := fun n => by
    apply div_nonneg
    · -- x^(2n) = (x^2)^n ≥ 0
      rw [pow_mul]
      exact pow_nonneg (sq_nonneg x) n
    · exact Nat.cast_nonneg _
  -- The sum is at least the sum of the first two terms
  have h_ge : Real.cosh x ≥ 1 + x^2 / 2 := by
    rw [← h.tsum_eq]
    calc ∑' n, x ^ (2 * n) / ↑(2 * n).factorial
        ≥ (x ^ (2 * 0) / ↑(2 * 0).factorial) + (x ^ (2 * 1) / ↑(2 * 1).factorial) := by
          have hs := h.summable
          have h01 : ({0, 1} : Finset ℕ).sum (fun n => x ^ (2 * n) / ↑(2 * n).factorial) ≤
                     ∑' n, x ^ (2 * n) / ↑(2 * n).factorial :=
            hs.sum_le_tsum _ (fun i _ => h_nn i)
          simp only [Finset.sum_pair (by decide : (0 : ℕ) ≠ 1)] at h01
          exact h01
      _ = 1 + x^2 / 2 := by simp
  exact h_ge
THEOREM Jlog_as_cosh · IndisputableMonolith/Cost.lean
Jlog_as_cosh · IndisputableMonolith/Cost.lean:175 
lemma Jlog_as_cosh (t : ℝ) : Jlog t = Real.cosh t - 1 := by
  unfold Jlog Jcost
  rw [Real.cosh_eq, inv_eq_one_div, Real.exp_neg]
  ring
THEOREM Jcost_one_plus_eps_quadratic · IndisputableMonolith/Cost.lean
Jcost_one_plus_eps_quadratic · IndisputableMonolith/Cost.lean:540 
lemma Jcost_one_plus_eps_quadratic (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 2) :
    ∃ (c : ℝ), Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 ∧ |c| ≤ 2 := by
  classical
  have hbounds := abs_le.mp hε
  have hpos : 0 < 1 + ε := by
    have : -(1 : ℝ) / 2 ≤ ε := by simpa [neg_div] using hbounds.1
    linarith
  have hne : 1 + ε ≠ 0 := ne_of_gt hpos
  have hcalc : Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
    simpa [pow_two, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]
      using (Jcost_eq_sq hne)
  let c : ℝ := -1 / (2 * (1 + ε))
  have h_eq :
      Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 := by
    have : ε ^ 2 / (2 * (1 + ε)) = ε ^ 2 / 2 + (-1 / (2 * (1 + ε))) * ε ^ 3 := by
      field_simp [hne]
      ring
    simpa [hcalc, c] using this
  have hden_pos : 0 < 2 * (1 + ε) := by nlinarith [hpos]
  have habs : |c| = 1 / (2 * (1 + ε)) := by
    simp [c, div_eq_mul_inv, abs_mul, abs_inv, abs_of_pos hpos]
  -- Use 1/(2(1+ε)) ≤ 1 from (1+ε) ≥ 1/2
  have hone_le : (1 : ℝ) ≤ 2 * (1 + ε) := by
    have : (1 / 2 : ℝ) ≤ 1 + ε := by linarith
    simpa [two_mul] using mul_le_mul_of_nonneg_left this (by norm_num : (0 : ℝ) ≤ 2)
  have hdiv_le_one : 1 / (2 * (1 + ε)) ≤ 1 := by
    have hpos1 : 0 < (1 : ℝ) := by norm_num
    simpa [one_div] using one_div_le_one_div_of_le hpos1 hone_le
  have hbound : |c| ≤ 2 := by
    have h1 : |c| ≤ 1 := by simpa [habs] using hdiv_le_one
    have h12 : (1 : ℝ) ≤ 2 := by norm_num
    exact le_trans h1 h12
  exact ⟨c, h_eq, hbound⟩

What this page does not claim

The cost function equals the quadratic expression 1 + x^2/2. The quadratic bound is tight for large values of x. This theorem alone forces the uniqueness of the cost function.

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/Cost.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