angular_deficit_per_vertex
plain-language theorem explainer
Angular deficit per vertex is defined as 2π minus three times the dihedral angle of π/2. Derivations of the recognition length λ_rec from curvature balance cite this when applying Gauss-Bonnet to the cube. The definition is a direct algebraic substitution from the dihedral angle definition.
Claim. The angular deficit per vertex in the cube is given by $2π - 3·(π/2)$.
background
The LambdaRecDerivation module derives λ_rec non-circularly from the normalized bit cost (=1) and curvature cost (=2λ²) via Q3 Gauss-Bonnet normalization, without presupposing G. The dihedral angle is defined upstream as π/2, the right angle between cube faces. The general deficit at a hinge is 2π minus the sum of the dihedral angles, as stated in the DihedralAngle and Schlaefli modules.
proof idea
One-line definition that substitutes the upstream dihedral_angle value π/2 into the expression 2π - 3θ.
why it matters
This supplies the per-vertex term for total_curvature_gauss_bonnet and the GDerivationChain structure. The chain runs from Q3 combinatorics (8 vertices) through Gauss-Bonnet total curvature 4π to the balance equation fixing λ_rec, then defines G = λ_rec² c³/(π ℏ). It realizes the curvature cost normalization step that connects to the phi-ladder and eight-tick octave in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.