SymmetryGroupPreferenceCert
plain-language theorem explainer
SymmetryGroupPreferenceCert bundles eight properties that certify J-cost minimization selects the p6m wallpaper group as maximally preferred among the seventeen groups. Researchers applying Recognition Science to aesthetic judgments would cite the certificate to ground cross-cultural symmetry predictions. The structure aggregates results from orbit-count definitions and Cost.Jcost lemmas without new derivations inside the declaration.
Claim. Let $o(g)$ be the orbit count of wallpaper group $g$, $r(g)=o(g)/12$, and $J$ the J-cost function. A symmetry-group preference certificate asserts: $o(g)>0$ for all $g$; $o(p6m)=12$; $r(g)≤1$ for all $g$; $J(r(g))≥0$ for all $g$; $J(1)=0$; $J(1/12)>0$; $o(g)≤o(h)$ implies $J(r(h))≤J(r(g))$; and $-J(r(g))≤-J(1)$ for all $g$.
background
The module enumerates the seventeen wallpaper groups by canonical generator-orbit multiplicity. orbitCount assigns each group its standard crystallographic orbit cardinality (p1 has one orbit, p6m has twelve). maxOrbitCount is the constant 12. symmetryRatio normalizes each count to the unit interval by division by maxOrbitCount. wallpaperJ applies Cost.Jcost to the resulting ratio, replacing the earlier placeholder that used raw integer orbit counts. preference is defined as the negation of wallpaperJ so that minimal cost yields maximal preference. The local setting is the replacement of the v4 skeleton by a genuine derivation from the Recognition Science J-cost functional applied to symmetry ratios.
proof idea
This is a structure definition that packages eight properties. Each field is supplied directly by a sibling result: orbit_pos from orbitCount_pos, orbit_p6m_eq_max from orbitCount_p6m, ratio_le_one from symmetryRatio_le_one, J_nonneg from wallpaperJ_nonneg, J_p6m_zero from wallpaperJ_p6m_eq_zero, J_p1_pos from wallpaperJ_p1_pos, J_mono from wallpaperJ_mono_in_orbits, and preference_p6m_max from the theorem of the same name.
why it matters
The certificate supplies the structural backbone for the claim that J-cost selects p6m as the universally preferred wallpaper group. It is instantiated by the downstream symmetryGroupPreferenceCert definition. Within the Recognition framework it applies the J-uniqueness property (T5) and the reciprocity of J to a concrete discrete symmetry setting, supporting the cross-cultural preference prediction that replaces the v4 placeholder. It touches the open question of quantitative fit between the derived ordering and empirical aesthetic data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.