angular_deficit_value
plain-language theorem explainer
The angular deficit at each vertex of the cube equals π/2. Researchers deriving the recognition length λ_rec from curvature costs in the non-circular Gauss-Bonnet normalization would cite this when evaluating the cube geometry. The proof is a one-line term that unfolds the definitions of angular_deficit_per_vertex and dihedral_angle then applies ring simplification.
Claim. The angular deficit at each vertex of the cube equals $π/2$.
background
The module formalizes the curvature-extremum derivation of the recognition length λ_rec. It is non-circular: it uses only the bit cost normalized to 1 and the curvature cost 2λ² from the Q₃ Gauss-Bonnet normalization, without reference to Newton's constant G. G is defined afterwards as π λ_rec² c³ / ℏ. The local setting is the explicit non-circular structure for the curvature functional in the constants domain.
proof idea
The proof is a one-line term that unfolds angular_deficit_per_vertex (defined as 2π - 3·dihedral_angle) and dihedral_angle (defined as π/2), then applies the ring tactic to reduce the expression directly to π/2.
why it matters
This supplies the per-vertex value required by the downstream total_curvature_gauss_bonnet theorem, which states that total curvature over the eight vertices equals 4π = 2π × χ(S²) and identifies this as the Gauss-Bonnet theorem for the cube. It fills the curvature normalization step in the λ_rec derivation and connects to the eight-tick octave together with the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.