dihedral_angle
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the angle from any Recognition Science cost function or J-equation.
- Does not apply to polyhedra other than the cube.
- Does not compute angular deficits or total curvature.
- Does not reference λ_rec, G, or the alpha band.
- Does not participate in the T0–T8 forcing chain.
Lean usage
theorem angular_deficit_value : angular_deficit_per_vertex = Real.pi / 2 := by unfold angular_deficit_per_vertex dihedral_angle; ringformal statement (Lean)
153noncomputable def dihedral_angle : ℝ := Real.pi / 2
proof body
Definition body.
154
155/-- At each cube vertex, 3 faces meet. The angular deficit is 2π - 3(π/2). -/