cube_dihedral
The dihedral angle of the cube Q₃ is defined as π/2. Researchers deriving α⁻¹ from the cubic ledger cite this value when summing vertex deficits to obtain the 4π total curvature. The definition is a direct assignment of the Euclidean right angle between adjacent square faces.
claimThe dihedral angle of the cube $Q_3$ equals $π/2$.
background
The module derives α⁻¹ from the geometry of the cubic ledger in D = 3. Cube geometry fixes 8 vertices, 12 edges and 6 faces; one edge is active per recognition tick while the remaining 11 are passive field edges. The dihedral angle enters vertex angular deficit as 2π − 3(π/2) and supplies the base angle for the discrete Gauss-Bonnet identity on ∂Q₃. Upstream results on SpectralEmergence record that Q₃ simultaneously forces SU(3) × SU(2) × U(1) gauge content and exactly three particle generations from face-pair counting.
proof idea
One-line definition that directly assigns the known Euclidean value Real.pi / 2.
why it matters in Recognition Science
This supplies the constant angle used by vertex_angular_deficit and vertex_deficit_eq, which together establish that the sum of eight vertex deficits equals 4π. The result anchors the geometric seed 4π · 11 in the alpha derivation and the D = 3 eight-tick octave of the forcing chain. It closes the crystallographic closure step (6 faces × 17 wallpaper groups + 1 Euler term = 103) that produces the curvature term 103/102π⁵.
scope and limits
- Does not derive the angle from Recognition forcing axioms.
- Does not apply to non-cubic polyhedra or curved lattices.
- Does not incorporate higher-order curvature corrections.
- Does not compute numerical approximations beyond the exact π/2.
formal statement (Lean)
105noncomputable def cube_dihedral : ℝ := Real.pi / 2
proof body
Definition body.
106
107/-- Faces meeting at each vertex of Q₃ (three square faces at each corner). -/