W_endo_at_2
plain-language theorem explainer
The endogenous wallpaper count at dimension two equals seven. Researchers proving dimension selection in Recognition Science cite this fact when showing that only three dimensions reach the critical wallpaper threshold of seventeen. The result follows from direct computational evaluation of the definition W_endo(d) := passive_field_edges(d) + cube_faces(d) at d = 2.
Claim. The endogenous wallpaper count satisfies $W_endo(2) = 7$, where $W_endo(d) := E_passive(d) + F(d)$ denotes the sum of passive field edges and cube faces for a $d$-cube.
background
The module establishes that the endogenous wallpaper count equals seventeen if and only if the spatial dimension equals three. This count is defined as the sum of passive field edges and cube faces for a $d$-cube. Upstream results supply the identical definition and note that the value at three dimensions is eleven plus six, equaling seventeen.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the definition of the endogenous wallpaper count at input two.
why it matters
This case supplies the dimension-two entry in the proof of the key theorem that the endogenous wallpaper count equals seventeen if and only if the dimension equals three. That theorem is the paper's Tr7 argument for dimension selection via the cube sum. It supports the forcing chain landmark that selects three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.