N0_ne_W_at_D5
plain-language theorem explainer
The result shows that twice the vertex count of the five-dimensional cube plus one differs from the plugged-in expression for W at dimension five, confirming the equality between these quantities holds only at D=3. Researchers studying dimension forcing within Recognition Science would cite this when establishing the uniqueness of three spatial dimensions. The proof evaluates the concrete numerical inequality directly via native decision procedures.
Claim. $2V(5) + 1 ≠ (5 · 2^4 - 1) + 2·5$, where $V(d) = 2^d$ is the vertex count of the $d$-cube.
background
The module proves that the integers {13, 11, 6, 8} match the cell counts of the three-dimensional cube Q3 and satisfy algebraic constraints including cyclic chains and the partition of 2D^D + 1 = 55. Assignments of these counts to specific fermion sectors are identified from PDG data for quarks, while lepton torsion and the D=3 coincidence are derived without data. Key definitions include cube_vertices'(d) := 2^d for the vertices of Q_d and E(d) := d · 2^(d-1) for the edges of the D-cube, as supplied by the upstream SpectralEmergence result.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the inequality 65 ≠ 89 directly.
why it matters
This declaration supports the module's claim that W = 2V + 1 = N0 holds only for D=3, supplying a genuine derivation of the dimension-forcing condition. It aligns with the T8 step in the unified forcing chain that selects D=3 spatial dimensions. No downstream theorems are listed, but the result closes a verification point for the D=3 uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.