theorem proved term proof

`charges_distinct`

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

formal statement (Lean)

 124theorem charges_distinct : Q_tilde_up ≠ Q_tilde_down := by native_decide

Term-mode proof.

 125
 126/-- The larger charge gets the larger span.
 127    |Q̃_up| = 4 > |Q̃_down| = 2, so span_up = 24 > span_down = 14. -/

Lean names referenced from this declaration's body.