W_endo
plain-language theorem explainer
W_endo(d) defines the endogenous wallpaper count for a d-dimensional hypercube as the sum of passive field edges and cube faces. Researchers deriving particle mass baselines or proving dimension uniqueness from the Recognition framework would reference this quantity when normalizing the wallpaper group count at D = 3. The definition is a direct one-line sum of two previously defined combinatorial functions.
Claim. $W_endo(d) := E_pass(d) + F(d)$, where $F(d) = 2d$ is the number of faces of the $d$-cube and $E_pass(d)$ counts the passive field edges obtained by subtracting the active edges per tick from the total edge count.
background
The module derives baseline rung integers from the combinatorics of the 3-cube Q3, upgrading prior boundary assumptions to derived status. Every integer traces to the single input D = 3. Cube_faces(d) equals 2d, the standard count of faces in a d-hypercube. Passive_field_edges(d) equals total edges minus active edges per tick; at D = 3 this yields the key number 11.
proof idea
The definition is a direct algebraic sum of the two upstream combinatorial functions passive_field_edges and cube_faces. No lemmas or tactics are invoked beyond the unfolding of the summands.
why it matters
This definition supplies the endogenous wallpaper count used in generation_ordering_general to establish 0 < E_pass < W and in dimension_unique_from_W_endo to prove D = 3 is the unique dimension yielding the value 17. It realizes item B-14 in the module table and feeds the WEndoForcing results that connect cube combinatorics to the eight-tick octave and spatial dimension selection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.