law_of_logic_forces_jcost_of_contDiff
plain-language theorem explainer
Under normalization, the Recognition Composition Law, calibration, and C² regularity of the shifted cost H, any admissible cost F on the positive reals equals the canonical J-cost (x+x⁻¹)/2−1. Reciprocal symmetry is derived rather than assumed. Anyone citing the sharpened T5 uniqueness surface under ContDiff hypotheses will use this. The proof reduces the composition law to a d'Alembert equation for H, solves it by the C² cosh uniqueness lemma, and matches calibration.
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ be normalized, satisfy the Recognition Composition Law, and be calibrated, and suppose the shifted cost $H_F:=G_F+1$ is $C^2$. Then for every $x>0$, $F(x)=J(x)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the canonical reciprocal cost.
background
The module ContDiffReduction tightens the T5 regularity seam: on a $C^2$ surface, normalization, composition, and calibration alone force the canonical reciprocal cost, with reciprocity derived rather than postulated.
The Recognition Composition Law (RCL) is the functional equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Passing to the shifted cost $H=G+1$ (equivalently $H(x)=J(x)+1=\frac12(x+x^{-1})$ in the multiplicative picture) converts RCL into the classical d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ in additive log coordinates. Normalization fixes $H(0)=1$; calibration fixes the second derivative at the origin, $H''(0)=1$.
The upstream lemma dAlembert_cosh_solution_of_contDiff states that any $C^2$ solution of d'Alembert with $H(0)=1$ and $H''(0)=1$ equals $\cosh$. The canonical cost is $J(x)=\cosh(\log x)-1$ on $x>0$, which is exactly T5's unique J-cost from the forcing chain.
proof idea
Fix $x>0$. Write $G_F$ and $H_F=G_F+1$ for the log-coordinate cost and its shift. Convert the composition-law hypothesis to the cosh-addition form via composition_law_equiv_coshAdd, then to the direct additive identity for $G_F$.
From that identity, a short ring calculation yields the d'Alembert equation for $H_F$. Normalization gives $H_F(0)=1$. Calibration gives $(G_F)''(0)=1$; since $H_F=G_F+1$, the second derivatives agree, so $H_F''(0)=1$.
Apply dAlembert_cosh_solution_of_contDiff to conclude $H_F=\cosh$, hence $G_F=\cosh-1$. Compare with the known identity $G_J(\log x)=\cosh(\log x)-1$ and unwind $F(x)=G_F(\log x)$ along $x=e^{\log x}$ to obtain $F(x)=J(x)$.
why it matters
This is the sharpened T5 surface announced in the module: the law of logic (normalization + RCL + calibration) plus $C^2$ regularity of $H$ already forces the canonical reciprocal cost, without assuming reciprocity a priori. It sits at landmark T5 of the forcing chain (J-uniqueness, $J(x)=\cosh(\log x)-1$), and feeds the broader claim that the Recognition Composition Law selects a unique cost functional once mild analytic hypotheses are fixed.
The module's three advances are realized here in one theorem: ContDiff d'Alembert solutions obey $H''=H$; RCL plus normalization force reciprocity; therefore on the ContDiff surface the canonical $J$ follows from normalization, composition, and calibration alone. No downstream consumers are wired yet (used_by is empty), so this is presently a terminal uniqueness lemma ready for import into the UnifiedForcingChain or any T5 closure argument that wants the ContDiff route rather than a stronger smoothness package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.