zeroFreeCriterion_of_EBBA
plain-language theorem explainer
Given the Euler boundary bridge assumption, this definition constructs the zero-free criterion for the analytic route to the Riemann hypothesis by first deriving the honest phase cost bridge and then extracting the criterion structure. Researchers closing RH from ontology assumptions would cite it to confirm both direct and analytic paths are satisfied simultaneously. The construction is a one-line composition of two upstream definitions.
Claim. Let $B$ be the Euler boundary bridge assumption. Then there exists a zero-free criterion consisting of: the carrier logarithmic derivative bounded above zero for all real parts greater than $1/2$; the carrier non-vanishing in that half-plane; and, for every witnessed defect sensor with non-zero charge, an honest phase family whose data matches the sensor.
background
The Analytic Trace module builds an axiom-free interface to the Riemann hypothesis from sampled Euler carriers and phase data. Former axioms on winding and charge are replaced by proved statements: contour winding vanishes under holomorphy plus non-vanishing, and floor coverage holds exactly when charge is zero. Two routes remain: the ontology route via the Euler boundary bridge assumption imported from UnifiedRH, and the pure analytic route that targets a ZeroFreeCriterion built from honest phase cost bounds.
proof idea
This is a one-line wrapper. It applies honestPhaseCostBridge_of_EBBA to the input bridge, then feeds the resulting honest phase cost bridge into zeroFreeCriterion_of_honestPhaseCostBridge. The extractor populates the three fields of the criterion using the proved carrier derivative bound, the non-vanishing lemma on the strip, and the honest argument principle phase family constructor.
why it matters
The declaration supplies the analytic-route input required by direct_rh_from_EBBA_via_analytic, which obtains a contradiction for any witnessed sensor with non-zero charge directly from the ontology bridge. It demonstrates that the Euler boundary bridge assumption closes both the ontology and analytic paths at once. In the module this completes the axiom-free assembly of the analytic trace interface and links to the unification result in UnifiedRH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.