Encyclopedia Cost Cost Cont Diff Reduction Composition Law Forces Reciprocity

ARTICLE 3 claims 3 theorems

Cost Cont Diff Reduction Composition Law Forces Reciprocity

A single rule about how costs combine turns out to force a symmetry that was once assumed by hand.

Verify this page

The forced symmetry

A cost function, in plain terms, is a rule that assigns a price to a comparison: how much it costs to say two things are the same. In the Recognition Science framework, a ledger is a discrete record of such recognition events, and the cost is forced, not chosen. The classical question is whether the cost must be symmetric, meaning the price of comparing A to B equals the price of comparing B to A. The declaration composition_law_forces_reciprocity answers that question: yes, symmetry is not an assumption but a consequence of a more basic rule.

The more basic rule is the composition law, which says how the cost of a combined comparison relates to the costs of its parts. In symbols, a function F satisfies the law when F(x+y) + F(x−y) = 2F(x)F(y) for all real x and y, a d'Alembert-style equation that appears across mathematics, from wave motion to probability. The framework's theorem proves that if F is normalized (F(0) = 0 in the cost form) and satisfies this composition law, then F is automatically reciprocal: F(x) = F(1/x) for all positive x. This is the key step, because reciprocity is the symmetry that makes the cost function take its canonical form.

The proof uses a standard regularity assumption: the function is twice continuously differentiable, written C². Under that assumption, the composition law plus normalization forces the second derivative of the related function H = F + 1 to satisfy the differential equation H'' = H. The solutions to that equation are hyperbolic cosine, up to scaling, and hyperbolic cosine has the reciprocal property that cosh(t) = cosh(−t) in the right coordinates. The theorem is checked in the framework's machine-checked library of formal theorems, with no unverified axioms beyond the standard logical ones.

What this does not claim is just as important. The theorem does not say that every cost function must be reciprocal; it says that a cost function which already satisfies the composition law and normalization must be reciprocal. Without the composition law, reciprocity can fail. The theorem also does not derive the full canonical cost J(x) = (x + 1/x)/2 − 1 by itself; that requires an additional calibration condition, which fixes the scaling. The composition law forces the symmetry; calibration forces the specific form. These are separate results, and the declaration under discussion covers only the first.

The consequence for the framework is that a central symmetry falls out of a more primitive rule, rather than being put in by hand. That matters because the whole derivation of the golden ratio, the eight-tick cycle, and three spatial dimensions in Recognition Science rests on the cost function having this exact reciprocal form. If the symmetry had to be assumed, the derivation would be weaker; because it is forced, the chain of consequences is tighter. The reader can now see that the cost function's symmetry is not a free choice but a logical necessity, given the composition law and smoothness.

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_to_ODE_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
dAlembert_to_ODE_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:119 
/-- A `C²` d'Alembert solution with calibrated second derivative satisfies `H'' = H`. -/
theorem dAlembert_to_ODE_of_contDiff
    (Hf : ℝ → ℝ)
    (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, deriv (deriv Hf) t = Hf t := by
  intro t
  have h_rel := dAlembert_second_deriv_at_zero_of_contDiff Hf h_dAlembert h_diff t
  rw [h_deriv2_zero] at h_rel
  linarith
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]

What this page does not claim

The theorem does not apply to cost functions that fail the composition law. The theorem does not derive the canonical cost form without calibration. The theorem does not require or use the full set of five conditions from the main forcing theorem.

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