zeroCompositionLaw_forces_cosh
plain-language theorem explainer
Any zero-composition law, defined by a function H with H(0)=1, continuity, the d'Alembert equation, and second derivative 1 at zero plus regularity conditions, must equal the hyperbolic cosine. Researchers exploring alternate Vector C routes to the Riemann hypothesis via zero-location observables would cite this interface result. The proof is a direct term-mode instantiation of the general d'Alembert-to-cosh theorem on the fields of the ZeroCompositionLaw structure.
Claim. Let $H:ℝ→ℝ$ satisfy $H(0)=1$, be continuous, obey the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and have second derivative equal to 1 at the origin (together with the associated regularity hypotheses). Then $H(t)=cosh(t)$ for all real $t$.
background
The ZeroCompositionLaw structure encodes an abstract functional equation for zero-location observables. It consists of a function H from reals to reals obeying H(0)=1, continuity, the d'Alembert relation H(t+u)+H(t-u)=2H(t)H(u), the curvature condition that the second derivative of H at 0 equals 1, and four regularity hypotheses (smooth, ODE, continuity, differentiability, bootstrap). The module is classified as alternate and isolates the exact interface Vector C would need to convert zero-location data into a critical-line forcing theorem. The key upstream result is the general d'Alembert_cosh_solution theorem, which already establishes that any d'Alembert law with this normalization and curvature must be the hyperbolic cosine.
proof idea
The proof is a one-line term-mode wrapper that applies the upstream theorem dAlembert_cosh_solution, passing the function H, the normalization H(0)=1, continuity, the d'Alembert equation, the curvature condition, and the four regularity hypotheses drawn directly from the ZeroCompositionLaw structure.
why it matters
This theorem forces any zero-composition law into the cosh form, which the downstream result zeroCompositionLaw_forces_unique_minimum then uses to conclude that the minimum value 1 occurs exactly at t=0. In the Recognition Science framework it links the Recognition Composition Law to the d'Alembert equation and to the J-uniqueness step of the forcing chain. The module documentation notes that this alternate path still requires extra Euler/Hadamard analytic input beyond functional-equation symmetry alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.