symmetryRatio_le_one
plain-language theorem explainer
SymmetryRatio_le_one establishes that the orbit-count ratio for any of the seventeen wallpaper groups is at most one, with equality only for p6m. Aesthetic theorists and crystallographers cite it when ordering groups by J-cost preference derived from the multiplicative recognizer. The proof reduces the claim to the integer orbit bound via unfolding, casts to reals, and applies the division inequality lemma.
Claim. For every crystallographic wallpaper group $g$, the ratio of its canonical orbit multiplicity to the maximum multiplicity 12 satisfies $orbitCount(g)/12 ≤ 1$.
background
The module enumerates the seventeen wallpaper groups in IUC notation and records each group's canonical orbit count under the full symmetry action on the unit cell. The symmetry ratio is the real division of this count by the fixed maximum of twelve (attained by p6m). This normalized ratio is the argument to the genuine Cost.Jcost, replacing the earlier placeholder that had used raw orbit count directly.
proof idea
Unfolds the definition of symmetryRatio to obtain the division. Invokes orbitCount_le_max to produce the numerator inequality after casting to reals. Confirms the denominator is positive by norm_num on the constant twelve. Rewrites the goal with the library lemma div_le_one and closes with the numerator bound.
why it matters
The bound is required by symmetryGroupPreferenceCert, which packages the properties certifying that p6m is the J-cost minimum. It also supports wallpaperJ_mono_in_orbits, which establishes anti-monotonicity of the cost on the orbit lattice. In the Recognition framework the result connects crystallographic orbit multiplicities to the J-cost functional on the unit interval, ensuring the aesthetic preference ordering is well-defined and reciprocal-symmetric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.