`HonestPhaseChargeZeroBridge`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.AnalyticTrace
domain: NumberTheory
line: 205 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.AnalyticTrace on GitHub at line 205.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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. -/
 205structure HonestPhaseChargeZeroBridge where
 206  charge_zero_of_honest_phase :
 207    ∀ zfd : ZetaPhaseFamilyData, zfd.sensor.charge = 0
 208
 209/-- A direct honest-phase charge-zero bridge discharges the `ZeroFreeCriterion`
 210charge-zero field. -/
 211theorem charge_zero_of_honest_phase_of_chargeZeroBridge
 212    (hb : HonestPhaseChargeZeroBridge)
 213    (sensor : WitnessedDefectSensor)
 214    (hzfd : ∃ zfd : ZetaPhaseFamilyData,
 215      zfd.sensor = sensor.toDefectSensor ∧
 216        zfd.phaseFamily.sensor = sensor.toDefectSensor) :
 217    sensor.charge = 0 := by
 218  rcases hzfd with ⟨zfd, hzsensor, _hzfamily⟩
 219  have hz : zfd.sensor.charge = 0 := hb.charge_zero_of_honest_phase zfd
 220  have hs : sensor.toDefectSensor.charge = 0 := by
 221    simpa [hzsensor] using hz
 222  simpa using hs
 223
 224/-- A direct charge-zero bridge gives a full `ZeroFreeCriterion`. -/
 225noncomputable def zeroFreeCriterion_of_honestPhaseChargeZeroBridge
 226    (hb : HonestPhaseChargeZeroBridge) :
 227    ZeroFreeCriterion where
 228  logDeriv_bounded_on_strip := fun _ hσ => carrierDerivBound_pos hσ
 229  carrier_nonvanishing_on_strip := fun _ hσ => carrier_nonvanishing hσ
 230  honest_phase_family := honest_argument_principle_phase_family
 231  charge_zero_of_honest_phase :=
 232    charge_zero_of_honest_phase_of_chargeZeroBridge hb
 233
 234/-- Any direct honest-phase charge-zero bridge proves the analytic RH core. -/
 235theorem direct_rh_from_honestPhaseChargeZeroBridge

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.