W_decomposition
plain-language theorem explainer
The decomposition states that the endogenous wallpaper count at three dimensions equals the sum of passive field edges and cube faces. Researchers deriving dimension selection from wallpaper counts cite this as the base case of the Tr7 forcing argument. The proof is a one-line reflexivity that follows directly from the definition of the count as that sum.
Claim. $W(3) = E(3) + F(3)$, where $W$ is the endogenous wallpaper count, $E$ counts passive field edges, and $F$ counts the faces of the three-cube.
background
The W_endo forcing module defines the endogenous wallpaper count by $W(d) := E(d) + F(d)$, where $E$ subtracts active edges per tick from total cube edges and $F$ equals $2d$. The module shows this sum equals 17 precisely when $d=3$, which supplies the paper's Tr7 argument via direct arithmetic on the formula $d·2^{d-1} + 2d - 1$ for successive integer dimensions.
proof idea
The proof is a one-line term that applies reflexivity to the definition of W_endo.
why it matters
This equality supplies the base case for the Tr7 claim that the wallpaper count equals 17 if and only if the spatial dimension is three. It anchors the forcing chain step that selects D=3 and feeds the uniqueness result for three dimensions from the wallpaper condition. The arithmetic verification closes the eight-tick octave selection in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.