IndisputableMonolith.Aesthetics.SymmetryGroupPreference
IndisputableMonolith/Aesthetics/SymmetryGroupPreference.lean · 346 lines · 25 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Cost
4
5/-!
6# Visual Symmetry-Group Preference (Track A5 / E5)
7
8## Status: THEOREM (real derivation, replaces v4 SKELETON)
9
10This module replaces the v4 `IS_SKELETON` placeholder. The v4 file
11defined "wallpaper J-cost" as `orbit_count` (an integer cast to ℝ),
12which had nothing to do with `Cost.Jcost`. This file enumerates the
13seventeen wallpaper groups by their canonical generator-orbit
14multiplicity and defines the wallpaper J-cost as the genuine
15`Cost.Jcost` of the orbit-multiplicity ratio relative to the maximum
16symmetry orbit.
17
18## What we prove
19
20For each of the seventeen wallpaper groups we record `orbitCount g`,
21the orbit cardinality of the canonical fundamental domain under the
22full symmetry group action (the standard crystallographic count: p1
23has 1 orbit, p6m has 12, etc.). We define
24
25 `wallpaperJ g := Cost.Jcost (orbitCount g / maxOrbitCount)`
26
27where `maxOrbitCount = orbitCount p6m = 12`. This is the genuine
28J-cost of the orbit-multiplicity *ratio*, which lives on the positive
29reals and is reciprocal-symmetric (`J(x) = J(1/x)`).
30
31Headline theorems:
32
33* `wallpaperJ_p6m_eq_zero` — the maximum-symmetry group `p6m` sits at
34 J = 0 (the cost minimum), exactly because its ratio is `1`.
35* `wallpaperJ_nonneg` — every wallpaper group has non-negative
36 J-cost (from `Cost.Jcost_nonneg`).
37* `wallpaperJ_p1_pos` — the trivial-symmetry group `p1` has strictly
38 positive J-cost (because its ratio `1/12` is not `1`).
39* `wallpaperJ_mono_in_orbits` — for two groups whose orbit counts both
40 lie in `[1, maxOrbitCount]`, the higher-orbit group has lower J-cost
41 (preference orders symmetric over asymmetric).
42* `preference_p6m_max` — `p6m` is the universally maximally preferred
43 wallpaper group under the J-cost-derived preference functional.
44
45This is the structural content for the cross-cultural preference
46prediction (Washburn & Crowe 1988; Dietsch 2024). The numerical
47preference *order* over the seventeen groups is the empirical
48falsifier; the structural fact "preference is anti-monotone in
49J-cost-of-orbit-ratio with `p6m` at the floor" is the Lean theorem.
50
51## Falsifier
52
53A cross-cultural preference experiment whose ranking is incompatible
54with the J-cost ordering on the canonical `orbitCount` table below.
55In particular, any experiment that ranks `p1` (trivial symmetry,
56orbit ratio `1/12`) above `p6m` (maximum symmetry, orbit ratio `1`)
57falsifies the prediction.
58-/
59
60namespace IndisputableMonolith
61namespace Aesthetics
62namespace SymmetryGroupPreference
63
64open Constants Cost
65
66/-! ## §1. The seventeen wallpaper groups -/
67
68/-- The seventeen crystallographic wallpaper (plane-symmetry) groups,
69in IUC notation. The order listed here matches Schattschneider 1978
70and the standard crystallographic tables. -/
71inductive WallpaperGroup
72 | p1 | p2 | pm | pg | cm | pmm | pmg | pgg | cmm
73 | p4 | p4m | p4g | p3 | p3m1 | p31m | p6 | p6m
74 deriving DecidableEq, Repr
75
76/-- Canonical orbit count under the full symmetry-group action on the
77unit cell. These are the standard crystallographic orbit
78multiplicities (point-group order × 1 for the symmorphic groups; the
79non-symmorphic groups inherit the same orbit count from their point
80group on a fundamental domain that ignores the glide). -/
81def orbitCount : WallpaperGroup → ℕ
82 | .p1 => 1
83 | .p2 => 2
84 | .pm => 2
85 | .pg => 2
86 | .cm => 2
87 | .pmm => 4
88 | .pmg => 4
89 | .pgg => 4
90 | .cmm => 4
91 | .p4 => 4
92 | .p4m => 8
93 | .p4g => 8
94 | .p3 => 3
95 | .p3m1 => 6
96 | .p31m => 6
97 | .p6 => 6
98 | .p6m => 12
99
100/-- The maximum-symmetry group is `p6m` with twelve canonical orbits. -/
101def maxOrbitCount : ℕ := 12
102
103theorem orbitCount_p6m : orbitCount .p6m = maxOrbitCount := by
104 unfold orbitCount maxOrbitCount
105 rfl
106
107theorem orbitCount_pos : ∀ g : WallpaperGroup, 0 < orbitCount g := by
108 intro g; cases g <;> (unfold orbitCount; norm_num)
109
110theorem orbitCount_le_max : ∀ g : WallpaperGroup,
111 orbitCount g ≤ maxOrbitCount := by
112 intro g; cases g <;> (unfold orbitCount maxOrbitCount; norm_num)
113
114/-! ## §2. Symmetry ratio and J-cost -/
115
116noncomputable section
117
118/-- Symmetry ratio: `orbitCount g / maxOrbitCount ∈ (0, 1]`. -/
119def symmetryRatio (g : WallpaperGroup) : ℝ :=
120 (orbitCount g : ℝ) / (maxOrbitCount : ℝ)
121
122theorem symmetryRatio_pos (g : WallpaperGroup) :
123 0 < symmetryRatio g := by
124 unfold symmetryRatio
125 have h_num : (0 : ℝ) < (orbitCount g : ℝ) := by
126 exact_mod_cast orbitCount_pos g
127 have h_den : (0 : ℝ) < (maxOrbitCount : ℝ) := by
128 unfold maxOrbitCount; norm_num
129 positivity
130
131theorem symmetryRatio_p6m : symmetryRatio .p6m = 1 := by
132 unfold symmetryRatio
133 rw [orbitCount_p6m]
134 unfold maxOrbitCount
135 norm_num
136
137theorem symmetryRatio_le_one (g : WallpaperGroup) :
138 symmetryRatio g ≤ 1 := by
139 unfold symmetryRatio
140 have h_num : (orbitCount g : ℝ) ≤ (maxOrbitCount : ℝ) := by
141 exact_mod_cast orbitCount_le_max g
142 have h_den : (0 : ℝ) < (maxOrbitCount : ℝ) := by
143 unfold maxOrbitCount; norm_num
144 rw [div_le_one h_den]
145 exact h_num
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
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)`
196decreases as `x → 1`. -/
197theorem Jcost_anti_mono_on_unit_interval {x y : ℝ}
198 (hx : 0 < x) (hy : 0 < y) (hxy : x ≤ y) (hy1 : y ≤ 1) :
199 Cost.Jcost y ≤ Cost.Jcost x := by
200 have hx_ne : x ≠ 0 := ne_of_gt hx
201 have hy_ne : y ≠ 0 := ne_of_gt hy
202 rw [Cost.Jcost_eq_sq hx_ne, Cost.Jcost_eq_sq hy_ne]
203 -- Goal: (y-1)²/(2y) ≤ (x-1)²/(2x)
204 -- Equivalent: 2x · (y-1)² ≤ 2y · (x-1)² (multiplying by 2xy > 0)
205 rw [div_le_div_iff₀ (by linarith : (0:ℝ) < 2 * y) (by linarith : (0:ℝ) < 2 * x)]
206 -- Goal: (y-1)² · (2*x) ≤ (x-1)² · (2*y)
207 -- Both x, y are in (0, 1], so y-1 ≤ 0 and x-1 ≤ 0. Let a = 1-x ≥ 0, b = 1-y ≥ 0,
208 -- then b ≤ a (since x ≤ y means 1-y ≤ 1-x).
209 -- (y-1)² = b², (x-1)² = a², so we want 2x · b² ≤ 2y · a².
210 -- Equivalently: x · b² ≤ y · a².
211 -- Since b ≤ a and b² ≤ a², and x ≤ y, the product inequality follows.
212 set a := 1 - x with ha_def
213 set b := 1 - y with hb_def
214 have ha_nn : 0 ≤ a := by linarith
215 have hb_nn : 0 ≤ b := by linarith
216 have hba : b ≤ a := by linarith
217 have hxy' : x ≤ y := hxy
218 have hsq_nn : (1 - y) ^ 2 = b ^ 2 := by rw [hb_def]
219 have hsq_nn' : (1 - x) ^ 2 = a ^ 2 := by rw [ha_def]
220 have hyy_eq : (y - 1) ^ 2 = b ^ 2 := by rw [show (y - 1) = -(1 - y) from by ring]; ring
221 have hxx_eq : (x - 1) ^ 2 = a ^ 2 := by rw [show (x - 1) = -(1 - x) from by ring]; ring
222 rw [hyy_eq, hxx_eq]
223 -- Goal: b^2 * (2*x) ≤ a^2 * (2*y).
224 -- Use: b ≤ a (both nonneg) ⇒ b^2 ≤ a^2; and x ≤ y. Then b^2 * x ≤ a^2 * y.
225 have hb2_le_a2 : b ^ 2 ≤ a ^ 2 := by
226 have := mul_self_le_mul_self hb_nn hba
227 rw [pow_two, pow_two]; exact this
228 have hb2_nn : 0 ≤ b ^ 2 := by positivity
229 have ha2_nn : 0 ≤ a ^ 2 := by positivity
230 -- b^2 · (2x) ≤ a^2 · (2x) ≤ a^2 · (2y).
231 have step1 : b ^ 2 * (2 * x) ≤ a ^ 2 * (2 * x) :=
232 mul_le_mul_of_nonneg_right hb2_le_a2 (by linarith)
233 have step2 : a ^ 2 * (2 * x) ≤ a ^ 2 * (2 * y) :=
234 mul_le_mul_of_nonneg_left (by linarith) ha2_nn
235 linarith
236
237/-- **PREFERENCE ANTI-MONOTONICITY ON THE WALLPAPER LATTICE.** For two
238wallpaper groups, the one with strictly more orbits has lower J-cost
239(equivalently, higher preference). -/
240theorem wallpaperJ_mono_in_orbits {g h : WallpaperGroup}
241 (hgh : orbitCount g ≤ orbitCount h) :
242 wallpaperJ h ≤ wallpaperJ g := by
243 unfold wallpaperJ
244 apply Jcost_anti_mono_on_unit_interval
245 · exact symmetryRatio_pos g
246 · exact symmetryRatio_pos h
247 · -- Goal: symmetryRatio g ≤ symmetryRatio h
248 unfold symmetryRatio
249 have h_den_pos : (0 : ℝ) < (maxOrbitCount : ℝ) := by
250 unfold maxOrbitCount; norm_num
251 rw [div_le_div_iff₀ h_den_pos h_den_pos]
252 have : (orbitCount g : ℝ) ≤ (orbitCount h : ℝ) := by exact_mod_cast hgh
253 nlinarith
254 · exact symmetryRatio_le_one h
255
256/-! ## §4. Aesthetic preference functional -/
257
258/-- Aesthetic preference is the negation of J-cost: higher preference =
259lower cost. -/
260def preference (g : WallpaperGroup) : ℝ := - wallpaperJ g
261
262theorem preference_p6m_eq_zero : preference .p6m = 0 := by
263 unfold preference
264 rw [wallpaperJ_p6m_eq_zero]
265 ring
266
267/-- **THEOREM.** `p6m` is the universally maximally preferred
268wallpaper group under the J-cost-derived preference functional. -/
269theorem preference_p6m_max (g : WallpaperGroup) :
270 preference g ≤ preference .p6m := by
271 unfold preference
272 rw [wallpaperJ_p6m_eq_zero]
273 have := wallpaperJ_nonneg g
274 linarith
275
276/-- Anti-monotone in orbits: if `orbitCount g ≤ orbitCount h`, then
277preference for `g` is at most preference for `h`. -/
278theorem preference_anti_mono_in_orbits {g h : WallpaperGroup}
279 (hgh : orbitCount g ≤ orbitCount h) :
280 preference g ≤ preference h := by
281 unfold preference
282 have := wallpaperJ_mono_in_orbits hgh
283 linarith
284
285/-! ## §5. Master certificate -/
286
287/-- **SYMMETRY GROUP PREFERENCE MASTER CERTIFICATE.** Eight clauses
288backing the J-cost-driven cross-cultural preference prediction. All
289fields derived from `Cost.Jcost`, not asserted as orbit-count
290arithmetic.
291
2921. `orbit_pos`: every group has positive orbit count.
2932. `orbit_p6m_eq_max`: `p6m` orbit count = 12 = `maxOrbitCount`.
2943. `ratio_le_one`: every symmetry ratio is in `(0, 1]`.
2954. `J_nonneg`: every wallpaper J-cost is non-negative.
2965. `J_p6m_zero`: `p6m` sits at the J-cost floor.
2976. `J_p1_pos`: `p1` has strictly positive J-cost.
2987. `J_mono`: J-cost is anti-monotone in orbit count.
2998. `preference_p6m_max`: `p6m` maximizes preference.
300-/
301structure SymmetryGroupPreferenceCert where
302 orbit_pos : ∀ g, 0 < orbitCount g
303 orbit_p6m_eq_max : orbitCount .p6m = maxOrbitCount
304 ratio_le_one : ∀ g, symmetryRatio g ≤ 1
305 J_nonneg : ∀ g, 0 ≤ wallpaperJ g
306 J_p6m_zero : wallpaperJ .p6m = 0
307 J_p1_pos : 0 < wallpaperJ .p1
308 J_mono : ∀ {g h}, orbitCount g ≤ orbitCount h → wallpaperJ h ≤ wallpaperJ g
309 preference_p6m_max : ∀ g, preference g ≤ preference .p6m
310
311def symmetryGroupPreferenceCert : SymmetryGroupPreferenceCert where
312 orbit_pos := orbitCount_pos
313 orbit_p6m_eq_max := orbitCount_p6m
314 ratio_le_one := symmetryRatio_le_one
315 J_nonneg := wallpaperJ_nonneg
316 J_p6m_zero := wallpaperJ_p6m_eq_zero
317 J_p1_pos := wallpaperJ_p1_pos
318 J_mono := wallpaperJ_mono_in_orbits
319 preference_p6m_max := preference_p6m_max
320
321/-! ## §6. One-statement summary -/
322
323/-- **SYMMETRY GROUP PREFERENCE ONE-STATEMENT.** Three structural
324facts assembled into one theorem:
325
326(1) `p6m` (orbit count 12) sits at J-cost zero.
327(2) `p1` (orbit count 1) sits at J-cost strictly positive.
328(3) For any pair, the group with more orbits has lower J-cost.
329
330This forces the universal preference ordering:
331maximum-symmetry groups are universally preferred to lower-symmetry
332groups under the J-cost-derived preference functional. -/
333theorem symmetry_group_preference_one_statement :
334 wallpaperJ .p6m = 0 ∧
335 0 < wallpaperJ .p1 ∧
336 ∀ {g h : WallpaperGroup},
337 orbitCount g ≤ orbitCount h → wallpaperJ h ≤ wallpaperJ g :=
338 ⟨wallpaperJ_p6m_eq_zero, wallpaperJ_p1_pos,
339 @wallpaperJ_mono_in_orbits⟩
340
341end
342
343end SymmetryGroupPreference
344end Aesthetics
345end IndisputableMonolith
346