W_endogenous_at_D3
plain-language theorem explainer
At spatial dimension three, the endogenous wallpaper count built from cube combinatorics equals 17. Anyone bridging RS cube geometry to the classical crystallographic constant W cites this equality. The proof is a one-shot native decision of the closed arithmetic form at D = 3.
Claim. Let $W_{\mathrm{end}}(d) := E_{\mathrm{passive}}(d) + F(d)$ be the endogenous wallpaper candidate from $d$-cube combinatorics, equivalently $W_{\mathrm{end}}(d) = d\,2^{d-1}-1+2d$. With the forced spatial dimension $D=3$, one has $W_{\mathrm{end}}(D)=17$.
background
This module is Pass 2 of the wallpaper endogenous bridge. The framework still imports the classical fact that there are 17 wallpaper groups (Fedorov 1891); it does not re-prove crystallographic classification. Instead it defines an RS-native candidate
$W_{\mathrm{endogenous}}(d) := E_{\mathrm{passive}}(d) + F(d)$
from hypercube combinatorics, with closed form $d,2^{d-1}-1+2d$. The module goal is to make the counting identity $11+6=17$ at $D=3$ explicit and machine-checked, matching the imported constant.
Spatial dimension $D$ is fixed to 3 by the forcing chain (T8 / T9 linking). Upstream constants modules expose that same $D:=3$. Passive field edges and cube faces are the two combinatorial summands: at $d=3$ they evaluate to 11 and 6 respectively.
proof idea
Term-mode proof by native_decide. After unfolding $W_{\mathrm{endogenous}}$ and the definition $D=3$, both sides are concrete natural numbers, so the kernel decides $W_{\mathrm{endogenous}},3=17$ by evaluation. No intermediate lemmas are invoked.
why it matters
This is the arithmetic anchor of the wallpaper bridge: it shows the RS cube formula lands exactly on the classical count 17 when dimension is the forced $D=3$ from the forcing chain (T8). Downstream, W_from_cube_eq_17 is a one-line simpa wrapper that rewrites the cube-derived $W$ through this equality, so every later identification of cube $W$ with wallpaper groups routes through here.
The module frames the result as a bridge step toward full endogeneity of $W$, not a replacement for Fedorov classification. It closes the counting-layer gap $11+6=17$ inside the verification layer while leaving the geometric classification external.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.