wallpaperJ_pos_of_ne_one

formal source

 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
 180  unfold symmetryRatio orbitCount maxOrbitCount
 181  norm_num
 182
 183/-- `p6m` strictly minimizes wallpaper J-cost over the seventeen groups
 184(strict for any group whose ratio is not `1`). -/
 185theorem wallpaperJ_p6m_le (g : WallpaperGroup) :
 186    wallpaperJ .p6m ≤ wallpaperJ g := by
 187  rw [wallpaperJ_p6m_eq_zero]
 188  exact wallpaperJ_nonneg g
 189
 190/-! ## §3. Anti-monotonicity of J-cost in symmetry ratio (on `[r, 1]`) -/
 191
 192/-- For ratios `x, y ∈ (0, 1]` with `x ≤ y`, the J-cost is monotone
 193*decreasing* in the ratio. This is the statement "more symmetric → lower
 194J-cost" on the relevant domain. Proof: on `(0, 1]`, `Jcost x = (x-1)²/(2x)`
 195is monotone decreasing because both `(x-1)²` decreases and `1/(2x)`