vertex_angular_deficit
plain-language theorem explainer
Angular deficit at each vertex of the cubic cell Q₃ is defined as 2π minus three times the right dihedral angle. Discrete curvature calculations in Recognition Science cite this when recovering total curvature via Gauss-Bonnet on the boundary of Q₃. It is introduced as a direct algebraic expression that subtracts the product of the fixed face count per vertex and the cube dihedral from 2π.
Claim. The angular deficit at each vertex of the cube $Q_3$ is $2π - 3 · (π/2)$.
background
The Alpha Derivation module derives α^{-1} from the geometry of the cubic ledger Q₃ in three dimensions. Cube geometry fixes eight vertices, twelve edges and six faces, with three square faces meeting at each vertex and dihedral angle π/2 between adjacent faces. The vertex angular deficit measures the discrete curvature concentrated at each corner of this fundamental cell during one recognition tick.
proof idea
One-line definition that subtracts the product of faces_per_vertex (equal to 3) and cube_dihedral (equal to π/2) from 2π.
why it matters
This definition supplies the per-vertex curvature term that feeds gauss_bonnet_Q3, which proves the sum of eight deficits equals 4π and thereby recovers 2π χ(S²). It realizes the discrete Gauss-Bonnet step in the module's derivation of α from cubic geometry, consistent with D = 3 forced at T8 of the UnifiedForcingChain. Downstream solid_angle_Q3 reuses the identical expression for the total solid angle seen from an interior point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.