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

not_costDivergent_of_charge_zero

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)

 327theorem not_costDivergent_of_charge_zero (sensor : DefectSensor)
 328    (hzero : sensor.charge = 0) :
 329    ¬ CostDivergent sensor := by

proof body

Tactic-mode proof.

 330  intro hdiv
 331  obtain ⟨N, hN⟩ := hdiv 1
 332  let mesh : AnnularMesh N := uniformChargeMesh N sensor.charge
 333  have hcost : 1 < annularCost mesh := by
 334    exact hN mesh (by intro n; rfl)
 335  have hexcess_zero : annularExcess mesh = 0 := by
 336    simpa [mesh, hzero] using uniformChargeMesh_excess_zero N sensor.charge
 337  have hfloor_zero : annularTopologicalFloor N mesh.charge = 0 := by
 338    simpa [mesh, hzero] using (annularTopologicalFloor_zero N)
 339  have hcost_zero : annularCost mesh = 0 := by
 340    unfold annularExcess at hexcess_zero
 341    rw [hfloor_zero] at hexcess_zero
 342    linarith
 343  have hfalse : ¬ (1 < (0 : ℝ)) := by norm_num
 344  exact hfalse (by simpa [hcost_zero] using hcost)
 345
 346/-- Any cost-divergent sensor must have nonzero charge. -/

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.