Foundation Existence Uniqueness From Cost Jcost Log Symmetric

The cost symmetry

In the Recognition Science framework, a cost is a measure of how far a positive number is from 1, the point of no recognition cost. The declaration jcost_log_symmetric proves a simple but powerful property: for any positive number x, the cost of x equals the cost of its reciprocal, 1/x. In symbols, J(x) = J(1/x). This means the cost function treats a number and its inverse identically, a symmetry that is not assumed but derived from the framework's founding principles.

This symmetry has a concrete interpretation. If the cost measures the effort of recognizing one quantity relative to another, then the cost of recognizing a ratio is the same whether you read it forward or backward. The cost of recognizing 2 relative to 1 is the same as recognizing 1 relative to 2. The theorem is a formal statement in the framework's machine-checked library of formal theorems, proved with no unverified assumptions, and it is a direct consequence of the cost function's definition.

The symmetry is one of several properties that together guarantee the cost function has exactly one minimum. The framework proves that the only positive number with zero cost is 1 itself, and that any other positive number has strictly positive cost. This uniqueness is what the framework calls the existence and uniqueness of the recognition point: there is exactly one point of no cost, and it is the identity. The symmetry theorem supports this by showing the cost function is well-behaved under inversion, a necessary step in the full argument.

What the theorem does not claim is broader. It does not say that the cost function is the only one with this symmetry, nor does it establish the full form of the cost function. The theorem is a single, precise statement about a specific function, not a claim about all possible cost functions. It is a building block in a larger structure, not the structure itself.

/-- J-cost is symmetric in log-ratio sense. -/
theorem jcost_log_symmetric {x : ℝ} (hx : 0 < x) :
    Jcost x = Jcost x⁻¹ := Jcost_symm hx

/-- The cost-zero set is exactly {1}. -/
theorem cost_zero_set_singleton :
    ∀ x : ℝ, 0 < x → (Jcost x = 0 ↔ x = 1) := by
  intro x hx
  constructor
  · intro h
    by_contra hne
    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  · rintro rfl; exact Jcost_unit0

/-- Away from 1, J-cost is strictly positive (isolation). -/
theorem jcost_isolated_from_zero {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
    0 < Jcost x := Jcost_pos_of_ne_one x hx hne

What this page does not claim

This theorem does not prove that the cost function is the only one with this symmetry. This theorem does not establish the full functional form of the cost function, only one of its properties. This theorem does not claim anything about the physical meaning of the cost beyond its mathematical definition.

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