faces_per_vertex
plain-language theorem explainer
faces_per_vertex fixes the count of square faces incident to each vertex of the cubic cell Q₃ at the integer 3. Derivations of the fine-structure constant from the discrete geometry of the ledger cite this value when evaluating vertex curvature. The declaration consists of a direct constant assignment drawn from the D=3 cube geometry.
Claim. In the cubic lattice $Q_3$, exactly three faces meet at each vertex.
background
The AlphaDerivation module constructs the fine-structure constant from the geometry of the cubic ledger in three dimensions. The fundamental unit cell Q₃ has eight vertices, twelve edges and six faces, with one active edge per recognition tick and eleven passive edges. Upstream SpectralEmergence shows that Q₃ simultaneously forces the gauge group SU(3)×SU(2)×U(1) and exactly three particle generations from face-pair counting.
proof idea
The declaration is a one-line definition that directly assigns the natural number 3 to faces_per_vertex, encoding the three square faces meeting at each corner of Q₃. No upstream lemmas are invoked in the body.
why it matters
This constant enters the computation of the vertex angular deficit, which sums over eight vertices to yield the total curvature 4π on the boundary of Q₃ via discrete Gauss-Bonnet. It supports the geometric seed 4π·11 for α^{-1} and aligns with the D=3 forcing step in the unified chain. The definition feeds vertex_angular_deficit and vertex_deficit_eq in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.