W_endo_eq_17_iff
plain-language theorem explainer
The theorem states that the endogenous wallpaper count W_endo equals 17 exactly when the dimension d is 3, for natural numbers d at least 1. Physicists deriving dimension selection in Recognition Science cite this as the arithmetic core of Tr7. The proof proceeds by case analysis on d, applying explicit evaluations at d=1,2,3,4 and a growth bound for d>=5.
Claim. $W(d) = 17$ if and only if $d=3$, for natural numbers $d$ with $1$ ≤ $d$, where $W(d)$ denotes the endogenous wallpaper count defined as the sum of passive field edges and cube faces in dimension $d$.
background
The module WEndoForcing defines the endogenous wallpaper count as W_endo(d) := passive_field_edges d + cube_faces d. The explicit closed form is W_endo(d) = d · 2^(d-1) + 2d - 1. The local setting is the paper's Tr7 argument that this count equals 17 precisely at d=3, providing the arithmetic engine for dimension selection. Upstream results include the same W_endo definition appearing in Masses.BaselineDerivation and the explicit evaluations W_endo_at_1, W_endo_at_2, W_endo_at_3, W_endo_at_4 together with the inequality W_endo_gt_17_of_ge_4.
proof idea
The tactic proof opens with constructor to split the biconditional. The forward direction performs a match on d (with the hypothesis 1 ≤ d) and dispatches each case by simp using the named evaluations at 1, 2, 4 or rfl at 3; for d+5 it invokes the growth lemma W_endo_gt_17_of_ge_4 followed by omega. The reverse direction substitutes d=3 and applies W_endo_at_3.
why it matters
This theorem supplies the if-and-only-if arithmetic uniqueness of dimension 3 for the wallpaper count equaling 17 and is used directly by dimension_unique_from_W_endo to obtain the unique-existence statement. It realizes the paper's Tr7 step inside the forcing chain that selects D=3 spatial dimensions. In the Recognition Science framework it closes the cube-sum argument that forces the eight-tick octave and the observed spatial dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.