Foundation Jcost Convexity In Log Space

The shape of cost in log space

The cost function, the price a recognition event pays, is J(x) = (x + 1/x)/2 - 1. It has a unique minimum at x = 1, where J(1) = 0. In log coordinates, writing t = ln(x), the cost becomes g(t) = J(e^t). This change of variables is not cosmetic: it reveals a convex, symmetric shape. The function g satisfies g(0) = 0, g(t) = g(-t), and g(t) > 0 for t ≠ 0. The simple quadratic h(t) = t²/2 shares all three properties. The module proves these facts in a machine-checked library of formal theorems.

The structural identity is that J(x) and ½(ln x)² belong to the same cost family. Both have the same fixed point at x = 1, the same symmetry J(x) = J(x⁻¹), and the same sign pattern: zero at the fixed point, positive elsewhere. Near t = 0, the approximation g(t) ≈ t²/2 holds, so the log-ratio form is the local shape of the cost. The module packages these shared properties into a certificate structure, a formal object that records the fixed point, symmetry, and positivity of both functions.

This convexity in log space is what makes the cost tractable for control. A closed-loop system that minimizes cost can treat the log-ratio as a target shape: the unique minimum at x = 1 is an attractor, and the even symmetry means deviations above and below the fixed point are penalized equally. The module does not derive the cost function itself; it takes J as given and proves the log-space structure that follows. The theorems are axiom-clean, with no unproven assumptions in the library.

/-- g(0) = J(e⁰) = J(1) = 0. -/
theorem g_at_zero : g 0 = 0 := by
  unfold g
  simp [Jcost_unit0]

/-- g is even: g(t) = g(-t). -/
theorem g_even (t : ℝ) : g t = g (-t) := by
  unfold g
  rw [Real.exp_neg]
  exact Jcost_symm (Real.exp_pos t)

/-- g(t) > 0 for t ≠ 0. -/
theorem g_pos_off_zero {t : ℝ} (ht : t ≠ 0) : 0 < g t := by
  unfold g
  apply Jcost_pos_of_ne_one
  · exact Real.exp_pos t
  · intro h
    have : t = 0 := by
      have hexp := h
      rw [← Real.log_exp t] at hexp
      simp [Real.log_one] at hexp ⊢
      exact Real.log_exp t ▸ hexp
    exact ht this

theorem h_at_zero : h 0 = 0 := by simp [h]

theorem h_pos_off_zero {t : ℝ} (ht : t ≠ 0) : 0 < h t := by
  unfold h; positivity

/-- g and h share the same fixed point at t = 0. -/
theorem same_fixed_point : g 0 = 0 ∧ h 0 = 0 := ⟨g_at_zero, h_at_zero⟩

/-- Both g and h are even functions. -/
theorem same_symmetry : ∀ t, g t = g (-t) ∧ h t = h (-t) :=
  fun t => ⟨g_even t, h_even t⟩

What this page does not claim

The module does not derive the cost function J from first principles. The approximation g(t) ≈ t²/2 is not an equality except at t = 0. The convexity result does not imply the cost function is globally quadratic in x.

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