Foundation Jcost Convexity In Log Space G At Zero

The fixed point in log space

In the Recognition Science framework, a ledger (a discrete record of recognition events) assigns a cost to every positive ratio x between two magnitudes. The cost function J(x) is built so that recognizing something as identical to itself costs nothing: J(1) = 0. The declaration g_at_zero restates that fact after a change of variables. Instead of writing the cost as a function of the ratio x, write t = ln x, the natural logarithm of the ratio. Define g(t) = J(e^t). Then the theorem g_at_zero proves, in the framework's machine-checked library of formal theorems, that g(0) = 0. In plain words: when the log-ratio is zero, meaning the ratio is exactly 1, the cost is exactly zero. That is the fixed point of the cost in logarithmic coordinates.

The same library also proves two companion facts about g. It is even, g(t) = g(-t), which says the cost of a ratio and its reciprocal are the same, and it is strictly positive away from zero, so the only place the cost vanishes is at t = 0. These three facts together describe the shape of the cost near its minimum. The framework also defines a simple comparison function h(t) = t²/2, the log-ratio form, and proves that g and h share the same fixed point, the same even symmetry, and the same sign pattern. That shared structure is what the internal note calls convexity in log space, and it is the reason the log-ratio form is a natural approximation near the fixed point.

What g_at_zero does not claim is just as precise as what it proves. It does not say that g(t) equals t²/2 everywhere; the theorem only establishes the shared fixed point, symmetry, and positivity, not equality of the two functions. The approximation g(t) ≈ t²/2 is stated in the internal note as a near-t behavior, not as a theorem of the library. The declaration also says nothing about the uniqueness of J, which is a separate result in the framework, and nothing about any physical interpretation of the cost beyond the formal definition. The lemma is a single, narrow stone in the foundation, not the whole arch.

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

/-- 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 theorem does not claim g(t) equals t²/2 for all t, only that they share a fixed point, symmetry, and sign pattern. The declaration says nothing about the uniqueness of the cost function J, which is a separate theorem in the framework. The lemma carries no physical interpretation of the cost beyond its formal definition as a function of a ratio.

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: