total_matches_W
plain-language theorem explainer
Edge-dominant plus face-dominant wallpaper counts equal the classical total W = 17 (namely 11 + 6). Anyone citing the cube-intrinsic split W = E_passive + F uses this equality. The proof is a one-line native decision on the concrete naturals already fixed by the surrounding definitions.
Claim. The number of edge-dominant wallpaper groups plus the number of face-dominant wallpaper groups equals the total number of distinct planar wallpaper groups: $11 + 6 = 17$.
background
Fedorov (1891) classified exactly 17 wallpaper groups: planar crystallographic symmetry groups generated by translations, rotations, reflections, and glides compatible with a 2D lattice. In Recognition Science this constant is written $W = 17$ and enters the alpha-denominator bookkeeping as faces times wallpaper groups.
This module strengthens the endogenous bridge from the 3-cube. Spatial dimension is fixed at $D = 3$ (forced by the linking/T9 step). The cube has $F = 6$ square faces; passive edge count is $E_{\mathrm{passive}}(D) = D \cdot 2^{D-1} - 1$, which equals 11 at $D = 3$. The structural claim is $W = E_{\mathrm{passive}} + F = 11 + 6$, matching the classical total only in three dimensions.
Sibling definitions partition the 17 groups by dominant symmetry type: edge-type (1D translations, reflections, glides) versus face-type (2D rotations and full face symmetries). The counts of those two classes are the left-hand summands here; wallpaper_groups is the constant 17.
proof idea
Both summands and the right-hand side are concrete natural-number definitions (11, 6, and 17). The proof is a single native_decide step that evaluates the closed arithmetic equality $11 + 6 = 17$ in the kernel. No algebraic lemmas are invoked; the content lives entirely in the surrounding count definitions and the crystallographic assignment of dominant type.
why it matters
Closes the numerical half of the structural decomposition advertised in the module: $W = $ (edge-generated groups) $+$ (face-generated groups) $= E_{\mathrm{passive}} + F = 11 + 6 = 17$, available only at $D = 3$. That identity is the cube-intrinsic reason the classical wallpaper count appears in the Recognition forcing chain (spatial dimension T8/T9, eight-tick octave, alpha curvature fraction).
It strengthens WallpaperEndogenousBridge, which already showed $W_{\mathrm{endogenous}}(D) = 17$ iff $D = 3$, by exhibiting the internal 11 + 6 split rather than only the total. The module notes the remaining open step: dominantType is still a definition from the standard classification, not yet derived from pure cube combinatorics (edge-type versus face-type generators). No downstream theorems currently depend on this lemma; it is a verification checkpoint for the bridge narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.