W_endo
plain-language theorem explainer
The endogenous wallpaper count is defined as the sum of passive field edges and cube faces for a d-dimensional cube. Researchers deriving why only three spatial dimensions arise in Recognition Science cite this as the quantity that must equal 17 to match the wallpaper groups. The definition is a direct arithmetic combination of two counting functions already fixed in the constants layer.
Claim. $W(d) := E(d) + F(d)$, where $F(d) = 2d$ is the number of faces of the $d$-cube and $E(d)$ counts the passive field edges obtained by subtracting the active edges per tick from the total cube edges.
background
The WEndoForcing module introduces the endogenous wallpaper count to encode the total wallpaper elements generated by passive fields plus cube faces. Its local setting is the claim that this count equals 17 if and only if the dimension is 3, presented as the paper's Tr7 step. Upstream, cube_faces is defined as twice the dimension, giving the face count of the hypercube, while passive_field_edges subtracts the active edges per tick from the total cube edges to isolate the dressing edges.
proof idea
This is a direct definition that adds the outputs of passive_field_edges and cube_faces. No lemmas or tactics are invoked beyond the two upstream counting definitions.
why it matters
The definition supplies the central quantity for dimension_unique_from_W_endo, which establishes that D=3 is the unique positive integer yielding the value 17. It implements the Tr7 forcing step that selects three spatial dimensions by matching the wallpaper group count. Downstream results such as W_decomposition and W_endo_at_D3 use it to verify the arithmetic at D=3 and to feed the generation ordering theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.