composition_law_forces_reciprocity
plain-language theorem explainer
Normalized functions satisfying the composition law are necessarily reciprocal. Researchers deriving T5 J-uniqueness in the Recognition Science forcing chain cite this result. The proof shifts to the H-function to convert the law into the d'Alembert equation, invokes evenness, and equates values at log x and its negative via the exponential substitution.
Claim. Let $F : (0,∞) → ℝ$ be normalized with $F(1) = 0$ and satisfy the composition law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for $x,y > 0$. Then $F(x) = F(x^{-1})$ for all $x > 0$.
background
The shifted cost is $H_F(x) = J(x) + 1 = ½(x + x^{-1})$, under which the Recognition Composition Law becomes the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The module addresses ContDiff reduction for T5: a $C^2$ d'Alembert solution satisfies the ODE $H'' = H$, and the RCL plus normalization already force reciprocity. Therefore the canonical reciprocal cost follows from normalization, composition, and calibration alone.
proof idea
Define Hf := H F and obtain Hf(0) = 1 from normalization. Apply composition_law_equiv_coshAdd to reach CoshAddIdentity, then CoshAddIdentity_implies_DirectCoshAdd to obtain the direct form on G F. Algebraic expansion and ring simplification yield the d'Alembert equation for Hf. Evenness follows from dAlembert_even. Specializing at t = log x and using exp_log and exp_neg produces F(x) + 1 = F(x^{-1}) + 1, from which reciprocity follows by linarith.
why it matters
This closes a central step in the T5 J-uniqueness argument of the forcing chain (T0-T8) by showing reciprocity is forced by the RCL and normalization without extra regularity. It supports the module claim that on the ContDiff surface the canonical reciprocal cost follows from normalization, composition, and calibration alone, and feeds the uniqueness result for C² solutions. It directly ties the RCL to the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.