theorem proved term proof

`linking_iff_D3`

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

formal statement (Lean)

 122theorem linking_iff_D3 (D : ℕ) :
 123    0 < independent_charge_count D ↔ D = 3 := by

Term-mode proof.

 124  simp [independent_charge_count]; split <;> omega
 125
 126/-- Charge count = face pairs = colors = generations. -/

Lean names referenced from this declaration's body.

Charge in IndisputableMonolith.Constants.RSNativeUnits decl_use
independent_charge_count in IndisputableMonolith.Foundation.TopologicalConservation decl_use