W_endo_eq_wallpaper
plain-language theorem explainer
The theorem establishes that the endogenous wallpaper count at three dimensions equals the crystallographic constant of seventeen wallpaper groups. Researchers tracing the Recognition Science forcing chain from T7 would reference this arithmetic identity. The proof reduces to a single native_decide tactic that evaluates the closed arithmetic expression for W_endo(3).
Claim. $W_endo(3) = 17$, where $W_endo(d)$ is the sum of passive field edges and cube faces for a $d$-cube, and 17 is the number of distinct two-dimensional wallpaper groups.
background
The module defines the endogenous wallpaper count as $W_endo(d) :=$ passive_field_edges $d +$ cube_faces $d$. The module document gives the closed form $W_endo(D) = D · 2^(D-1) + 2D - 1$ and states that this equals 17 precisely when $D=3$, supplying the Tr7 step. Upstream results define wallpaper_groups as the constant 17, the Fedorov count of 2D wallpaper groups from 1891.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the arithmetic equality between W_endo(3) and the constant 17.
why it matters
This theorem supplies the arithmetic verification for the Tr7 claim that W_endo equals 17 if and only if D=3. It supports the uniqueness of three spatial dimensions by matching the observed wallpaper groups count. The declaration has no downstream uses in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.