angular_deficit_per_vertex
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not sum deficits over all vertices.
- Does not solve for λ_rec.
- Does not invoke the Recognition Composition Law.
- Does not reference the forcing chain T0-T8.
formal statement (Lean)
156noncomputable def angular_deficit_per_vertex : ℝ := 2 * Real.pi - 3 * dihedral_angle
proof body
Definition body.
157
158/-- The angular deficit at each vertex equals π/2. -/