zeroFreeCriterion_of_vectorC
plain-language theorem explainer
Researchers pursuing the pure analytic route to the Riemann hypothesis cite this definition to obtain a complete ZeroFreeCriterion once a Vector C bridge is available. It converts honest phase data into the required charge-zero implication without altering the criterion contract. The construction is a direct structure assembly that applies the carrier derivative bound, nonvanishing lemma, honest argument principle, and the bridge-specific charge-zero theorem.
Claim. Let $vc$ be a Vector C bridge. The zero-free criterion is the structure with logarithmic derivative bounded positively by the carrier derivative bound on the strip, carrier nonvanishing on the strip, honest phase family supplied by the honest argument principle, and charge zero of honest phase supplied by $vc$.
background
The Analytic Trace module assembles an axiom-free interface for the pure analytic RH route. Former axioms on winding and argument principle have been replaced by proved results on contour winding from holomorphy and floor coverage iff charge zero. A Vector C bridge is the structure that turns honest zeta-derived phase data into a ZeroCompositionWitness for the witnessed zero. The ZeroFreeCriterion packages the honest analytic target: witnessed zeta-reciprocal defect data in the strip yields an honest phase-family package whose analytic estimates force defect charge to vanish. This definition draws on the honest argument principle phase family theorem, which extracts a DefectPhaseFamily of charge exactly equal to multiplicity from the Euler quantitative factorization at any zero with real part exceeding one half.
proof idea
The definition constructs the ZeroFreeCriterion by direct field assignment. The logDeriv_bounded_on_strip field receives the carrierDerivBound_pos lemma. The carrier_nonvanishing_on_strip field receives the carrier_nonvanishing lemma. The honest_phase_family field receives the honest_argument_principle_phase_family theorem. The charge_zero_of_honest_phase field receives the charge_zero_of_honest_phase_of_vectorC theorem applied to the input bridge.
why it matters
This definition supplies the final link for the pure analytic route by producing a ZeroFreeCriterion from any Vector C bridge. It is invoked by the direct_rh_from_vectorC_bridge theorem, which feeds the result into rh_from_zero_free_criterion to obtain a contradiction from any nonzero-charge sensor. In the module setting the sampled Euler package carries budget zero and floor coverage holds exactly when charge vanishes. The construction realizes the analytic target stated in the module documentation and leaves open only the concrete instantiation of a Vector C bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.