Encyclopedia Cost Cost Cont Diff Reduction Law Of Logic Forces Jcost Of Cont Diff

ARTICLE 3 claims 3 theorems

Cost Cont Diff Reduction Law Of Logic Forces Jcost Of Cont Diff

A single forced formula governs the price of recognition; this theorem shows which assumptions are truly needed.

Verify this page

The cost function

In mathematics, a cost function assigns a number to each possible outcome, measuring the price of choosing it. The Recognition Science framework studies a particular kind of cost: one that measures the price of a recognition event, a discrete record of something being identified. The central question is whether the form of this cost is forced by a few natural conditions, or whether many different shapes are possible.

The framework's library, a machine-checked collection of formal theorems, proves a sharp answer. The declaration law_of_logic_forces_jcost_of_contDiff establishes that any cost function F satisfying four conditions must equal the specific formula J(x) = (x + 1/x)/2 - 1 for all positive x. The four conditions are: normalization (F(1) = 0), a composition law that fixes how costs combine, a calibration condition, and a smoothness condition called C² regularity, meaning the function has two continuous derivatives.

The theorem's force is that it removes an assumption. Earlier versions of the result required reciprocal symmetry, the condition that F(1/x) = F(x), as a separate input. This theorem shows that reciprocal symmetry is not needed as an assumption: it follows automatically from normalization, the composition law, and calibration alone, provided the function is smooth enough. The proof works by showing that a related function H = G + 1 satisfies a classical equation known as d'Alembert's functional equation, H(t+u) + H(t-u) = 2H(t)H(u), and that the smoothness condition forces H to be the hyperbolic cosine function.

What the theorem does not claim is equally important. It does not claim that the cost function is unique without the smoothness condition. Without C² regularity, the d'Alembert equation admits many pathological solutions that are not hyperbolic cosine, so the smoothness assumption is essential. The theorem also does not claim that the framework's other results, such as the golden ratio or three-dimensional space, follow from this declaration alone; those are separate theorems in the library. Finally, it does not claim that the cost function describes any physical system; it is a mathematical result about a specific class of functions.

THEOREM law_of_logic_forces_jcost_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
law_of_logic_forces_jcost_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:186 
/-- Sharpened T5 surface:
normalization, the composition law, calibration, and `C²` regularity of `H = G + 1`
already force the canonical reciprocal cost. Reciprocal symmetry is derived, not assumed. -/
theorem law_of_logic_forces_jcost_of_contDiff
    (F : ℝ → ℝ)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F)
    (hCalib : IsCalibrated F)
    (h_diff : ContDiff ℝ 2 (H F)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  intro x hx
  let Gf : ℝ → ℝ := G F
  let Hf : ℝ → ℝ := H F
  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  have h_H0 : Hf 0 = 1 := by
    dsimp [Hf]
    simpa [H, G, IsNormalized] using hNorm
  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
    simpa [Hf, H, Gf] using h_goal
  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
      simpa [Gf, G, IsCalibrated] 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_of_contDiff Hf h_H0 h_dAlembert (by simpa [Hf] using h_diff) h_H_d2
  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
    intro t
    have hH := h_H_cosh t
    have hH' : Gf t + 1 = Real.cosh t := by
      simpa [Hf, H, Gf] using hH
    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 simpa using hJG.symm
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by rw [ht]
THEOREM composition_law_forces_reciprocity · IndisputableMonolith/Cost/ContDiffReduction.lean
composition_law_forces_reciprocity · IndisputableMonolith/Cost/ContDiffReduction.lean:138 
/-- A normalized composition-law cost is automatically reciprocal. -/
theorem composition_law_forces_reciprocity
    (F : ℝ → ℝ)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F) :
    IsReciprocalCost F := by
  intro x hx
  let Hf : ℝ → ℝ := H F
  have h_H0 : Hf 0 = 1 := by
    dsimp [Hf]
    simpa [H, G, IsNormalized] using hNorm
  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have h_direct : DirectCoshAdd (G F) := 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 :
        (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 [Hf, H] using h_goal
  have h_even : Function.Even Hf := dAlembert_even Hf h_H0 h_dAlembert
  have h_even_at_log := h_even (Real.log x)
  have h_eq_plus :
      F x + 1 = F x⁻¹ + 1 := by
    simpa [Hf, H, G, Real.exp_log hx, Real.exp_neg] using h_even_at_log.symm
  linarith
THEOREM dAlembert_cosh_solution_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
dAlembert_cosh_solution_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:169 
/-- `C²` d'Alembert solutions are determined by calibration and equal `cosh`. -/
theorem dAlembert_cosh_solution_of_contDiff
    (Hf : ℝ → ℝ)
    (h_one : Hf 0 = 1)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf)
    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
    ∀ t, Hf t = Real.cosh t := by
  have h_ode : ∀ t, deriv (deriv Hf) t = Hf t :=
    dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
  have h_even : Function.Even Hf := dAlembert_even Hf h_one h_dAlembert
  have h_diff0 : DifferentiableAt ℝ Hf 0 :=
    (contDiffTwo_differentiable h_diff).differentiableAt
  have h_deriv_zero : deriv Hf 0 = 0 :=
    even_deriv_at_zero Hf h_even h_diff0
  exact ode_cosh_uniqueness_contdiff Hf h_diff h_ode h_one h_deriv_zero

What this page does not claim

The theorem does not claim uniqueness without the C² smoothness condition. The theorem does not claim that the framework's other results follow from this declaration alone. The theorem does not claim that the cost function describes any physical system.

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