W_endo_at_3
plain-language theorem explainer
The endogenous wallpaper count at spatial dimension three equals seventeen. Researchers studying dimension selection in Recognition Science cite this to anchor the eight-tick octave at D equals three. The proof is a direct native decision on the closed-form arithmetic expression for the count.
Claim. $W_endo(3) = 17$, where the endogenous wallpaper count is given by $W_endo(d) = d · 2^{d-1} + 2d - 1$.
background
The W_endo forcing module defines the endogenous wallpaper count as the sum of passive field edges and cube faces for a d-dimensional cube. This produces the explicit formula d times 2 to the power of d minus one plus two d minus one. The local theoretical setting is the forcing-chain argument that this count equals the wallpaper-groups constant of seventeen if and only if the dimension is three, realizing the Tr7 step. Upstream results in the masses baseline derivation establish the identical definition as the sum of passive edges and faces, with the same evaluation at dimension three.
proof idea
The proof is a one-line wrapper that invokes native decision procedures to evaluate the arithmetic expression for the wallpaper count at dimension three.
why it matters
This supplies the base value for the uniqueness theorem that dimension three is the sole positive integer yielding the wallpaper count of seventeen and for the biconditional theorem that the count equals seventeen precisely when the dimension is three. It realizes the Tr7 step in the forcing chain, confirming that the eight-tick octave forces exactly three spatial dimensions. The downstream uniqueness result builds directly on this evaluation to complete the existence and uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.