symmetryGroupPreferenceCert
plain-language theorem explainer
The definition constructs the master certificate structure by instantiating its eight fields with lemmas on orbit counts and J-cost. Researchers deriving cross-cultural aesthetic preferences from Recognition Science would cite it to certify that maximum-symmetry wallpaper groups sit at minimal J-cost. The construction is a direct record builder that references the positivity, maximality, monotonicity, and zero-cost results already proved in the module.
Claim. The certificate is the structure whose fields assert: every wallpaper group $g$ has positive orbit count, the group $p6m$ achieves the maximum orbit count of 12, every symmetry ratio lies in $(0,1]$, every group has non-negative J-cost, $p6m$ has J-cost exactly zero, $p1$ has strictly positive J-cost, J-cost decreases monotonically as orbit count increases, and $p6m$ is the group of maximal preference.
background
The module defines wallpaper J-cost for the seventeen wallpaper groups by their canonical orbit multiplicities under the full symmetry action. Specifically, $wallpaperJ(g) := Cost.Jcost(orbitCount(g)/maxOrbitCount)$ where $maxOrbitCount = 12$ for $p6m$, so that the cost is the genuine J-function applied to the normalized ratio; this inherits reciprocity and non-negativity from the Recognition Composition Law. Preference is then the negation of this cost. Upstream lemmas establish the orbit facts by direct unfolding and case analysis on the enumerated groups, while the J-cost properties follow from the imported Cost.Jcost_nonneg and the monotonicity of J on $(0,1]$.
proof idea
The definition is a record constructor that assigns each of the eight fields of SymmetryGroupPreferenceCert directly to the corresponding sibling theorem: orbit positivity from orbitCount_pos, $p6m$ maximality from orbitCount_p6m, ratio bound from symmetryRatio_le_one, non-negativity from wallpaperJ_nonneg, zero at $p6m$ from wallpaperJ_p6m_eq_zero, positivity at $p1$ from wallpaperJ_p1_pos, monotonicity from wallpaperJ_mono_in_orbits, and maximal preference from preference_p6m_max.
why it matters
The certificate assembles the structural facts that underwrite the one-statement summary: $p6m$ at J-cost zero, $p1$ at positive cost, and monotonic preference ordering by orbit count. It thereby supplies the concrete content for the J-cost-derived aesthetic prediction in the Aesthetics track. The construction closes the derivation for wallpaper-group preference without introducing new hypotheses; it sits downstream of the Cost module and the orbit enumeration but has no further dependents listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.