Foundation Phi Closure Selection Cosh Strict Mono On Nonneg

The strict climb of cosh

The hyperbolic cosine, written cosh, is a close cousin of the familiar cosine but built from exponential growth instead of circular motion. Its value at a number x is (e^x + e^-x)/2, the average of an exponential and its reciprocal. On the nonnegative half of the number line, from 0 upward, cosh never dips and never stalls: if x is less than y, then cosh(x) is strictly less than cosh(y). This property, called strict monotonicity, is the kind of fact that makes a function trustworthy as a measuring stick, since each input gets its own distinct output.

The strict climb has a direct geometric picture. The graph of cosh is the shape a hanging chain takes under gravity, the catenary. Starting at height 1 when x is 0, the curve rises ever more steeply as x grows, with no flat stretches and no backtracking. The function's derivative, sinh, is positive for every positive x, which is the calculus-level reason for the monotonic climb. But the property also holds by a more elementary identity: cosh(y) minus cosh(x) equals 2 times sinh((y+x)/2) times sinh((y-x)/2), a product of two positive terms when 0 is at most x and x is less than y.

In Recognition Science, the framework's machine-checked library of formal theorems records this monotonicity as the theorem cosh_strictMono_on_nonneg. The framework models reality as maintaining a ledger, a discrete record of recognition events, and assigns each scale a cost via the function J(x) = (x + 1/x)/2 - 1. That cost function is built from the same exponential average as cosh, so the strict climb of cosh on nonnegative inputs becomes a tool for comparing costs. The theorem itself is a pure statement about real numbers: for any x and y with 0 at most x and x less than y, the inequality cosh(x) < cosh(y) holds. The proof in the library derives it from the difference identity and the positivity of sinh on positive arguments, with no appeal to calculus or to any framework-specific axiom.

The theorem does not claim that cost itself is monotone in the closure level. In fact, the framework's library proves the opposite for the per-closure cost: J(1 + r) strictly decreases as the closure level k rises, so a higher-level ladder is cheaper than a lower-level one. The monotonicity of cosh is a local fact about the function on a half-line, not a global statement about the cost of ladders. It also does not assert anything about cosh on negative inputs, where the function is symmetric and decreasing toward 1. The theorem's reach is exactly the nonnegative half-line, and its role is to support comparisons of costs that are built from cosh, not to select any particular closure level.

/-- `cosh` is strictly monotone on `[0, ∞)`, from the difference identity
banked in `Cost.GeometricRoot`. -/
theorem cosh_strictMono_on_nonneg {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y) :
    Real.cosh x < Real.cosh y := by
  have h := Cost.GeometricRoot.cosh_sub_cosh x y
  have hA : 0 < Real.sinh ((y + x) / 2) := Cost.GeometricRoot.sinh_pos_of_pos (by linarith)
  have hB : 0 < Real.sinh ((y - x) / 2) := Cost.GeometricRoot.sinh_pos_of_pos (by linarith)
  have hpos : 0 < 2 * Real.sinh ((y + x) / 2) * Real.sinh ((y - x) / 2) := by
    positivity
  linarith

/-- `cosh` is strictly monotone on `[0, ∞)`, from the difference identity
banked in `Cost.GeometricRoot`. -/
theorem cosh_strictMono_on_nonneg {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y) :
    Real.cosh x < Real.cosh y := by
  have h := Cost.GeometricRoot.cosh_sub_cosh x y
  have hA : 0 < Real.sinh ((y + x) / 2) := Cost.GeometricRoot.sinh_pos_of_pos (by linarith)
  have hB : 0 < Real.sinh ((y - x) / 2) := Cost.GeometricRoot.sinh_pos_of_pos (by linarith)
  have hpos : 0 < 2 * Real.sinh ((y + x) / 2) * Real.sinh ((y - x) / 2) := by
    positivity
  linarith

/-- **Route-kill measurement.** The per-closure cost `J(1 + r)` is strictly
decreasing as the closure level rises: for any two closure ladders at
consecutive levels, the higher-level ladder has the cheaper closure.
Cost-minimization therefore does not select `k = 2`; it selects nothing
finite. This kills the sub-route "the J-cost excess selects the closure
level by minimization." -/
theorem closure_cost_strictly_decreasing {r s : ℝ} {k : ℕ}
    (hr : 1 < r) (hrc : 1 + r = r ^ (k + 2))
    (hs : 1 < s) (hsc : 1 + s = s ^ (k + 3)) :
    Cost.Jcost (1 + s) < Cost.Jcost (1 + r) := by
  have hsr : s < r := by
    by_contra h
    push_neg at h
    rcases lt_or_eq_of_le h with hlt | heq
    · -- r < s: strict monotonicity of the closure polynomial gives
      -- f_{k+3}(r) < f_{k+3}(s) = 0, but f_{k+3}(r) = r² - 1 > 0.
      have h1 : r ^ (k + 3) - r - 1 < s ^ (k + 3) - s - 1 :=
        closurePoly_strictMono (le_of_lt hr) hlt (by omega)
      have hfs : s ^ (k + 3) - s - 1 = 0 := by
        have e : s ^ (k + 3) = 1 + s := by rw [← hsc]
        linarith
      have hfr : r ^ (k + 3) - r - 1 = r ^ 2 - 1 := by
        have e0 : k + 3 = (k + 2) + 1 := by omega
        have e : r ^ (k + 3) = r * r ^ (k + 2) := by rw [e0, pow_succ']
        rw [e, ← hrc]
        ring
      nlinarith [h1, hfs, hfr, hr,
        mul_pos (sub_pos.mpr hr) (by linarith : (0 : ℝ) < r + 1)]
    · -- r = s: then r^{k+2} = r^{k+3}, impossible.
      rw [← heq] at hsc
      have e1 : r ^ (k + 2) = r ^ (k + 3) := by rw [← hrc, ← hsc]
      have := pow_inj_right hr e1
      omega
  have hlog : Real.log (1 + s) < Real.log (1 + r) :=
    Real.log_lt_log (by linarith) (by linarith)
  have hc : Real.cosh (Real.log (1 + s)) < Real.cosh (Real.log (1 + r)) :=
    cosh_strictMono_on_nonneg (Real.log_nonneg (by linarith)) hlog
  have e1 : Cost.Jcost (1 + s) = Real.cosh (Real.log (1 + s)) - 1 :=
    Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (by linarith)
  have e2 : Cost.Jcost (1 + r) = Real.cosh (Real.log (1 + r)) - 1 :=
    Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (by linarith)
  linarith [e1, e2, hc]

What this page does not claim

The theorem does not claim that the cost function J is monotone in the closure level. It does not assert any property of cosh on negative inputs. It does not select a particular closure level for the golden ratio ladder.

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/PhiClosureSelection.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: