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

charge_zero_of_honest_phase_of_costBridge

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)

 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

proof body

Tactic-mode proof.

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

used by (1)

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

depends on (17)

Lean names referenced from this declaration's body.