ZeroCompositionWitness
A structure that combines an abstract d'Alembert-type functional law H with the normalization condition H(2(Re ρ - 1/2)) = 1 for a complex point ρ. Researchers pursuing Vector C routes to the Riemann hypothesis would cite this interface when constructing bridges from phase data. It is introduced as a bare record type with no attached proof.
claimLet $ρ ∈ ℂ$. A witness consists of a map $H:ℝ→ℝ$ obeying the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, with $H(0)=1$, continuous, second derivative $H''(0)=1$, together with the evaluation $H(2(Re ρ - 1/2))=1$.
background
The module isolates an abstract interface for Vector C routes, classified as alternate and not on the primary path to unconditional RH. It asks whether completed-ξ data can instantiate a zero-location observable that forces the critical line, but notes that pure FE symmetry plus RCL doubling data cannot succeed. ZeroCompositionLaw is the required abstract structure: a function H with H(0)=1, continuity, the d'Alembert relation, curvature condition deriv(deriv H)0=1, and regularity hypotheses. The shifted cost H(x)=J(x)+1 reparametrizes the Recognition Composition Law into standard d'Alembert form. zeroDeviation(ρ) extracts twice the real-part offset of ρ from the critical line in log-coordinate scale.
proof idea
The declaration is a structure definition with no proof body. It simply records the supplied law together with the evaluation condition at the deviation point for use in downstream forcing theorems.
why it matters in Recognition Science
It is used by zeroCompositionWitness_forces_on_critical_line and VectorCChargeZeroBridge, which feed direct_rh_from_honestPhaseChargeZeroBridge. The module documentation states that this interface turns a zero-location observable into critical-line forcing, yet sibling results prove that pure Vector C doubling data cannot produce such a witness and that extra Euler/Hadamard analytic input is required. It touches the open question of whether honest zeta-derived phase data can close the Vector C route.
scope and limits
- Does not instantiate the witness with concrete zeta zero data.
- Does not derive the d'Alembert law from first principles.
- Does not apply outside the NumberTheory domain.
- Does not resolve the extra analytic input requirement shown by sibling no-go results.
formal statement (Lean)
86structure ZeroCompositionWitness (ρ : ℂ) where
87 law : ZeroCompositionLaw
88 value_at_deviation : law.H (zeroDeviation ρ) = 1
89
90/-- Any such witness forces the corresponding point onto the critical line. -/