W_endo_at_D3
plain-language theorem explainer
At D=3 the endogenous wallpaper count W_endo equals the crystallographic constant 17. Mass-ladder derivations cite this equality to anchor the generation ordering 0 < 11 < 17. The proof is a one-line native_decide that evaluates the definition W_endo(D) = passive_field_edges(D) + cube_faces(D) directly at D=3.
Claim. At spatial dimension $D=3$, the endogenous wallpaper count $W_endo(D)=E_pass(D)+F(D)$ equals the number of distinct 2D wallpaper groups, which is 17.
background
W_endo(D) is defined as passive_field_edges(D) + cube_faces(D), the endogenous wallpaper count arising from 3-cube combinatorics. The module derives all baseline rung integers from the single input D=3, upgrading prior boundary assumptions to derived status; B-14 records the generation ordering 0 < E_pass < W. wallpaper_groups is the standard crystallographic constant 17 established by Fedorov in 1891.
proof idea
One-line wrapper that applies native_decide to evaluate the combinatorial definition of W_endo at D=3 and match it against the constant 17.
why it matters
This declaration supplies the numerical anchor for generation ordering in the cube-geometry derivations (module B-14). It connects the Recognition forcing chain (T8: D=3) to the crystallographic constant, supporting the phi-ladder mass formulas and the completeness condition for the Z-map polynomial. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.