Encyclopedia Cost Jcost

ARTICLE 2 claims 2 theorems

Jcost

The expression (x + 1/x)/2 - 1 charges every positive ratio x, vanishing only at x = 1 and treating x and 1/x alike.

Verify this page

The price of a ratio

Every positive number can be read as a ratio between two amounts. The expression J(x) = (x + 1/x)/2 - 1 turns that ratio into a price: zero when x = 1, positive for every other x, and unchanged when x is replaced by 1/x. The same price, 0.25, applies to 2 and to 1/2. Near x = 1 the price is approximately (x - 1)^2/2, so a small mismatch is paid quadratically, while for large x the price grows like x/2.

The substitution x = e^t brings out an underlying symmetry: J(e^t) = cosh t - 1, where hyperbolic cosine cosh t = (e^t + e^{-t})/2. Adding 1 turns that identity into the classical d'Alembert functional equation: H(t+u) + H(t-u) = 2H(t)H(u) with H(t) = cosh t. The equation carries d'Alembert's name from 18th-century analysis. Continuity, H(0) = 1, the d'Alembert equation, and a second derivative of 1 at 0 force H(t) = cosh t.

In Recognition Science, this function is called the recognition cost function. A ledger is a discrete record of events; a recognition is an event in which the ledger registers a ratio x between two amounts, and the cost of registering that ratio is what J charges. The framework's central theorem states that J is the only possible cost function of this kind. Any function on positive reals that is reciprocal-symmetric, normalized to zero at 1, obeys the composition law, is calibrated, and is continuous must be J. The composition law links the cost of xy and x/y to the costs of x and y; calibration fixes the second derivative at 1 to 1. The proof is checked in the framework's library, a collection of formal theorems verified by the the formal library 4 proof assistant.

One concrete value anchors the function in the framework's mathematics: at the golden ratio phi = (1 + sqrt 5)/2, J(phi) = phi - 3/2, a positive number. The useful consequence is the uniqueness theorem itself. Any proposed cost function can be settled by checking the five conditions; if they all hold, the formula is decided.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean
law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean:1104 
/-- **Law of Logic cost theorem**: The J-cost function is the unique
    reciprocal cost satisfying the RCL, normalization, calibration, and continuity.

    This version uses the global Aczél axiom internally and requires NO regularity
    hypothesis parameters from the caller. -/
theorem law_of_logic_forces_jcost (F : ℝ → ℝ)
    [AczelSmoothnessPackage]
    (hRecip : IsReciprocalCost F)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F)
    (hCalib : IsCalibrated F)
    (hCont : ContinuousOn F (Set.Ioi 0)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  intro x hx
  have hSymm : ∀ {y}, 0 < y → F y = F y⁻¹ := fun {y} hy => hRecip y hy
  have hCoshAdd : CoshAddIdentity F := composition_law_equiv_coshAdd F |>.mp hComp
  let Gf : ℝ → ℝ := G F
  let Hf : ℝ → ℝ := H F
  have h_G0 : Gf 0 = 0 := G_zero_of_unit F hNorm
  have h_H0 : Hf 0 = 1 := by
    show H F 0 = 1
    simp only [H, G, Real.exp_zero]
    rw [hNorm]; ring
  have h_G_cont : Continuous Gf := by
    have h := ContinuousOn.comp_continuous hCont continuous_exp
    have h' : Continuous (fun t => F (Real.exp t)) :=
      h (by intro t; exact Set.mem_Ioi.mpr (Real.exp_pos t))
    simp [Gf, G] at h'
    exact h'
  have h_H_cont : Continuous Hf := by
    simpa [Hf, H] using h_G_cont.add continuous_const
  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
    intro t u
    have hG := h_direct t u
    have h_goal : (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
      calc (Gf (t + u) + 1) + (Gf (t - u) + 1)
          = (Gf (t + u) + Gf (t - u)) + 2 := by ring
        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
    simp [Hf, H, Gf] at h_goal
    exact h_goal
  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
    have hG_d2 : deriv (deriv Gf) 0 = 1 := by simpa [Gf, G] using hCalib
    have hderiv : deriv Hf = deriv Gf := by
      funext t; change deriv (fun y => Gf y + 1) t = deriv Gf t
      exact (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
    dAlembert_cosh_solution_aczel Hf h_H0 h_H_cont h_dAlembert h_H_d2
  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := fun t => by
    have : Gf t + 1 = Real.cosh t := h_H_cosh t
    linarith
  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
    Jcost_G_eq_cosh_sub_one (Real.log x)
  calc F x
      = F (Real.exp (Real.log x)) := by rw [ht]
    _ = Gf (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
    _ = G Cost.Jcost (Real.log x) := by simp only [hJG]
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by simp [ht]
THEOREM dAlembert_cosh_solution_aczel · IndisputableMonolith/Cost/FunctionalEquation.lean
dAlembert_cosh_solution_aczel · IndisputableMonolith/Cost/FunctionalEquation.lean:1082 
/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.

    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
theorem dAlembert_cosh_solution_aczel
    [AczelSmoothnessPackage]
    (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_cont : Continuous H)
    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
    (h_d2_zero : deriv (deriv H) 0 = 1) :
    ∀ t, H t = Real.cosh t := by
  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
  have hDiff : Differentiable ℝ H :=
    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
  have h_ode : ∀ t, deriv (deriv H) t = H t :=
    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0

What this page does not claim

No claim that the five conditions are themselves derived rather than assumed as the framework's axioms. No claim that a smaller set of conditions, for instance reciprocal symmetry alone, forces J. No claim that the uniqueness theorem identifies any physical process as a recognition event; the physical bridge is open.

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/Cost/FunctionalEquation.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND