symmetryRatio_p6m
plain-language theorem explainer
The theorem establishes that the symmetry ratio for the p6m wallpaper group equals one. Researchers deriving J-cost minima for maximal symmetry patterns under the Recognition Science framework cite this when ordering wallpaper groups by preference. The short tactic proof unfolds the ratio definition, rewrites via the orbit count equality for p6m, unfolds the maximum orbit definition, and reduces numerically.
Claim. Let $r(g)$ denote the symmetry ratio of wallpaper group $g$, defined as the real number obtained by dividing the orbit count of $g$ by the maximum orbit count. Then $r(p6m) = 1$.
background
The Aesthetics module enumerates the seventeen wallpaper groups by canonical generator-orbit multiplicity. orbitCount assigns to each group the cardinality of orbits in its fundamental domain under the full symmetry action, while maxOrbitCount is the constant 12 corresponding to the p6m group. The symmetry ratio is the real division (orbitCount g) / (maxOrbitCount), which lies in (0,1] and enters the definition wallpaperJ g := Cost.Jcost of that ratio.
proof idea
The term-mode proof unfolds symmetryRatio, rewrites the p6m orbit count using the lemma orbitCount_p6m, unfolds maxOrbitCount, and closes with norm_num.
why it matters
This supplies the equality required by the downstream theorem wallpaperJ_p6m_eq_zero, which places p6m at the J-cost floor of zero. It supports the module's headline claim that maximal symmetry is preferred under the J-cost functional, consistent with the Recognition Science emphasis on J-uniqueness and the self-similar fixed point. The result completes the computation for the highest-symmetry case in the wallpaper enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.