Geometry Dihedral Angle Dihedral Angle Cert

The certificate

A dihedral angle is the angle between two faces of a solid that share an edge. For a cube, that angle is 90 degrees; for a regular tetrahedron, it is about 70.53 degrees, the angle whose cosine is 1/3. These angles appear throughout geometry and physics, wherever solids meet along edges.

The certificate, a machine-checked bundle of formal theorems, gathers the essential facts about dihedral angles into one structure. It records that the cube's dihedral angle is exactly π/2, that the regular tetrahedron's angle lies strictly between 0 and π, and that four right angles sum to 2π, the flat-space condition. It also states that every dihedral angle in the framework lies between 0 and π, and that its cosine recovers the original data by construction.

In Recognition Science, this certificate is part of a program to discharge the Regge deficit linearization hypothesis on general simplicial complexes. The flat-sum condition, where angles around a hinge sum to 2π, is the piecewise-flat analog of zero curvature at that hinge. The certificate proves the cubic lattice is flat in this sense, a baseline identity for the framework's gravity work.

The certificate does not claim to derive the fine-structure constant, prove the Riemann Hypothesis, or establish the physical bridge from recognition to linking. It is a formal object, not a physical law. It does not say that any particular physical solid has these angles; it says that if a solid is modeled with this data, then these angle facts hold.

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

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

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

/-- `θ ∈ [0, π]`. -/
theorem theta_nonneg (d : DihedralAngleData) : 0 ≤ d.theta :=
  Real.arccos_nonneg d.cosine

What this page does not claim

The certificate does not derive the fine-structure constant. The certificate does not prove the Riemann Hypothesis. The certificate does not establish the physical recognition-to-linking bridge.

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: