ZeroCompositionLaw
plain-language theorem explainer
The ZeroCompositionLaw structure encodes the minimal functional equation and regularity conditions on a real function H that any zero-location observable must satisfy to participate in Vector C arguments. Number theorists exploring alternate routes to the Riemann hypothesis via composition laws would cite this interface when checking whether zeta-zero data can instantiate it. The definition directly packages the d'Alembert equation together with the curvature normalization and the suite of smoothness hypotheses drawn from Aczél's theorem andODE
Claim. A map $H : {R} {to} {R}$ satisfies the zero-composition law when $H(0) = 1$, $H$ is continuous, it obeys the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, the second derivative satisfies $H''(0) = 1$, and the four regularity hypotheses hold that guarantee continuous solutions are smooth and satisfy the ODE $H'' = H$.
background
In Recognition Science the shifted cost is defined by $H(x) = J(x) + 1$, where $J$ is the J-cost appearing in the Recognition Composition Law. Under this change of variable the RCL becomes the classical d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The upstream lemma dAlembert_continuous_implies_smooth_hypothesis records Aczél's theorem that continuous solutions normalized by $H(0)=1$ are analytic and of the form cosh($lambda t$).
proof idea
The declaration is a structure definition that bundles the functional equation, the curvature condition, and the four named regularity hypotheses; no proof is required. The hypotheses are taken verbatim from the Cost.FunctionalEquation module, where dAlembert_continuous_implies_smooth_hypothesis encodes Aczél's theorem, dAlembert_to_ODE_hypothesis encodes the derivation of $H''=H$, and the remaining three close the regularity bootstrap for the linear ODE.
why it matters
This interface supplies the exact contract used by the downstream theorems zeroCompositionLaw_forces_cosh, zeroCompositionLaw_forces_unique_minimum and zeroCompositionLaw_forces_eta_zero to conclude that any such $H$ equals cosh and attains its minimum value 1 only at the origin. The module documentation states that Vector C requires genuinely extra Euler/Hadamard analytic input beyond pure functional-equation symmetry, and that the April 2026 gate VectorCSymmetryOnlyNoGo already shows pure RCL data cannot produce a ZeroCompositionWitness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.