W_endo_at_4
plain-language theorem explainer
Endogenous wallpaper count equals 39 at dimension 4. Researchers deriving dimension uniqueness via the Recognition Composition Law cite this value to bound the count strictly above 17 for all D greater than or equal to 4. The proof reduces to direct arithmetic evaluation of the defining sum via native decision.
Claim. The endogenous wallpaper count satisfies $W_endo(4)=39$, where $W_endo(d)$ is the sum of passive field edges and cube faces for a $d$-cube.
background
The endogenous wallpaper count is defined by $W_endo(d) := passive_field_edges d + cube_faces d$. This decomposition counts the passive field edges plus the faces of the $D$-cube and appears in both the local module and the upstream BaselineDerivation module. The module setting states that $W_endo(D)$ equals 17 if and only if $D=3$, supplying the Tr7 argument for dimension selection through explicit arithmetic checks for small $D$ and growth for $D$ greater than or equal to 4.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic expression for $W_endo$ at input 4. It relies only on the prior definition of $W_endo$ as the sum of passive_field_edges and cube_faces together with decidability of natural-number arithmetic; no additional lemmas are invoked.
why it matters
This supplies the base case for $W_endo_gt_17_of_ge_4$, which feeds the key equivalence $W_endo_eq_17_iff$ establishing $W_endo(D)=17$ if and only if $D=3$. That equivalence is the paper's Tr7 argument. It aligns with framework landmark T8 forcing $D=3$ spatial dimensions and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.