Pith. sign in
module module moderate

IndisputableMonolith.Verification.WallpaperClassificationBridge

show as:
view Lean formalization →

Bridge module that classifies the 17 wallpaper groups by edge-type versus face-type generators on the cubic ledger. It records E_passive = 11 independent edge symmetries and the complementary face count, then equates their sum to the classical wallpaper total. Anyone tracing the combinatorial seed 4π·11 in the alpha construction cites this split. The content is definitional enumeration plus equality lemmas, not a deep existence proof.

claimThe 17 wallpaper groups $W$ of the plane decompose as edge-generated groups (1D symmetries: edge translations, edge-perpendicular reflections, glides) together with face-generated groups. There are $E_{\mathrm{passive}}=11$ independent edge-type generators and a complementary face-dominant count $F$, with $|W|=E_{\mathrm{passive}}+F=17$.

background

Recognition Science builds the fine-structure seed from cubic-ledger combinatorics. The upstream AlphaDerivation module assembles the seed $4\pi\cdot 11$ from that geometry; the factor 11 is identified with a count of independent edge-type (passive) generators rather than derived from first principles as the measured $\alpha^{-1}(0)$.

This module supplies the geometric side of that identification. Edge-type symmetries are the 1D operations along cube edges: translations parallel to edges, reflections across planes perpendicular to edges, and the associated glide reflections. Face-type symmetries complete the classical list. The ambient setting is the standard crystallographic classification of the 17 wallpaper groups, re-indexed by which generator class dominates.

Notation introduced here includes the edge-generated and face-generated families, a two-valued symmetry type, a dominant-type projection, and the numerical counts $E_p$ and $F$ with the equalities that pin them to 11 and to the residual face total.

proof idea

Definition module with supporting count lemmas. It introduces the edge- and face-generated families, the wallpaper-group type, and a dominant-type classifier, then proves the numerical identities edge-dominant count $= E_p$ and face-dominant count $= F$, together with the decomposition $|W|=17$. Arguments are by exhaustive case split on the classical 17 groups and direct comparison of generator support; no analytic estimates.

why it matters in Recognition Science

The module exists to underwrite the combinatorial factor 11 inside the alpha seed $4\pi\cdot 11$ assembled in Constants.AlphaDerivation. That upstream doc states the cube combinatorics explain the seed's construction (while the exact infrared $\alpha^{-1}(0)$ remains an open boundary condition). By equating the edge-passive generator count to 11 and closing $W=17$, the bridge makes the geometric origin of the seed auditable inside the verification layer. No downstream consumers are wired yet; the intended parent is the alpha-construction audit path rather than a forcing-chain step (T0–T8).

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)