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

ordering_B_equal_ends

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)

 109theorem ordering_B_equal_ends :
 110    ordering_B_spans.1 = ordering_B_spans.2.2 := by native_decide

proof body

Term-mode proof.

 111
 112/-! ## Step 4: Charge Asymmetry Forces Ordering A
 113
 114The integerized charges are |Q̃_up| = 4 and |Q̃_down| = 2.
 115Since 4 ≠ 2, the up and down sectors are physically distinct.
 116Equal spans would imply charge-degenerate mass hierarchies.
 117
 118Ordering B (equal spans) is therefore excluded.
 119Ordering A (unequal spans) is forced. -/
 120

depends on (10)

Lean names referenced from this declaration's body.