Encyclopedia Cost Reciprocal Cost

ARTICLE 4 claims 3 theorems 1 model

Reciprocal Cost

Reciprocal cost is the unique mismatch price that treats a ratio and its inverse the same, then combines products by one fixed rule.

Verify this page

Definition

Reciprocal cost is a function F on positive reals that prices mismatch under two structural demands. First, F(x) equals F(1/x): the price of a ratio does not depend on which side is treated as the base. Second, products and quotients combine under a single composition identity. Under those demands, and after one local scale fix at the identity, the only continuous solution is J(x) = (x + 1/x)/2 − 1. That formula is not a decorative choice. It is the object every later ratio in the theory inherits.

In log coordinates the composition identity becomes d'Alembert's functional equation, a classical equation whose even continuous solutions are hyperbolic cosine (up to the scale fix). The reciprocal symmetry is what makes the solution even. The scale fix, written as unit log-curvature at the origin, kills the constant branch and selects cosh. Translating back to the original variable recovers J. The chain that carries this selection is machine-checked under a regularity package; the public anchor is the forcing theorem that concludes F equals J on the positive reals.

What this does not settle is the origin of the scale fix itself. The number that sets curvature to 1 is an input, not a derived constant. Everything downstream that uses J inherits that input. The definition of reciprocal cost therefore has a sharp split: the shape of the function is forced, and the scale that names which cosh solution is chosen remains a model choice until a deeper derivation closes it.

THEOREM IsReciprocalCost · IndisputableMonolith/Cost/FunctionalEquation.lean
IsReciprocalCost · IndisputableMonolith/Cost/FunctionalEquation.lean:623 
/-- **Definition 2.1 (Reciprocal Cost)**
A function F : ℝ₊ → ℝ is a reciprocal cost if F(x) = F(1/x) for all x > 0. -/
def IsReciprocalCost (F : ℝ → ℝ) : Prop :=
  ∀ x : ℝ, 0 < x → F x = F x⁻¹
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 composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean
composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean:1301 
/-- **The cost theorem on two premises.** The composition law and unit log
curvature force `F = J` on the positives. Normalization, nonnegativity, and
continuity are all conclusions rather than hypotheses; compare
`law_of_logic_forces_jcost`, which assumes all of them. -/
theorem composition_logCurvature_forces_jcost [AczelSmoothnessPackage]
    (F : ℝ → ℝ)
    (hComp : SatisfiesCompositionLaw F)
    (hκ : HasLogCurvature (H F) 1) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  have hNorm : IsNormalized F := logCurvature_forces_normalized F hComp hκ
  have hN : F 1 = 0 := hNorm
  have hH0 : H F 0 = 1 := by simp [H, G, hN]
  have hCosh : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have hdA : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u := by
    intro t u
    have hG := hCosh t u
    have hgoal :
        (G F (t + u) + 1) + (G F (t - u) + 1) =
          2 * (G F t + 1) * (G F u + 1) := by
      calc
        (G F (t + u) + 1) + (G F (t - u) + 1)
            = (G F (t + u) + G F (t - u)) + 2 := by ring
        _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
        _ = 2 * (G F t + 1) * (G F u + 1) := by ring
    simpa [H] using hgoal
  have hcont : Continuous (H F) :=
    dAlembert_continuous_of_log_curvature (H F) hH0 hdA hκ
  have hsm : ContDiff ℝ ⊤ (H F) := aczel_dAlembert_smooth (H F) hH0 hcont hdA
  have heven : Function.Even (H F) := dAlembert_even (H F) hH0 hdA
  have hd0 : deriv (H F) 0 = 0 :=
    even_deriv_at_zero (H F) heven
      (hsm.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) 0)
  have hd2 : deriv (deriv (H F)) 0 = 1 :=
    deriv2_of_logCurvature (H F) hsm hH0 hd0 hκ
  have hcosh : ∀ t, H F t = Real.cosh t :=
    dAlembert_cosh_solution_aczel (H F) hH0 hcont hdA hd2
  intro x hx
  have hGc : G F (Real.log x) = Real.cosh (Real.log x) - 1 := by
    have h := hcosh (Real.log x)
    simp only [H] at h
    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]
    _ = G F (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := hGc
    _ = 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]
MODEL HasLogCurvature · IndisputableMonolith/Cost/FunctionalEquation.lean
HasLogCurvature · IndisputableMonolith/Cost/FunctionalEquation.lean:156 
/-- The paper's log curvature `κ(F) = lim_{t→0} 2 F(e^t)/t²`, stated on the
**punctured** filter.

The puncture is not cosmetic. On the full filter `nhds 0` this predicate is
unsatisfiable for every nonzero `κ`: Lean's division is total with `x / 0 = 0`,
so the quotient takes the value `0` at `t = 0`, and convergence along a filter
that contains the point pins the value at the point. The repo carried the
full-filter reading until 2026-07-25, which silently made two results vacuous;
`hasLogCurvature_full_filter_forces_zero` keeps that from recurring quietly. -/
def HasLogCurvature (H : ℝ → ℝ) (κ : ℝ) : Prop :=
  Filter.Tendsto (fun t => 2 * (H t - 1) / t^2)
    (nhdsWithin (0 : ℝ) ({(0 : ℝ)}ᶜ)) (nhds κ)

What this page does not claim

That the calibration value 1 is forced by reciprocity and composition alone. That every possible combining rule for recognition events is ruled out. That the page names a physical experiment that measures J directly.

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