color_offset_eq

formal source

 187/-- **B-25 DERIVED**: Color offset from face edge count. -/
 188def color_offset : ℕ := edges_per_face D
 189
 190theorem color_offset_eq : color_offset = 4 := by
 191  exact edges_per_face_at_D3
 192
 193/-- Color offset equals quark baseline (same geometric origin). -/
 194theorem color_offset_eq_quark_baseline : color_offset = quark_baseline := rfl
 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. -/
 205theorem generation_ordering :
 206    (0 : ℕ) < passive_field_edges D ∧
 207    passive_field_edges D < wallpaper_groups := by
 208  constructor
 209  · -- 0 < 11
 210    native_decide
 211  · -- 11 < 17
 212    native_decide
 213
 214/-- The ordering generalizes: for any D ≥ 2, 0 < E_pass(D) < W(D). -/
 215theorem generation_ordering_general (d : ℕ) (hd : 2 ≤ d) :
 216    0 < passive_field_edges d ∧
 217    passive_field_edges d < passive_field_edges d + cube_faces d := by
 218  constructor
 219  · unfold passive_field_edges cube_edges active_edges_per_tick
 220    have : d * 2 ^ (d - 1) ≥ 2 := by