zeroCompositionWitness_forces_on_critical_line
plain-language theorem explainer
A ZeroCompositionWitness at complex point ρ forces ρ onto the critical line Re(s) = 1/2. Researchers building Vector C bridges to the Riemann hypothesis cite this as the interface forcing step. The proof is a one-line term application of the forward direction of zeroCompositionLaw_forces_eta_zero to the law and value fields of the witness.
Claim. Let ρ ∈ ℂ. Suppose there exists a zero-composition law H together with the condition H(zeroDeviation ρ) = 1. Then Re(ρ) = 1/2.
background
The module isolates an abstract interface that a Vector C construction would need to turn a zero-location observable into a critical-line forcing theorem. ZeroCompositionWitness ρ is the structure containing a ZeroCompositionLaw and the assertion that the law's functional H satisfies H(zeroDeviation ρ) = 1. OnCriticalLine ρ is the predicate ρ.re = 1/2. The upstream theorem zeroCompositionLaw_forces_eta_zero states that for any such law the minimum condition on the deviation is equivalent to the critical-line location.
proof idea
The proof is the one-line term (zeroCompositionLaw_forces_eta_zero w.law ρ).mp w.value_at_deviation, which extracts the left-to-right direction of the equivalence and feeds it the law and value_at_deviation fields of the witness.
why it matters
This supplies the critical-line forcing step inside the Vector C interface. It is invoked by zeroCompositionWitness_forces_zero_defect to conclude that the defect vanishes at ρ, and appears in the no-go theorem pureVectorCDoublingData_requires_extra_input and the bridge charge_zero_of_honest_phase_of_vectorC. The module classifies the whole interface as ALTERNATE and notes that any successful Vector C path must import extra Euler/Hadamard analytic input beyond pure functional-equation symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.