cube_edges
plain-language theorem explainer
cube_edges supplies the closed-form count of edges in a d-dimensional hypercube as d times 2 to the power d-1. Derivations of the fine-structure constant in Recognition Science cite the D=3 case to fix the total at 12 and the passive field edges at 11. The definition is a direct algebraic expression with no lemmas or tactics.
Claim. The number of edges in a $d$-dimensional hypercube is $d · 2^{d-1}$.
background
The Alpha Derivation module starts from the cubic ledger Q₃ as the fundamental unit cell forced by the Meta-Principle on Z³. D is fixed at 3 by the upstream forcing chain. Standard hypercube combinatorics then give vertices 2^D, edges d·2^(d-1), and faces 2d. These counts separate active edges (one per recognition tick) from the remaining passive field edges that dress the vacuum geometry.
proof idea
Direct definition that implements the standard hypercube edge formula. No lemmas are invoked and no tactics are applied; the expression is the closed combinatorial form.
why it matters
The definition anchors the geometric seed 4π·11 and the seam numerator 6·17+1 inside alpha_ingredients_from_D3_cube and eleven_is_forced. Those theorems close the provenance of all numerical constants in the α^{-1} derivation to D=3 cube geometry, consistent with the eight-tick octave and the T8 forcing of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.