module module high

`IndisputableMonolith.Aesthetics.SymmetryGroupPreference`

The module enumerates the seventeen wallpaper groups in IUC notation and supplies supporting functions for orbit counts and symmetry ratios. Researchers in pattern aesthetics or crystallographic symmetry would cite the standardized list when quantifying preference via J-cost. The module is purely definitional and imports only the time quantum from Constants together with cost primitives.

claimThe set of seventeen wallpaper groups in IUC notation, ordered as in Schattschneider 1978, together with the functions orbitCount : WallpaperGroup → ℕ and symmetryRatio : WallpaperGroup → ℝ that measure orbit structure and symmetry density.

background

The module sits in the Aesthetics domain and imports the RS time quantum τ₀ = 1 tick from Constants and the cost machinery from Cost. WallpaperGroup is defined as an inductive enumeration of the seventeen plane symmetry groups; orbitCount returns the number of distinct orbits under the group action on the plane, while symmetryRatio normalizes this count to a value in (0,1]. These definitions prepare symmetry data for later J-cost comparisons.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the canonical list of wallpaper groups required for any downstream symmetry-preference metric. It directly supports the definitions of symmetryRatio and wallpaperJ that appear among its siblings, providing the enumeration step needed before J-cost or phi-ladder comparisons can be applied to aesthetic patterns.

scope and limits

Does not enumerate three-dimensional space groups.
Does not prove any algebraic relations among the groups.
Does not compute explicit J-cost values for patterns.
Does not address non-crystallographic or aperiodic symmetries.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (25)

inductive WallpaperGroup L71
def orbitCount L81
def maxOrbitCount L101
theorem orbitCount_p6m L103
theorem orbitCount_pos L107
theorem orbitCount_le_max L110
def symmetryRatio L119
theorem symmetryRatio_pos L122
theorem symmetryRatio_p6m L131
theorem symmetryRatio_le_one L137
def wallpaperJ L149
theorem wallpaperJ_nonneg L152
theorem wallpaperJ_p6m_eq_zero L157
theorem wallpaperJ_pos_of_ne_one L165
theorem wallpaperJ_p1_pos L178
theorem wallpaperJ_p6m_le L185
theorem Jcost_anti_mono_on_unit_interval L197
theorem wallpaperJ_mono_in_orbits L240
def preference L260
theorem preference_p6m_eq_zero L262
theorem preference_p6m_max L269
theorem preference_anti_mono_in_orbits L278
structure SymmetryGroupPreferenceCert L301
def symmetryGroupPreferenceCert L311
theorem symmetry_group_preference_one_statement L333