symmetryRatio_pos
plain-language theorem explainer
The theorem states that the symmetry ratio of any wallpaper group is strictly positive. Researchers modeling visual symmetry preferences via J-cost would cite it to ensure the argument to Jcost lies in the open unit interval. The proof unfolds the ratio definition, casts the upstream orbitCount_pos result to reals, confirms the denominator is twelve, and closes with the positivity tactic.
Claim. For every wallpaper group $g$, $0 < orbitCount(g)/12$, where $orbitCount(g)$ is the canonical orbit multiplicity of $g$ under its full symmetry action.
background
The module enumerates the seventeen wallpaper groups as the inductive type WallpaperGroup. For each $g$, the function orbitCount assigns the standard crystallographic orbit cardinality (1 for p1, 12 for p6m). maxOrbitCount is the constant 12. symmetryRatio is defined as the real division orbitCount g / maxOrbitCount, which therefore lies in (0,1]. The upstream theorem orbitCount_pos asserts that every orbitCount value is a positive natural number. This positivity lemma is required before Cost.Jcost can be applied to the ratio, as done in the module's headline results on wallpaper J-cost.
proof idea
The proof unfolds symmetryRatio to obtain the division. It derives a real positivity statement for the numerator via exact_mod_cast applied to orbitCount_pos g. It unfolds maxOrbitCount and uses norm_num to obtain positivity of the denominator. The positivity tactic then finishes the goal.
why it matters
The result is invoked by wallpaperJ_nonneg, wallpaperJ_pos_of_ne_one, and wallpaperJ_mono_in_orbits. Those theorems establish that p6m sits at J-cost zero while every other group has strictly positive cost, with the ordering anti-monotonic in orbit count. The lemma therefore supports the module claim that p6m is the universally preferred wallpaper group under the J-cost preference functional derived from the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.