`VectorCChargeZeroBridge`

definition

show as: view math explainer →

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

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

 245
 246Once this structure is instantiated, the existing analytic RH route closes
 247without any further changes to the `ZeroFreeCriterion` contract. -/
 248structure VectorCChargeZeroBridge where
 249  witness_of_honest_phase :
 250    ∀ (sensor : WitnessedDefectSensor),
 251      (∃ zfd : ZetaPhaseFamilyData,
 252        zfd.sensor = sensor.toDefectSensor ∧
 253          zfd.phaseFamily.sensor = sensor.toDefectSensor) →
 254        ZeroCompositionWitness sensor.rho
 255
 256/-- Any Vector C bridge discharges the sole open analytic target:
 257`charge_zero_of_honest_phase`. -/
 258theorem charge_zero_of_honest_phase_of_vectorC
 259    (vc : VectorCChargeZeroBridge)
 260    (sensor : WitnessedDefectSensor)
 261    (hzfd : ∃ zfd : ZetaPhaseFamilyData,
 262      zfd.sensor = sensor.toDefectSensor ∧
 263        zfd.phaseFamily.sensor = sensor.toDefectSensor) :
 264    sensor.charge = 0 := by
 265  have hline : OnCriticalLine sensor.rho :=
 266    zeroCompositionWitness_forces_on_critical_line
 267      (vc.witness_of_honest_phase sensor hzfd)
 268  have hcontr : False := by
 269    have hstrip : 1 / 2 < sensor.rho.re := sensor.in_strip.1
 270    have hre : sensor.rho.re = 1 / 2 := hline
 271    linarith
 272  exact False.elim hcontr
 273
 274/-- A successful Vector C bridge upgrades the proved Euler-carrier and honest
 275phase-family infrastructure into a complete `ZeroFreeCriterion`. -/
 276noncomputable def zeroFreeCriterion_of_vectorC
 277    (vc : VectorCChargeZeroBridge) :
 278    ZeroFreeCriterion where

papers checked against this theorem

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