W_endo_gt_17_of_ge_4
plain-language theorem explainer
The theorem shows that for any natural number dimension d at least 4, the endogenous wallpaper count W_endo(d) exceeds 17. Physicists deriving spatial dimension uniqueness in Recognition Science cite this as supporting evidence for the Tr7 claim. The proof computes the value at d equals 4 as 39 and establishes monotonic increase by bounding the expression d times 2 to the d minus 1.
Claim. For every natural number $d$ with $dgeq 4$, the endogenous wallpaper count $W_{endo}(d)$ satisfies $W_{endo}(d)>17$.
background
In the W_endo Forcing module the endogenous wallpaper count is defined as $W_{endo}(d):=$ passive_field_edges(d) + cube_faces(d). Passive_field_edges(d) equals $dcdot 2^{d-1}-1$, the total hypercube edges minus one active edge per tick, while cube_faces(d) equals $2d$. The module proves that this sum equals 17 precisely when $d$ equals 3, with the present theorem handling the case $dgeq 4$ by direct comparison to the value at 4. Upstream definitions from AlphaDerivation supply cube_edges(d) as $dcdot 2^{d-1}$ and passive_field_edges as that quantity minus the constant active_edges_per_tick of 1.
proof idea
The proof first invokes W_endo_at_4 to obtain $W_{endo}(4)=39$. It then shows $W_{endo}(4)leq W_{endo}(d)$ by unfolding the definition into $dcdot 2^{d-1}+2d-1$ and applying inequalities: $2^3leq 2^{d-1}$ and $4cdot 2^3leq dcdot 2^{d-1}$, followed by the omega tactic to conclude the strict inequality $17<W_{endo}(d)$.
why it matters
This result feeds directly into the key theorem W_endo_eq_17_iff, which states $W_{endo}(d)=17$ if and only if $d=3$ and is identified as the paper's Tr7 dimension selection via the cube sum. Within the Recognition Science framework it supports the forcing chain step that selects D equals 3 as the unique spatial dimension satisfying the wallpaper count condition of 17. No open questions are addressed here; the result closes the case for $dgeq 4$ in the arithmetic argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.