Geometry Dihedral Angle

The hinge angle

A dihedral angle is the angle between two intersecting planes. Picture an open book: the angle between the two pages is a dihedral angle, measured along their shared edge, the spine. In geometry, this angle is defined for any two faces that meet along an edge, such as the faces of a pyramid or the sides of a box. Its cosine can be computed from the edge lengths alone, using a formula from Cayley-Menger determinants, which give the volume of a simplex from its side lengths.

In a regular tetrahedron, the simplest Platonic solid, the dihedral angle is arccos(1/3), about 70.53 degrees. In a cube, the angle between adjacent faces is exactly 90 degrees, or π/2 radians. These values are classical and well known. When several shapes meet around a single edge, the sum of their dihedral angles determines whether space is flat or curved at that edge. If the angles sum to 360 degrees, the region is flat; any shortfall is called the deficit angle, a measure of positive curvature.

In Recognition Science, the framework models physical space as a discrete record of recognition events, and it treats conventional geometry as a derived structure. The module in question, a machine-checked library of formal theorems, formalizes dihedral angles for simplices, the building blocks of triangulated spaces. It defines a ledger, a discrete record of events, for each angle: a cosine value together with a proof that this cosine lies between -1 and 1. From this data, the angle itself is defined as the arccosine, and the framework proves that this angle always lies between 0 and π.

The library then establishes the canonical values. It proves that the regular tetrahedron's dihedral angle is arccos(1/3), and that the cube's is exactly π/2. It also formalizes the flat-space condition: at an edge where space is flat, the dihedral angles of the surrounding shapes sum to 2π. The library proves that four cube angles, each π/2, sum to 2π, confirming that the cubic lattice is flat. The deficit, defined as 2π minus the sum, is proved to be zero in this flat case.

This formalization is a step toward a larger goal: checking the Regge calculus, a method that approximates curved spacetime by flat pieces. The module provides the angle data needed to state Schläfli's identity and to discharge the deficit linearization hypothesis. In plain terms, the module gives a precise, verified language for talking about angles in a piecewise-flat space, and it confirms the basic flat cases that any such theory must get right.

/-- The regular-tetrahedron dihedral angle is `arccos(1/3) ≈ 70.53°`. -/
theorem regular_tet_dihedral_theta :
    regular_tet_dihedral.theta = Real.arccos (1/3) := rfl

/-- The cube dihedral is `π / 2` exactly. -/
theorem cube_dihedral_theta : cube_dihedral.theta = Real.pi / 2 := by
  unfold DihedralAngleData.theta cube_dihedral
  simp only
  exact Real.arccos_zero

/-- Four cube-dihedral angles (`π/2 + π/2 + π/2 + π/2 = 2π`) sum to `2π`:
    the classical "Z³ lattice is flat" statement. -/
theorem cubic_lattice_flatSum :
    FlatSumCondition [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] := by
  unfold FlatSumCondition sumThetas
  simp only [List.map, List.sum_cons, List.sum_nil, cube_dihedral_theta]
  ring

/-- At a flat hinge, the deficit is zero. -/
theorem deficit_eq_zero_of_flat (ds : List DihedralAngleData)
    (h : FlatSumCondition ds) : deficit ds = 0 := by
  unfold deficit
  rw [h]; ring

What this page does not claim

This module does not prove that any particular physical space is flat or curved; it only formalizes the angle data and the flat-sum condition. The module does not derive the dihedral angle formula from Cayley-Menger determinants; it takes the cosine value as given data.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/DihedralAngle.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: