theorem
proved
charge_zero_of_honest_phase_of_costBridge
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.AnalyticTrace on GitHub at line 156.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
bridge -
of -
phase -
cost -
cost -
of -
of -
for -
of -
HonestPhaseCostBridge -
ZeroFreeCriterion -
RealizedDefectAnnularCostBounded -
WitnessedDefectSensor -
honestPhaseFamily_charge_zero_of_costBounded -
ZetaPhaseFamilyData -
phase
used by
formal source
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
163 rcases hzfd with ⟨zfd, hzsensor, _hzfamily⟩
164 have hcost : RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily) :=
165 hb.cost_bounded_of_honest_phase sensor zfd hzsensor
166 have hzero_sensor : zfd.sensor.charge = 0 :=
167 honestPhaseFamily_charge_zero_of_costBounded zfd hcost
168 have hzero_base : sensor.toDefectSensor.charge = 0 := by
169 simpa [hzsensor] using hzero_sensor
170 simpa using hzero_base
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)