W_endo_at_5
plain-language theorem explainer
The theorem states that the endogenous wallpaper count equals 89 at dimension 5. Researchers tracing the Recognition Science forcing chain cite it to confirm W_endo exceeds 17 once D passes 3. The proof is a direct native_decide evaluation of the closed-form expression D·2^(D-1) + 2D - 1.
Claim. The endogenous wallpaper count satisfies $W_endo(5) = 89$.
background
W_endo(d) is defined as passive_field_edges d + cube_faces d and expands to the closed form d · 2^(d-1) + 2d - 1. The WEndoForcing module uses this quantity to show W_endo(D) = 17 if and only if D = 3, supplying the arithmetic core of the Tr7 step. The definition is imported from BaselineDerivation, where it is introduced as the sum of passive field edges and cube faces for a D-cube.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic expression for W_endo at 5 directly from its definition.
why it matters
This instance supports the general claim that W_endo(D) > 17 for all D ≥ 4, which forces D = 3 in the Recognition Science framework. It fills the D = 5 case in the Tr7 argument of the WEndoForcing module and aligns with the eight-tick octave and D = 3 landmark. The result feeds the uniqueness statement dimension_unique_from_W_endo.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.