wallpaperJ

formal source

 146
 147/-- **Wallpaper J-cost.** The genuine `Cost.Jcost` evaluated on the
 148symmetry ratio, replacing the v4 placeholder `wallpaper_J_cost := orbit_count`. -/
 149def wallpaperJ (g : WallpaperGroup) : ℝ :=
 150  Cost.Jcost (symmetryRatio g)
 151
 152theorem wallpaperJ_nonneg (g : WallpaperGroup) :
 153    0 ≤ wallpaperJ g :=
 154  Cost.Jcost_nonneg (symmetryRatio_pos g)
 155
 156/-- **THEOREM.** `p6m` sits at the J-cost floor `J = 0`. -/
 157theorem wallpaperJ_p6m_eq_zero : wallpaperJ .p6m = 0 := by
 158  unfold wallpaperJ
 159  rw [symmetryRatio_p6m]
 160  exact Cost.Jcost_unit0
 161
 162/-- For any non-`p6m` group whose ratio is not `1`, J-cost is strictly
 163positive. The technical content is `Jcost x = (x-1)²/(2x) > 0` when
 164`x ≠ 1`. -/
 165theorem wallpaperJ_pos_of_ne_one {g : WallpaperGroup}
 166    (h : symmetryRatio g ≠ 1) : 0 < wallpaperJ g := by
 167  unfold wallpaperJ
 168  have hx_pos : 0 < symmetryRatio g := symmetryRatio_pos g
 169  have hx_ne : symmetryRatio g ≠ 0 := ne_of_gt hx_pos
 170  rw [Cost.Jcost_eq_sq hx_ne]
 171  have h_sq_pos : 0 < (symmetryRatio g - 1) ^ 2 := by
 172    have h_diff : symmetryRatio g - 1 ≠ 0 := sub_ne_zero.mpr h
 173    positivity
 174  have h_den_pos : 0 < 2 * symmetryRatio g := by linarith
 175  positivity
 176
 177/-- The trivial-symmetry group `p1` has strictly positive J-cost. -/
 178theorem wallpaperJ_p1_pos : 0 < wallpaperJ .p1 := by
 179  apply wallpaperJ_pos_of_ne_one