pith. machine review for the scientific record. sign in
theorem proved tactic proof

charge_zero_of_honest_phase_of_vectorC

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.