euler_char_cube
plain-language theorem explainer
The boundary of the elementary 3-cube has Euler characteristic χ = V − E + F = 8 − 12 + 6 = 2, matching χ(S²). Anyone citing the non-circular λ_rec chain (Gauss-Bonnet on ∂Q₃) needs this combinatorial identity. The proof is a one-line numerical check of the four constant definitions.
Claim. For the 3-cube cell $Q_3$ with $V=8$ vertices, $E=12$ edges and $F=6$ faces, the integer Euler characteristic equals that of the 2-sphere: $V - E + F = \chi(S^2) = 2$.
background
This module derives the recognition length $\lambda_{\mathrm{rec}}$ in four steps from the recognition composition law and polyhedral Gauss-Bonnet on the elementary cell $Q_3$, with no free parameter and no fit to data (paper: RS_Lambda_Rec_Derivation).
Cost minimization on the discrete ledger forces $D=3$ and the cube $Q_3$ as the recognition cell. The boundary $\partial Q_3$ is combinatorially a topological 2-sphere. The raw cube counts are fixed defs: $Q_3$ vertices $=8$, edges $=12$, faces $=6$; the sphere reference is $\mathrm{euler_S2}:=2$.
Upstream AlphaHigherOrder packages the same counts as $2^3$, $3\cdot 2^2$, $2\cdot 3$. The identity here is pure combinatorics: no metric, angles, or curvature yet. It supplies $\chi(\partial Q_3)=2$ for the later Gauss-Bonnet normalization that produces the curvature cost.
proof idea
Term-mode proof by norm_num on the four constants. Unfold vertices $=8$, edges $=12$, faces $=6$, and $\chi(S^2)=2$, then discharge the integer equality $8-12+6=2$. No lemmas beyond the definitions; no induction or topology.
why it matters
Step (III) of the $\lambda_{\mathrm{rec}}$ chain needs $\chi(\partial Q_3)=\chi(S^2)=2$ so that polyhedral Gauss-Bonnet fixes integrated curvature at $4\pi$ and forces the curvature cost $J_{\mathrm{curv}}(\lambda)=2\lambda^2$. That cost is then balanced against the normalized bit cost $J_{\mathrm{bit}}=1$ to give the unique positive root $\lambda_{\mathrm{rec}}=1/\sqrt{2}$ in cost units.
Downstream the module uses this combinatorial $\chi$ inside the curvature-cost and balance development (siblings $J_{\mathrm{curv}}$, $\mathrm{balance_at_lambda_0}$, $\mathrm{lambda0_forced_in_cost_units}$). Framework landmarks: T8 forces $D=3$ and the cube cell; the identity closes the combinatorial half of "$\partial Q_3\cong S^2$" before geometry enters. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.