delta_1_structure

formal source

 101/-- First-order curvature correction. -/
 102def delta_1 : ℝ := -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension)
 103
 104theorem delta_1_structure :
 105    delta_1 = -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension) :=
 106  rfl
 107
 108theorem delta_1_numerator : (curvature_numerator : ℕ) = 103 := curvature_numerator_eq
 109theorem delta_1_denominator_nat : (face_wallpaper_pairs : ℕ) = 102 := face_wallpaper_pairs_eq
 110theorem delta_1_power : measure_dimension = 5 := measure_dimension_eq
 111
 112/-- δ₁ is negative (the curvature correction subtracts). -/
 113theorem delta_1_neg : delta_1 < 0 := by
 114  unfold delta_1
 115  have hnum : (0 : ℝ) < (curvature_numerator : ℝ) := by
 116    simp [curvature_numerator, face_wallpaper_pairs, Q3_faces, wallpaper_groups, active_edges]
 117  have hfwp : (0 : ℝ) < (face_wallpaper_pairs : ℝ) := by
 118    simp [face_wallpaper_pairs, Q3_faces, wallpaper_groups]
 119  have hden : (0 : ℝ) < (face_wallpaper_pairs : ℝ) * π ^ measure_dimension :=
 120    mul_pos hfwp (pow_pos pi_pos _)
 121  exact div_neg_of_neg_of_pos (neg_neg_of_pos hnum) hden
 122
 123/-! ## n-fold Configuration Space -/
 124
 125/-- The number of ordered n-fold face-wallpaper configurations. -/
 126def n_fold_configs (n : ℕ) : ℕ := face_wallpaper_pairs ^ n
 127
 128theorem n_fold_configs_1 : n_fold_configs 1 = 102 := rfl
 129theorem n_fold_configs_2 : n_fold_configs 2 = 10404 := by native_decide
 130
 131/-- The Q₃ automorphism group order (for symmetry reduction). -/
 132def Q3_aut_order : ℕ := 48
 133
 134/-- Symmetry-reduced configuration count (upper bound). -/