edges_at_D3
plain-language theorem explainer
The declaration asserts that a three-dimensional hypercube contains precisely twelve edges. Derivations of the fine-structure constant from lattice geometry and counts of directed recognition fluxes cite this count. The result follows from direct substitution into the closed-form expression for hypercube edges at the forced dimension of three.
Claim. When the spatial dimension equals three, the hypercube possesses exactly twelve edges.
background
This module constructs the fine-structure constant from the geometry of the cubic ledger. The hypercube in D dimensions has D times two to the power of D minus one edges. The framework forces D to equal three, yielding eight vertices, twelve edges, and six faces. One edge is active per recognition tick, leaving eleven passive field edges that enter the curvature calculation. Upstream results supply the general edge-counting function and a parallel statement in the sector-dependent torsion module.
proof idea
The proof evaluates the edge-counting function at D equals three using native decision procedures. It computes three multiplied by two to the power of two directly to obtain twelve.
why it matters
This supplies the base edge count for the passive-edge factor of eleven in the alpha derivation and for the twenty-four directed edges on the cube. The latter connects to Ramanujan's discriminant and the prefactor in the Chudnovsky series for one over pi. It anchors the geometric inputs to the recognition composition law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.