Geometry Dihedral Angle Regular Tet Dihedral Theta

The regular tetrahedron's angle

A regular tetrahedron is a pyramid with four identical equilateral triangular faces. The dihedral angle is the angle between two faces that share an edge, measured inside the solid. For this shape, the angle is the same at every edge, and its cosine is exactly one third. That means the angle is arccos(1/3), which is about 70.53 degrees. This value is not new: it appears in classical solid geometry, where it is often derived from the dot product of face normals or from the geometry of a cube.

In the Recognition Science framework, this classical fact is formalized in a machine-checked library of formal theorems. The declaration regular_tet_dihedral_theta states that the dihedral angle of a regular tetrahedron, defined from Cayley-Menger data, equals arccos(1/3). The proof is a definitional equality, meaning the value follows directly from how the angle is defined. The framework also proves that this angle lies strictly between 0 and π, and that for a cube the dihedral angle is exactly π/2, or 90 degrees. These are not new discoveries; they are formal restatements of known geometry.

The framework's library also records the flat-space sum condition: at a hinge where simplices meet in flat Euclidean space, the dihedral angles sum to 2π. For four cube angles, this gives π/2 + π/2 + π/2 + π/2 = 2π, which is the statement that the cubic lattice is flat. The deficit at such a hinge is zero. These facts are part of a larger program to discharge the Regge deficit linearization hypothesis on simplicial complexes, a step toward relating discrete geometry to general relativity.

What the declaration does not claim is important. It does not derive the dihedral angle from the framework's cost function or forcing chain; it simply formalizes a classical geometric result. It does not claim that the regular tetrahedron's angle has any special significance in Recognition Science beyond being a canonical value. And it does not prove that the flat-sum condition holds for any particular physical configuration; that remains a condition to be verified, not a theorem about the world.

/-- 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

/-- `arccos(1/3)` lies strictly between 0 and π. -/
theorem regular_tet_dihedral_in_open_interval :
    0 < regular_tet_dihedral.theta ∧ regular_tet_dihedral.theta < Real.pi := by
  refine ⟨?_, ?_⟩
  · rw [regular_tet_dihedral_theta]
    apply Real.arccos_pos.mpr
    norm_num
  · rw [regular_tet_dihedral_theta]
    have h_le : Real.arccos (1/3) ≤ Real.pi := Real.arccos_le_pi _
    have h_ne : Real.arccos (1/3) ≠ Real.pi := by
      intro h_eq
      rw [Real.arccos_eq_pi] at h_eq
      linarith
    exact lt_of_le_of_ne h_le h_ne

/-- 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

/-- The flat-sum condition: the total dihedral angle at a hinge equals `2π`. -/
def FlatSumCondition (ds : List DihedralAngleData) : Prop :=
  sumThetas ds = 2 * Real.pi

/-- 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

What this page does not claim

The dihedral angle value is not derived from the Recognition Science cost function or forcing chain. The flat-sum condition is not proved for any specific physical configuration; it is a condition to be verified. The regular tetrahedron's angle has no special significance in the framework beyond being a canonical geometric value.

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: