generation_ordering

formal source

 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
 221      have hd1 : 1 ≤ d - 1 + 1 := by omega
 222      calc d * 2 ^ (d - 1) ≥ 2 * 2 ^ (2 - 1) := by
 223              apply Nat.mul_le_mul hd (Nat.pow_le_pow_right (by norm_num) (by omega))
 224            _ = 4 := by norm_num
 225            _ ≥ 2 := by norm_num
 226    omega
 227  · unfold cube_faces
 228    omega
 229
 230/-- W_endo(D) = E_pass(D) + F(D) — the endogenous wallpaper count. -/
 231def W_endo (d : ℕ) : ℕ := passive_field_edges d + cube_faces d
 232
 233/-- At D = 3: W_endo = 11 + 6 = 17 = wallpaper_groups. -/
 234theorem W_endo_at_D3 : W_endo D = wallpaper_groups := by native_decide
 235