dihedral_angle
plain-language theorem explainer
The declaration assigns the cube dihedral angle the constant value π/2. Workers deriving λ_rec from curvature cost in the Recognition framework cite this value to evaluate vertex deficits under Gauss-Bonnet normalization. The assignment is a direct constant with no lemmas or reductions.
Claim. The dihedral angle at each cube edge equals $π/2$.
background
This definition sits inside the LambdaRecDerivation module, which obtains λ_rec non-circularly from normalized bit cost (=1) and curvature cost (=2λ²) taken from the Q₃ Gauss-Bonnet normalization; G is then recovered as π λ_rec² c³ / ℏ. The local geometry is supplied by upstream deficit operations: DihedralAngle.deficit computes 2π − Σ θ at a hinge, while Schlaefli.deficit lifts the same operation to simplicial hinge data. The cube is used here only as a regular polyhedron whose three faces meet at each vertex.
proof idea
The definition is a one-line constant assignment of Real.pi / 2. No tactics, lemmas, or upstream results are invoked; the value is supplied directly for later unfolding in angular_deficit_per_vertex and angular_deficit_value.
why it matters
The constant is the immediate input to angular_deficit_per_vertex and to the theorem angular_deficit_value, which together recover the total curvature 4π = 2π χ(S²) for the cube and thereby close the Gauss-Bonnet step in the non-circular λ_rec derivation. It therefore supports the spatial structure (D = 3) presupposed by the eight-tick octave and the curvature functional K(λ) used throughout the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.