vertex_deficit_eq
plain-language theorem explainer
The equality establishes that the angular deficit at each vertex of the cubic cell Q₃ equals π/2. Researchers deriving the fine-structure constant from discrete curvature on the cubic ledger would cite this when summing eight vertex contributions to recover total curvature 4π. The proof is a direct algebraic reduction after unfolding the definitions of vertex angular deficit, faces per vertex, and the cube dihedral angle.
Claim. The angular deficit at each vertex of the unit cube $Q_3$, given by $2π - 3·(π/2)$, equals $π/2$.
background
In the Alpha Derivation module the fundamental unit cell is the cube Q₃ in D = 3 dimensions, with eight vertices, twelve edges and six faces. The dihedral angle between adjacent faces is π/2 and three faces meet at each vertex, so the angular deficit at a vertex is the difference between the full plane angle 2π and the sum of the three right angles. This deficit supplies the discrete curvature concentrated at vertices of the cubic ledger during each recognition tick.
proof idea
The proof is a one-line term-mode wrapper that unfolds the definitions of vertex_angular_deficit, faces_per_vertex and cube_dihedral, then applies the ring tactic to verify the algebraic identity 2π − 3·(π/2) = π/2.
why it matters
This supplies the per-vertex curvature term required by the downstream theorem gauss_bonnet_Q3, which shows that the total curvature of ∂Q₃ equals 4π and equals 2π times the Euler characteristic of the sphere. It fills the geometric seed step in the module's derivation of α⁻¹ from the cubic ledger geometry, linking directly to the framework's D = 3 and the discrete Gauss-Bonnet application on the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.