`HonestPhaseCostBridge`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.AnalyticTrace
domain: NumberTheory
line: 148 · 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 148.

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

 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
 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σ

papers checked against this theorem

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