rh_from_zero_free_criterion
plain-language theorem explainer
A ZeroFreeCriterion, packaging bounded log-derivative on the strip, carrier nonvanishing for real parts above 1/2, and an honest phase-family map for nonzero-charge sensors, directly forces every witnessed defect sensor to have zero charge. Analysts working the pure analytic route to the Riemann Hypothesis in Recognition Science cite this as the terminal converter from criterion to global statement. The proof is a short term-mode reduction that extracts the phase family and applies the charge-zero lemma for honest phases.
Claim. Let $Z$ be a zero-free criterion consisting of bounded logarithmic derivative of the carrier on the critical strip, nonvanishing of the carrier for real parts greater than $1/2$, and an honest phase-family assignment that maps each nonzero-charge witnessed defect sensor to zeta-phase family data. Then for every witnessed defect sensor $s$, the assumption that the charge of $s$ is nonzero yields a contradiction.
background
The Analytic Trace module assembles an axiom-free RH bridge from carrier infrastructure. Former axioms (zero winding from holomorphy and argument-principle forcing of charge zero) have been replaced by proved results such as contourWinding and the floor-coverage iff charge-zero theorem. A ZeroFreeCriterion is the structure that packages the remaining honest analytic target: witnessed zeta-inverse defect data in the strip, with fields for bounded log-derivative, carrier nonvanishing, and honest phase family.
proof idea
Assume a sensor with nonzero charge. Apply the honest_phase_family field of the criterion to obtain zeta-phase family data. Invoke the charge_zero_of_honest_phase lemma on that data to conclude the charge equals zero. The resulting equality contradicts the nonzero-charge hypothesis.
why it matters
This theorem is the central converter for the pure analytic route, feeding every direct_rh_from_* bridge (honestPhaseCostBridge, vectorC, honestPhaseAdmissibility, EBBA) into the global charge-zero statement. It completes the module's contribution of carrier-side infrastructure that eliminates prior axioms and targets a ZeroFreeCriterion from honest phase data. In the Recognition framework it closes the analytic estimates to the global defect-charge condition without invoking the cost-framework contradiction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.