wallpaperJ_nonneg
plain-language theorem explainer
The J-cost of the symmetry ratio is non-negative for every one of the seventeen wallpaper groups. Researchers deriving symmetry preferences in aesthetics or crystallography would cite this to bound the preference functional from below. The proof is a one-line wrapper applying the general J-cost non-negativity lemma to the positivity of the symmetry ratio.
Claim. For every wallpaper group $g$, $0 ≤ J(g)$, where $J(g)$ is the J-cost of the ratio of the canonical orbit count of $g$ to the maximum orbit count.
background
The SymmetryGroupPreference module enumerates the seventeen crystallographic wallpaper groups by their canonical orbit multiplicities under the full symmetry action, with p6m attaining the maximum of 12. The symmetry ratio of a group $g$ is the orbit count of $g$ divided by 12; this ratio is positive. The wallpaper J-cost is defined as the J-cost function applied to this ratio. The module replaces an earlier placeholder definition with the genuine Cost.Jcost on the orbit-multiplicity ratio, which is reciprocal-symmetric and lives on the positive reals.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_nonneg (J-cost non-negative for positive arguments, via the identity Jcost(x) = (x-1)^2/(2x)) to the theorem symmetryRatio_pos g.
why it matters
This supplies the non-negativity fact required by downstream results including preference_p6m_max (which shows p6m maximizes the J-cost-derived preference) and the certificate symmetryGroupPreferenceCert. It confirms that J-cost reaches its floor of zero at the highest-symmetry group, supporting the framework emphasis on J-uniqueness and the cost minimum at the self-similar fixed point. The result closes a structural step in the aesthetics track by ensuring the cost ordering is well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.