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

color_offset_eq_quark_baseline

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)

 194theorem color_offset_eq_quark_baseline : color_offset = quark_baseline := rfl

proof body

Term-mode proof.

 195
 196/-! ## B-14: Generation torsion ordering 0 < E_pass < W
 197
 198The three generations have torsion offsets {0, E_pass, W}.
 199The ordering 0 < E_pass < W is a consequence of cube arithmetic:
 200E_pass = E − 1 = D·2^(D−1) − 1 and W = E_pass + F = E_pass + 2D.
 201Since F = 2D > 0, we have W > E_pass.
 202Since D ≥ 1 implies E ≥ 1, we have E_pass ≥ 0; for D ≥ 2, E_pass > 0. -/
 203
 204/-- **B-14 DERIVED**: Generation torsion is strictly ordered. -/

depends on (25)

Lean names referenced from this declaration's body.