wallpaperJ
plain-language theorem explainer
Wallpaper groups receive a real-valued cost by applying the Recognition Science J-cost function to the ratio of each group's canonical orbit count to the maximum of 12. Researchers in aesthetic preference or crystallography would cite this definition when grounding symmetry orderings in the J-cost functional. It is realized as a direct one-line composition of Cost.Jcost with the symmetry ratio map.
Claim. For a wallpaper group the associated J-cost equals the Recognition Science cost function applied to the ratio of the group's canonical orbit count to the maximum orbit count of twelve, where the cost function satisfies $J(x) = (x + x^{-1})/2 - 1$.
background
The module replaces the v4 skeleton that set wallpaper J-cost to raw orbit count with the genuine Cost.Jcost applied to the symmetry ratio. WallpaperGroup is the inductive type enumerating the seventeen crystallographic plane symmetry groups in IUC notation. The symmetry ratio of a group is its orbit count divided by maxOrbitCount, which equals 12 for the p6m group. Cost is the abbrev for Quantity CostUnit drawn from the RSNative measurement core.
proof idea
The definition is a one-line wrapper that applies Cost.Jcost to the symmetry ratio of the input wallpaper group.
why it matters
This definition supplies the J-cost values used by the preference functional, the SymmetryGroupPreferenceCert structure, and the symmetry_group_preference_one_statement theorem. It enables the proofs that p6m achieves J-cost zero, p1 has positive J-cost, and J-cost decreases with orbit count. In the Recognition Science framework it instantiates J-uniqueness from the forcing chain on the unit interval for the aesthetic preference application.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.