euler_identity_Q3
plain-language theorem explainer
The Euler characteristic identity for the 3-cube equates vertex plus face count minus body to edge count plus one. Mass modelers enumerating generation steps in Recognition Science cite it to confirm 13 arises as both V+F-C and E+1. The proof evaluates the closed-form cell-count expressions at dimension 3 via native decision.
Claim. Let $V(d)=2^d$, $E(d)=d·2^{d-1}$, $F(d)=2d$ and $C=1$ denote the numbers of vertices, edges, faces and body cells of the $d$-dimensional cube. Then for $d=3$, $V(3)+F(3)-C=E(3)+1$.
background
The Step Value Enumeration module narrows the open forcing step by proving structural constraints on the generation values 13, 11, 6, 8 as Q3 cube invariants at D=3. It imports the cell-count definitions from SectorDependentTorsion: vertices of Qd equal 2 to the d, edges equal d times 2 to the d-1, faces equal 2d, and body always 1. The module doc notes that the Euler relation V-E+F=2 on the boundary sphere rearranges directly to the stated identity when the body cell count is 1.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the arithmetic expressions for the cell counts at d=3, confirming both sides equal 13.
why it matters
This identity is invoked by the downstream theorem thirteen_natural_interpretations to show that 13 admits three equivalent natural-invariant interpretations. It supplies the explicit structural constraint required by the module to make the choice of generation steps from PDG data an explicit modeling decision rather than a hidden one. The result sits inside the D=3 forcing step of the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.