generation_ordering_general

formal source

 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
 236/-! ## B-26: Completeness condition for Z-map polynomial
 237
 238For the charge index Z(Q̃) = aQ̃² + bQ̃⁴ to produce a valid ordered
 239hierarchy (distinct Z values for distinct |Q̃|), the polynomial must be
 240strictly increasing for Q̃ > 0. This requires a > 0 and b > 0.
 241Combined with integerization (a, b ∈ ℕ), this gives a ≥ 1, b ≥ 1.
 242
 243The minimal solution is (a, b) = (1, 1). -/
 244
 245/-- Z-map polynomial for the charge index. -/