ZeroCompositionWitness
plain-language theorem explainer
ZeroCompositionWitness records a d'Alembert function H obeying the zero-composition law together with the normalization H(2(Re ρ − 1/2)) = 1. Researchers pursuing Vector C bridges to the Riemann hypothesis cite this interface to convert zeta phase data into critical-line forcing. The declaration is a structure definition that simply packages the law instance and the evaluation predicate.
Claim. Let $H : ℝ → ℝ$ satisfy $H(0) = 1$, continuity, the d'Alembert identity $H(t+u) + H(t-u) = 2 H(t) H(u)$, and $H''(0) = 1$. A witness at a complex point $ρ$ consists of such an $H$ together with the condition $H(2(ℜ(ρ) − 1/2)) = 1$.
background
The module isolates an abstract interface needed by Vector C routes. ZeroCompositionLaw requires a function $H$ with $H(0)=1$, continuity, the d'Alembert equation, curvature condition $H''(0)=1$, and regularity hypotheses. The shifted cost from CostAlgebra is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$, under which the Recognition Composition Law becomes the standard d'Alembert equation. zeroDeviation($ρ$) = 2($ρ$.re − 1/2) expresses the real deviation from the critical line in log coordinates. The module is classified ALTERNATE and states that pure FE symmetry plus RCL doubling cannot produce such a witness.
proof idea
This is a structure definition that records an instance of ZeroCompositionLaw together with the predicate that the associated $H$ evaluates to 1 at zeroDeviation $ρ$. No lemmas or tactics are invoked; the declaration serves only as a record type for downstream arguments.
why it matters
The structure supplies the exact data that VectorCChargeZeroBridge must produce from honest phase data to close the analytic RH route. It is the input to zeroCompositionWitness_forces_on_critical_line and zeroCompositionWitness_forces_zero_defect, which derive that any witness places $ρ$ on the critical line and forces zero defect. The module records the stage-gate result that pure Vector C symmetry data is insufficient and that extra Euler/Hadamard analytic input is required.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.