dimension_unique_from_W_endo
plain-language theorem explainer
The theorem shows that three is the unique positive integer dimension where the endogenous wallpaper count equals seventeen. Recognition Science derivations of spatial dimensionality from symmetry counts would cite this to close the forcing argument for D = 3. The term proof exhibits the value at three and reduces uniqueness to an equivalence lemma on all other candidates.
Claim. There exists a unique natural number $d$ with $d$ at least 1 such that the endogenous wallpaper count $W_endo(d)$ equals 17.
background
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 upstream abbrev W from the Anchor module fixes the wallpaper groups count at 17. The module WEndoForcing states that this count equals 17 if and only if the dimension is 3, supplying the paper's Tr7 step.
proof idea
The term proof uses the constructor to witness dimension 3 via the fact W_endo_at_3 together with a norm_num check on the lower bound. For uniqueness it applies the equivalence W_endo_eq_17_iff to any other candidate d satisfying the hypothesis.
why it matters
This declaration supplies the uniqueness direction of the Tr7 argument in the W_endo Forcing module, confirming that the wallpaper count of 17 forces exactly three spatial dimensions. It directly supports the Recognition Science chain step T8 that derives D = 3 from the eight-tick octave. The result is fully closed with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.