zeroCompositionLaw_forces_eta_zero
plain-language theorem explainer
A zero-composition law forces a complex point ρ onto the critical line precisely when the cost function H attains the value 1 at the deviation of ρ. Researchers exploring Vector C routes to the Riemann hypothesis would cite this interface result. The equivalence is obtained by composing the unique-minimum property of the law with the zero-deviation characterization of the critical line.
Claim. Let $H : ℝ → ℝ$ satisfy the zero-composition law axioms ($H(0)=1$, continuity, d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$, second derivative at zero equal to 1, and regularity hypotheses). For any complex number ρ, $H(δ(ρ))=1$ if and only if ρ lies on the critical line, where δ(ρ) denotes the deviation observable.
background
The module isolates an abstract interface for zero-composition laws in an alternate Vector C approach to the Riemann hypothesis. A ZeroCompositionLaw is a structure supplying a function H:ℝ→ℝ with H(0)=1, continuity, the d'Alembert equation, curvature condition deriv(deriv H)0=1, and associated regularity hypotheses. This H is the shifted cost from the Recognition Science framework, where H(x)=J(x)+1 and J satisfies the Recognition Composition Law, turning the latter into the standard d'Alembert form. The module is classified ALTERNATE and notes that pure functional-equation symmetry plus RCL data cannot produce a witness; extra Euler/Hadamard analytic input is required.
proof idea
The term proof uses constructor to split the biconditional. The forward direction applies zeroCompositionLaw_forces_unique_minimum to obtain zeroDeviation ρ=0 from the assumption H(zeroDeviation ρ)=1, then invokes zeroDeviation_eq_zero_iff_on_critical_line. The reverse direction runs the same two lemmas in opposite order.
why it matters
This supplies the forcing step for the alternate Vector C path and is invoked directly by the downstream theorem zeroCompositionWitness_forces_on_critical_line, which concludes that any concrete witness places the point on the critical line. The module is marked ALTERNATE with a stage gate (April 2026) showing that pure FE symmetry cannot instantiate the interface, so any successful path must import the same extra analytic data used by primary routes. It touches the open question of whether completed-ξ data can realize the ZeroCompositionLaw.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.