Geometry Dihedral Angle Regular Tet Dihedral In Open Interval

The regular tetrahedron's angle

The dihedral angle of a regular tetrahedron is the angle between two of its triangular faces. For a regular tetrahedron, all six edges are equal, and the angle is the same at every edge. Its cosine is exactly 1/3, so the angle itself is arccos(1/3), approximately 70.53 degrees. This value is a classical result in solid geometry, derivable from the dot product of the face normals or from the Cayley-Menger determinant.

The declaration regular_tet_dihedral_in_open_interval is a theorem in the machine-checked library of formal theorems. It states that the angle, defined as the arccosine of 1/3, is strictly greater than 0 and strictly less than π (180 degrees). This is a precise, unconditional statement: it holds for the regular tetrahedron without any additional assumptions. The proof is immediate from the properties of the arccosine function, since 1/3 lies strictly between -1 and 1.

In Recognition Science, this theorem is part of a larger program to formalize Regge calculus, a discrete approach to general relativity where spacetime is approximated by flat simplices. The angle at an edge of a tetrahedron is defined from Cayley-Menger data, which encodes the edge lengths. The framework's library proves the range of the angle, the exact value for the regular tetrahedron, and the flat-sum condition: at a hinge in flat space, the dihedral angles around it sum to 2π. This particular theorem, however, does not itself assert anything about curvature, gravity, or the Regge deficit. It is a geometric fact, not a physical claim.

What the theorem does not claim is as important as what it proves. It does not claim that the regular tetrahedron's angle is the only possible value, nor does it relate the angle to any Recognition Science constant or forcing chain. It does not assert that the angle is irrational or transcendental; arccos(1/3) is a specific real number, and the theorem only pins its range. The theorem also does not claim that the angle is the same for all tetrahedra, only for the regular one. Finally, it does not claim anything about the sum of angles around an edge in a curved simplicial complex; that is a separate condition, formalized elsewhere as the flat-sum condition.

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

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

What this page does not claim

The theorem does not claim the angle is irrational or transcendental. The theorem does not claim anything about curvature or the Regge deficit. The theorem does not claim the angle is the same for all tetrahedra.

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: