W_from_cube
plain-language theorem explainer
Names the endogenous wallpaper count at spatial dimension three by specializing the cube-combinatorial formula to D=3. Anyone working the Pass-2 bridge from hypercube edge and face counts to the classical crystallographic constant 17 cites this abbreviation. It is a one-line definitional specialization, not a derived equality.
Claim. Define the cube-derived wallpaper candidate at the forced spatial dimension by $W_{\mathrm{cube}} := W_{\mathrm{endog}}(3)$, where $W_{\mathrm{endog}}(d) = E_{\mathrm{passive}}(d) + F(d)$ is the sum of passive-field edges and cube faces on the $d$-cube (equivalently $d\cdot 2^{d-1}-1+2d$).
background
The module builds an explicit counting-layer bridge from RS cube combinatorics to the crystallographic constant $W=17$. Classically, $W=17$ is imported as Fedorov's 1891 classification of wallpaper groups; the file does not re-prove that classification. Instead it defines an endogenous candidate
$W_{\mathrm{endog}}(d) := E_{\mathrm{passive}}(d) + F(d)$,
with closed form $d\cdot 2^{d-1}-1+2d$. At the forced spatial dimension $D=3$ (T8/T9), this splits as $E_{\mathrm{passive}}=11$ and $F=6$, so $11+6=17$.
Upstream, $D$ is the constant natural number 3 in AlphaDerivation, GapDerivation, and FermionDOFGapBridge: the spatial dimension forced by the forcing chain. The sibling $W_{\mathrm{endog}}$ is the $d$-dependent generator; the present definition freezes it at that $D$.
proof idea
Pure definitional abbreviation: bind the natural-number constant to the endogenous formula evaluated at the forced dimension constant $D$. No tactics, no lemmas, no computation at this site. Equalities such as equality to 17 or to the imported wallpaper-group count are proved downstream by rewriting through this name.
why it matters
Gives a stable named handle for the cube-derived $W$ so later bridge and mass-path theorems can replace the imported classical constant by an RS-native expression. Downstream, $W_{\mathrm{from,cube}}=17$ and $W_{\mathrm{from,cube}}=\mathrm{wallpaper_groups}$ are one-line rewrites; the generator-level biconditional identifies the wallpaper slot with $E_{\mathrm{passive}}(D)+F(D)$; and the package theorem packages those facts as endogenous closure of the counting-layer slot.
On the mass path, base-shift and ledger-fraction rewrites, and the endogenous-replacement completeness theorem, substitute this constant for the classical $W$, showing mass-topology formulae are invariant under the endogenous swap. In the broader framework this is a Pass-2 step toward full endogeneity of $W$, sitting on the $D=3$ landmark (T8) without yet discharging the classical classification itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.