zeroCompositionLaw_forces_unique_minimum
plain-language theorem explainer
A zero-composition law forces the observable H to attain its minimum value of 1 uniquely at deviation t = 0. Analysts exploring Vector C routes to the Riemann hypothesis would cite this uniqueness result when calibrating zero-location observables. The proof reduces the claim to the standard characterization of cosh via a single rewrite step.
Claim. Let $H : ℝ → ℝ$ satisfy the zero-composition law: $H(0) = 1$, $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, with second derivative at zero equal to 1 and the listed regularity hypotheses. Then $H(t) = 1$ if and only if $t = 0$.
background
The ZeroCompositionLaw structure abstracts the functional properties required for a zero-location observable. It consists of a map H obeying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u), normalized so H(0) = 1, with curvature condition (deriv (deriv H)) 0 = 1 and regularity hypotheses ensuring smoothness from the ode and continuous hypotheses.
proof idea
The term proof first invokes zeroCompositionLaw_forces_cosh to rewrite zc.H t as the cosh expression in t. It then applies the standard identity cosh_eq_one_iff, which states that cosh(s) = 1 precisely when s = 0.
why it matters
This theorem supplies the uniqueness step needed by the downstream result zeroCompositionLaw_forces_eta_zero, which concludes that the observable attaining its minimum forces the complex point onto the critical line. It fills a slot in the alternate Vector C path, where the module documentation notes that pure functional-equation symmetry plus RCL doubling data cannot produce a ZeroCompositionWitness. The result relies on the d'Alembert form of the Recognition Composition Law but does not advance the primary T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.