wallpaperJ_p1_pos
plain-language theorem explainer
The J-cost of the p1 wallpaper group is strictly positive. Researchers on visual symmetry preferences cite this to establish that the lowest-symmetry pattern carries positive recognition cost under the J-functional. The proof applies the general positivity lemma for non-unit ratios and confirms the ratio equals 1/12 by direct normalization.
Claim. $0 < J(1/12)$, where $J(r) = (r-1)^2/(2r)$ is the J-cost applied to the symmetry ratio $r =$ orbitCount(p1)/12.
background
The module enumerates the seventeen wallpaper groups by canonical orbit multiplicities under the full symmetry action. orbitCount assigns 1 to p1 and 12 to p6m, with maxOrbitCount defined as 12. The symmetry ratio is orbitCount(g)/12 and wallpaperJ(g) is Cost.Jcost of this ratio, replacing the v4 placeholder with the genuine cost from the multiplicative recognizer. The local setting is the derivation of symmetry-group preference from the J-functional in the aesthetics track. Upstream, the lemma wallpaperJ_pos_of_ne_one states: 'For any non-p6m group whose ratio is not 1, J-cost is strictly positive. The technical content is Jcost x = (x-1)²/(2x) > 0 when x ≠ 1.'
proof idea
The proof applies the lemma wallpaperJ_pos_of_ne_one to the p1 group. It unfolds symmetryRatio, orbitCount, and maxOrbitCount, then uses norm_num to verify that the ratio equals 1/12 and is therefore not 1.
why it matters
This supplies the strict positivity for p1 that enters the parent symmetry_group_preference_one_statement. That theorem assembles zero cost at p6m, positive cost at p1, and monotonicity in orbit count to force the universal preference ordering toward maximal symmetry. It supplies the concrete structural content for the cross-cultural preference claim in the aesthetics module and links to J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.