W_endo_at_1
plain-language theorem explainer
The endogenous wallpaper count for a one-dimensional cube equals 2. Researchers proving dimension selection in Recognition Science cite this base case when showing that only D equals 3 yields the wallpaper-group count of 17. The proof evaluates the arithmetic definition of the sum directly via native decision.
Claim. $W_endo(1) = 2$, where $W_endo(d)$ is the endogenous wallpaper count given by the sum of passive field edges and cube faces in $d$ dimensions.
background
In the W_endo forcing module the endogenous wallpaper count is defined by $W_endo(d) :=$ passive_field_edges $d +$ cube_faces $d$, which expands to the closed form $d · 2^{d-1} + 2d - 1$. The module shows this quantity equals 17 precisely when $d = 3$, implementing the paper's Tr7 argument for spatial-dimension selection. The upstream definition in BaselineDerivation supplies the identical expression and notes that the value 17 at $d = 3$ matches the number of wallpaper groups.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the defining arithmetic sum at input 1.
why it matters
This base case is invoked inside the key theorem W_endo_eq_17_iff, which asserts $W_endo(d) = 17$ if and only if $d = 3$. That result supplies the paper's Tr7 step for dimension selection via the cube sum and aligns with the eight-tick octave (T7) together with the forcing of three spatial dimensions (T8) in the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.