theorem proved term proof

`canonicalDefectSampledFamily_sensor`

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

formal statement (Lean)

 101theorem canonicalDefectSampledFamily_sensor (sensor : DefectSensor)
 102    (hm : sensor.charge ≠ 0) :
 103    (canonicalDefectSampledFamily sensor hm).sensor = sensor :=

proof body

Term-mode proof.

 104  chosenDefectPhaseFamily_sensor sensor hm
 105
 106/-- Every mesh in the canonical sampled family has the requested sensor charge. -/

used by (4)

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

canonicalDefectSampledFamily_charge in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
defect_annular_cost_bounded_inconsistent in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
defect_bounded_impossible in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
realizedDefectCollapseBoundaryApproaching_of_nonzero_charge in IndisputableMonolith.Unification.UnifiedRH decl_use

depends on (7)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
canonical in IndisputableMonolith.Foundation.ArithmeticOf decl_use
canonical in IndisputableMonolith.Gap45.Beat decl_use
canonical in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
canonicalDefectSampledFamily in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
chosenDefectPhaseFamily_sensor in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use