symmetryRatio
plain-language theorem explainer
The symmetry ratio normalizes each wallpaper group's canonical orbit count against the fixed maximum of twelve attained by p6m. Aesthetic theorists and crystallographers modeling cross-cultural symmetry preference cite this ratio to supply the argument to the J-cost functional. The definition performs a direct real division of the integer orbit count by the constant twelve.
Claim. For a wallpaper group $g$, define the symmetry ratio $r(g) = k(g)/12$, where $k(g)$ is the canonical orbit multiplicity of the fundamental domain under the full symmetry action (with $k(p6m)=12$).
background
The module enumerates the seventeen wallpaper groups via the inductive type WallpaperGroup (p1 through p6m, matching Schattschneider 1978). The sibling definition orbitCount assigns each group its standard crystallographic multiplicity: 1 for p1, 2 for several groups, and 12 for p6m. The constant maxOrbitCount is fixed at 12, the value for the highest-symmetry group p6m.
proof idea
One-line definition that casts orbitCount g to ℝ and divides by the constant maxOrbitCount = 12.
why it matters
This supplies the normalized ratio that enters wallpaperJ and the SymmetryGroupPreferenceCert structure. It supports downstream results including symmetryRatio_le_one, symmetryRatio_pos, wallpaperJ_mono_in_orbits, and the claim that p6m realizes the J-cost minimum. The construction replaces the v4 placeholder orbit-count cost with the genuine Cost.Jcost of the ratio, operationalizing J-uniqueness for aesthetic ordering among the seventeen plane groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.