Foundation Jcost Convexity In Log Space G Pos Off Zero

The cost stays positive

In the Recognition Science framework, the cost of a recognition event is measured by a function J(x). The variable x is the ratio between the new state and the old state, so x = 1 means nothing changed. The framework's central theorem proves that this cost function must take the specific form J(x) = (x + 1/x)/2 - 1. A natural way to study this function is to switch to logarithmic coordinates, writing t = ln(x). In these coordinates, the cost becomes g(t) = J(e^t), and the point x = 1 becomes t = 0.

The declaration g_pos_off_zero establishes a simple fact about this transformed cost function: for any nonzero value of t, the cost g(t) is strictly greater than zero. In plain language, the only input that costs nothing is t = 0, which corresponds to x = 1, the state of no change. Any departure from that state, no matter how small, carries a positive cost. The theorem is proved in the framework's machine-checked library of formal theorems, with no unproved assumptions, and it relies on two earlier results: the cost function is zero at x = 1, and it is positive for every x other than 1.

The same file also introduces the simpler function h(t) = t²/2, which is the quadratic approximation to g(t) near t = 0. The theorems prove that h shares three structural properties with g: both are zero at t = 0, both are even functions (symmetric about the vertical axis), and both are positive for all nonzero t. This comparison is what the internal note calls the log-ratio form: near the fixed point, the cost behaves like half the square of the logarithmic change. The two functions are not identical, but they agree in their fixed point, their symmetry, and their sign pattern.

What this declaration does not claim is just as important as what it proves. It does not claim that g(t) equals t²/2 exactly; the approximation is only near t = 0, and the full form of g comes from the original J(x). It also does not claim that g is convex in the sense of having a positive second derivative everywhere, even though the internal note's title mentions convexity. The formal theorems in the pack prove positivity, symmetry, and the shared fixed point, but convexity of g is not among the stated results. Finally, the declaration says nothing about why the cost function has this form; that is the job of the deeper forcing chain that derives J(x) from first principles.

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

/-- 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⟩

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

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

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

What this page does not claim

It does not claim that g(t) equals t²/2 exactly, only that they share a fixed point, symmetry, and sign pattern. It does not claim that g is convex in the sense of a positive second derivative; the pack proves positivity, not convexity. It does not claim to explain why the cost function has this form; the origin of J(x) belongs to the deeper forcing chain.

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: