zeroFreeCriterion_of_honestPhaseCostBridge

formal source

 171
 172/-- Therefore a bounded-cost bridge for honest phase data already yields a full
 173analytic `ZeroFreeCriterion`, independently of Vector C. -/
 174noncomputable def zeroFreeCriterion_of_honestPhaseCostBridge
 175    (hb : HonestPhaseCostBridge) :
 176    ZeroFreeCriterion where
 177  logDeriv_bounded_on_strip := fun _ hσ => carrierDerivBound_pos hσ
 178  carrier_nonvanishing_on_strip := fun _ hσ => carrier_nonvanishing hσ
 179  honest_phase_family := honest_argument_principle_phase_family
 180  charge_zero_of_honest_phase := charge_zero_of_honest_phase_of_costBridge hb
 181
 182/-- Consequently any honest-phase bounded-cost bridge proves RH through the
 183existing analytic route. -/
 184theorem direct_rh_from_honestPhaseCostBridge (hb : HonestPhaseCostBridge) :
 185    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False :=
 186  rh_from_zero_free_criterion (zeroFreeCriterion_of_honestPhaseCostBridge hb)
 187
 188/-! ### §4b'. Route C bottleneck — exact current analytic state -/
 189
 190/-- Honest zeta phase data already has bounded excess, but bounded total cost
 191is equivalent to zero charge.  This records the exact Route C bottleneck:
 192the perturbative/excess estimate is complete; the missing analytic content is
 193the upgrade from bounded excess to zero charge (or an equivalent admissibility
 194principle). -/
 195theorem honestPhase_routeC_bottleneck (zfd : ZetaPhaseFamilyData) :
 196    RealizedDefectAnnularExcessBounded (zfd.phaseFamily.toSampledFamily) ∧
 197      (RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily) ↔
 198        zfd.sensor.charge = 0) :=
 199  ⟨honestPhaseFamily_excess_bounded zfd,
 200    honestPhaseFamily_cost_bounded_iff_charge_zero zfd⟩
 201
 202/-- A direct charge-zero bridge for honest zeta phase data.  This is weaker
 203and cleaner than asking for bounded total cost: it states exactly the charge
 204conclusion needed by the analytic route. -/