washburn_uniqueness_of_contDiff
Normalization, the composition law, calibration, and C² regularity of the shifted cost H already force F to equal the canonical Jcost on positive reals. Researchers closing the T5 uniqueness surface would cite this to derive reciprocal symmetry rather than assume it. The proof converts the composition law to the d'Alembert equation on H, obtains the initial conditions H(0)=1 and H''(0)=1, applies the cosh solution theorem, and matches via the log substitution.
claimLet $F : ℝ → ℝ$ be normalized, satisfy the composition law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$, be calibrated, and let $H = G + 1$ be twice continuously differentiable. Then $F(x) = J(x)$ for all $x > 0$, where $J(x) = cosh(log x) - 1$.
background
The module removes a central portion of the explicit T5 regularity seam. The shifted cost is defined by $H(x) = J(x) + 1$, which converts the Recognition Composition Law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The composition law on F is equivalent to the CoshAddIdentity on G via the substitution $x = e^s$, $y = e^t$ (composition_law_equiv_coshAdd). Upstream, dAlembert_cosh_solution_of_contDiff states that any C² solution of the d'Alembert equation with $H(0) = 1$ and $H''(0) = 1$ equals cosh.
proof idea
The proof first applies composition_law_equiv_coshAdd to obtain CoshAddIdentity, then CoshAddIdentity_implies_DirectCoshAdd. It extracts $H(0) = 1$ from normalization and the second-derivative condition at zero from calibration. The d'Alembert equation on H is derived by direct expansion of the cosh-add identity. dAlembert_cosh_solution_of_contDiff is invoked to conclude $H(t) = cosh t$, hence $G(t) = cosh t - 1$. The final step substitutes $t = log x$ for $x > 0$ and uses the identity $Jcost(exp t) = cosh t - 1$.
why it matters in Recognition Science
This sharpens the T5 surface by showing that normalization, composition, calibration, and C² regularity on H suffice to force the canonical reciprocal cost; reciprocal symmetry is derived. It closes part of the regularity seam for the J-uniqueness step in the forcing chain (T5), where $J(x) = cosh(log x) - 1$ is the self-similar fixed point. The result sits immediately below the main T5 uniqueness theorem and removes an explicit regularity hypothesis from earlier presentations.
scope and limits
- Does not establish the result for $x ot> 0$.
- Does not remove the C² regularity assumption on H.
- Does not derive the composition law from weaker axioms.
- Does not address functions that violate normalization or calibration.
formal statement (Lean)
189theorem washburn_uniqueness_of_contDiff
190 (F : ℝ → ℝ)
191 (hNorm : IsNormalized F)
192 (hComp : SatisfiesCompositionLaw F)
193 (hCalib : IsCalibrated F)
194 (h_diff : ContDiff ℝ 2 (H F)) :
195 ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
proof body
Tactic-mode proof.
196 intro x hx
197 let Gf : ℝ → ℝ := G F
198 let Hf : ℝ → ℝ := H F
199 have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
200 have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
201 have h_H0 : Hf 0 = 1 := by
202 dsimp [Hf]
203 simpa [H, G, IsNormalized] using hNorm
204 have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
205 intro t u
206 have hG := h_direct t u
207 have h_goal :
208 (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
209 calc
210 (Gf (t + u) + 1) + (Gf (t - u) + 1)
211 = (Gf (t + u) + Gf (t - u)) + 2 := by ring
212 _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simp [hG]
213 _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
214 simpa [Hf, H, Gf] using h_goal
215 have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
216 have hG_d2 : deriv (deriv Gf) 0 = 1 := by
217 simpa [Gf, G, IsCalibrated] using hCalib
218 have hderiv : deriv Hf = deriv Gf := by
219 funext t
220 change deriv (fun y => Gf y + 1) t = deriv Gf t
221 exact deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ))
222 have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
223 exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
224 have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
225 dAlembert_cosh_solution_of_contDiff Hf h_H0 h_dAlembert (by simpa [Hf] using h_diff) h_H_d2
226 have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
227 intro t
228 have hH := h_H_cosh t
229 have hH' : Gf t + 1 = Real.cosh t := by
230 simpa [Hf, H, Gf] using hH
231 linarith
232 have ht : Real.exp (Real.log x) = x := Real.exp_log hx
233 have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
234 Jcost_G_eq_cosh_sub_one (Real.log x)
235 calc
236 F x = F (Real.exp (Real.log x)) := by rw [ht]
237 _ = Gf (Real.log x) := rfl
238 _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
239 _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
240 _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
241 _ = Cost.Jcost x := by rw [ht]
242
243end
244
245end FunctionalEquation
246end Cost
247end IndisputableMonolith