W_endogenous
plain-language theorem explainer
Defines the endogenous W-count as the sum of passive field edges and hypercube faces in dimension d. Recognition Science uses this as a cube-combinatorial candidate for the classical wallpaper constant 17. At d=3 the sum is 11+6=17. The definition is a one-line arithmetic combination of two existing cube counts.
Claim. For each natural number $d$, the endogenous $W$-count is $W_{\mathrm{end}}(d) := E_{\mathrm{passive}}(d) + F(d)$, where $E_{\mathrm{passive}}(d)$ is the number of passive (field) edges of the $d$-cube and $F(d)=2d$ is the number of faces. Equivalently, $W_{\mathrm{end}}(d)=d\cdot 2^{d-1}-1+2d$.
background
The Wallpaper Endogenous Bridge module builds an explicit counting path from RS cube combinatorics to the crystallographic constant $W=17$. Classically, $W=17$ is imported as Fedorov's 1891 classification of plane wallpaper groups; this file does not re-prove that classification. Instead it formalizes an endogenous candidate $W_{\mathrm{end}}(D):=E_{\mathrm{passive}}(D)+F(D)$.
Passive field edges are total cube edges minus the single active edge per tick (the edges that "dress" the interaction). Cube faces are the standard $F=2D$ faces of the $D$-hypercube. For $D=3$ the module records $E_{\mathrm{passive}}=11$ and $F=6$, so the candidate equals 17 and matches the imported wallpaper constant at the counting layer.
This sits in the verification layer of the RS forcing story: spatial dimension $D=3$ is already forced (T8), and the eight-tick octave and cube geometry supply the edge and face counts used here.
proof idea
Pure definitional abbreviation: the body is the sum of the two upstream natural-number defs passive_field_edges d and cube_faces d. No tactics or lemmas are required. The companion theorem W_endogenous_formula unfolds the sum to the closed form $d\cdot 2^{d-1}-1+2d$ by rfl once the edge and face formulas are expanded.
why it matters
This def is the counting-layer anchor of the Pass-2 wallpaper bridge. Downstream theorems pin its value and uniqueness: W_endogenous_at_D3 shows equality to 17 at $D=3$; W_endogenous_matches_wallpaper_groups equates it to the imported wallpaper_groups; decomposition_at_D3 packages the component identity $11+6=17$; unique17ScanUpTo64 checks that among dimensions $0..64$ only $D=3$ yields 17; and wallpaper_slot_iff_endogenous_formula closes the generator-level slot as exactly $E_{\mathrm{passive}}+F$.
In the broader RS chain this is a bridge step toward full endogeneity of $W$: the classical 17 is no longer a free import at the counting layer once $D=3$ is fixed. It does not yet replace the geometric classification of wallpaper groups, but it makes the $11+6=17$ identity machine-checked and dimensionally selective.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.