cube_faces
plain-language theorem explainer
The definition returns twice the input dimension to give the face count of a D-dimensional hypercube. Derivations of the fine-structure constant and the recognition wavelength from D=3 cube geometry cite this for the six-face case. The implementation is a direct arithmetic definition with no lemmas or computation steps.
Claim. The number of faces $F$ of a $D$-dimensional hypercube is given by $F(D) = 2D$.
background
In the Planck-Scale Matching module the derivation of the recognition wavelength from the ledger-curvature extremum begins with the bit-cost functional $J(x) = (x + x^{-1})/2 - 1$ evaluated at the self-similar fixed point and a curvature cost distributed over the faces of the three-dimensional cube. The same face-count expression appears upstream in AlphaDerivation as the basic count for hypercube geometry. The module sets $D=3$ to obtain the six faces that enter the solid-angle sum and the seam-denominator expressions used later in the alpha derivation.
proof idea
This is a direct definition that returns the product of 2 and the supplied natural number D.
why it matters
The definition supplies the face count that feeds alpha_ingredients_from_D3_cube and the subsequent solid-angle theorems that reconstruct $4pi$ from six equal contributions of $2pi/3$. It therefore anchors the geometric seed for the fine-structure constant inside the D=3 case of the forcing chain. The same count reappears in the curvature-cost term of the Planck-scale matching argument that yields lambda_rec approximately 0.564 Planck lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.