edges_at_D3
plain-language theorem explainer
The declaration establishes that the edge count of the three-dimensional hypercube equals 12 under the closed-form expression d times 2 to the power of d minus 1. Researchers tracing the factor of 12 in the Chudnovsky series for 1 over pi and the origin of 24 directed edges in the recognition ledger would cite this result. The proof is a direct native evaluation of the arithmetic identity at d equals 3.
Claim. The number of 1-cells in the three-dimensional hypercube is $3 times 2^{2} = 12$.
background
In the Sector-Dependent Generation Torsion module the definition cube_edges' computes the number of edges (1-cells) of the hypercube Q_d via the formula d times 2 to the power of d minus 1. The module verifies algebraic properties of the cell counts 13, 11, 6, 8 for Q3 while recording that fermion-sector assignments remain data-driven hypotheses except for the lepton torsion pair. The D=3 coincidence that W equals 2V plus 1 equals N0 holds only for D=3 and is derived without external data.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the definition of cube_edges' at argument 3, confirming the arithmetic identity 3 times 2 squared equals 12.
why it matters
This supplies the edge count 12 that feeds directly into directed_edges_Q3, which identifies the source of the magic number 24 in Ramanujan's modular discriminant, the Leech lattice dimension, and bosonic string theory. It also certifies the prefactor 12 in the Chudnovsky series as packaged in RamanujanPiCert. Within the Recognition framework the result anchors the D=3 forcing condition and the numerical link to the Ramanujan pi factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.