Foundation Jcost Convexity In Log Space Same Fixed Point

The shared fixed point

A cost function (a rule that assigns a nonnegative number to every possible state, measuring how far that state is from a preferred one) often has a fixed point: a state where the cost is exactly zero. For the Recognition Science framework's central cost, that state is the ratio x = 1, meaning no deviation from the reference. The declaration same_fixed_point concerns what happens when you switch to logarithmic coordinates, writing t = ln(x). In those coordinates, the cost becomes a function g(t) = J(e^t), and the fixed point x = 1 becomes t = 0.

The declaration proves a structural identity: both the original cost g(t) and the much simpler log-ratio function h(t) = t²/2 vanish at t = 0. In plain terms, the two functions share the same fixed point. The machine-checked theorem states this as the conjunction g(0) = 0 and h(0) = 0. It also proves that both functions are even, meaning g(t) = g(-t) and h(t) = h(-t), so they treat positive and negative deviations symmetrically. And it proves that both are positive away from zero, so the shared fixed point is not just a crossing but a unique minimum in each case.

The framework's library of formal theorems records these facts as g_at_zero, g_even, g_pos_off_zero, and their analogues for h, then packages them into the single certificate same_fixed_point. This certificate is what the framework uses when it wants to justify working with the simpler quadratic form t²/2 in place of the full cost, at least near the fixed point. The approximation g(t) ≈ t²/2 for small t is a separate claim, recorded in the internal note, not part of the certificate itself.

What the declaration does not claim is equally precise. It does not assert that g(t) equals h(t) for all t; the two functions agree at the fixed point and share symmetry and sign, but they are different functions elsewhere. It does not claim that the log-ratio form is the true cost, only that it shares these structural features. And it says nothing about how the framework derives the cost function itself; that is the work of the forcing theorem, not of this certificate.

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

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

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

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

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

theorem h_even (t : ℝ) : h t = h (-t) := by unfold h; ring

/-- 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_pos_off_zero {t : ℝ} (ht : t ≠ 0) : 0 < h t := by
  unfold h; positivity

What this page does not claim

The declaration does not claim g(t) equals h(t) for all t. The declaration does not claim the log-ratio form is the true cost function. The declaration does not derive the cost function itself; that is the forcing theorem's work.

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: