rh_from_zero_free_criterion

formal source

 129        sensor.charge = 0
 130
 131/-- A `ZeroFreeCriterion` gives the RH directly. -/
 132theorem rh_from_zero_free_criterion (zfc : ZeroFreeCriterion) :
 133    ∀ (sensor : WitnessedDefectSensor), sensor.charge ≠ 0 → False := by
 134  intro sensor hm
 135  obtain ⟨zfd, hzfd, hfamily⟩ := zfc.honest_phase_family sensor hm
 136  have hzero : sensor.charge = 0 :=
 137    zfc.charge_zero_of_honest_phase sensor ⟨zfd, hzfd, hfamily⟩
 138  exact hm hzero
 139
 140/-! ### §4b. Vector C insertion point -/
 141
 142/-- A minimal Euler/Hadamard-side bridge for the honest analytic route.
 143
 144The current code already supplies perturbation control, and the present honest
 145sampled family has exact zero excess. The remaining bridge is to show that the
 146honest sampled family also has bounded total annular cost. Once that is known,
 147the general defect-cost theorem forces zero charge immediately. -/
 148structure HonestPhaseCostBridge where
 149  cost_bounded_of_honest_phase :
 150    ∀ (sensor : WitnessedDefectSensor) (zfd : ZetaPhaseFamilyData),
 151      zfd.sensor = sensor.toDefectSensor →
 152        RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily)
 153
 154/-- Any honest-phase cost bridge discharges the sole remaining analytic
 155charge-zero target. -/
 156theorem charge_zero_of_honest_phase_of_costBridge
 157    (hb : HonestPhaseCostBridge)
 158    (sensor : WitnessedDefectSensor)
 159    (hzfd : ∃ zfd : ZetaPhaseFamilyData,
 160      zfd.sensor = sensor.toDefectSensor ∧
 161        zfd.phaseFamily.sensor = sensor.toDefectSensor) :
 162    sensor.charge = 0 := by