zeroCompositionWitness_forces_zero_defect
plain-language theorem explainer
A concrete Vector C witness at a complex point ρ forces the zero-location defect attached to ρ to vanish. Researchers exploring the alternate Vector C route to the Riemann hypothesis would cite this interface result. The proof is a one-line application of the equivalence between vanishing defect and the critical line to the prior forcing of the critical line from the witness.
Claim. If a complex number ρ admits a concrete Vector C witness (a ZeroCompositionLaw together with the condition that its H function equals 1 at the zero deviation of ρ), then the RS defect attached to the zero-location deviation of ρ equals zero.
background
The Zero Composition Interface module isolates an abstract theorem interface that Vector C would need to convert a zero-location observable into a critical-line forcing result. It is classified as ALTERNATE and not on the primary path to unconditional RH; the module notes that any successful Vector C path must import extra Euler/Hadamard analytic input beyond pure functional-equation symmetry. A ZeroCompositionWitness for ρ is the structure consisting of a ZeroCompositionLaw and the equality law.H (zeroDeviation ρ) = 1. The zeroDefect of ρ is the defect from the LawOfExistence applied to exp(zeroDeviation ρ). Upstream results establish that any such witness forces ρ onto the critical line and that the defect vanishes exactly on the critical line.
proof idea
One-line wrapper that applies the right-to-left direction of zeroDefect_zero_iff_on_critical_line to the theorem zeroCompositionWitness_forces_on_critical_line.
why it matters
This declaration completes the Vector C interface by showing that a witness forces both the critical line and the vanishing of the attached defect. It fills the step described in the module doc-comment: 'Therefore the zero-location defect must vanish there as well.' The module documentation states that pure FE symmetry plus RCL data cannot produce a ZeroCompositionWitness, so this result touches the April 2026 stage gate requiring genuinely extra analytic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.