theorem proved term proof

`physical_sensor_charge_zero`

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

formal statement (Lean)

 947theorem physical_sensor_charge_zero (ps : PhysicalSensor) :
 948    ps.val.charge = 0 :=

proof body

Term-mode proof.

 949  (ontological_dichotomy ps.val).mpr ps.property
 950
 951/-- **RH from the ontological dichotomy.**  If every sensor physically exists,
 952then every sensor has charge `0`. -/

used by (1)

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

charge_zero_unconditional in IndisputableMonolith.NumberTheory.RH_Certificate decl_use

depends on (4)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
ontological_dichotomy in IndisputableMonolith.Unification.UnifiedRH decl_use
PhysicalSensor in IndisputableMonolith.Unification.UnifiedRH decl_use