IndisputableMonolith.Geometry.DihedralAngle

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
   3import IndisputableMonolith.Geometry.CayleyMenger
   4
   5/-!
   6# Dihedral Angles for Simplices
   7
   8This module sets up dihedral angles at edges and 2-faces of simplices
   9from Cayley-Menger data. It is Phase C2 of the program to discharge the
  10Regge deficit linearization hypothesis on general simplicial complexes.
  11
  12## Scope
  13
  14A dihedral angle at an edge of a tetrahedron is the angle between the
  15two faces containing that edge. Classically,
  16
  17  cos(θ_e) = (CM_45) / √(CM_43 · CM_53)
  18
  19where `CM_ij` is a minor of the Cayley-Menger matrix (see Berger,
  20*Geometry I*, §9.7). The exact formula is lengthy but explicit.
  21
  22We take the same honest minimal approach as Phase C1:
  23
  24- Define a `DihedralAngleData` structure that carries a cosine value
  25  and a bound `−1 ≤ cos ≤ 1`, matching the existing
  26  `IndisputableMonolith/Gravity/ReggeCalculus.DihedralAngleData`.
  27- Define the canonical dihedral angle `θ = arccos(cos)`.
  28- Prove its range `θ ∈ [0, π]`.
  29- Unconditionally evaluate the *regular-tetrahedron* dihedral angle:
  30  `θ = arccos(1/3) ≈ 70.53°`.
  31- Unconditionally evaluate the *cube* dihedral angle: `θ = π/2`.
  32- Record the flat-space sum `Σ_σ θ_σ = 2π` at a non-singular edge as
  33  a Prop-valued condition (named `FlatSumCondition`), exactly as Regge
  34  calculus uses it.
  35
  36## What this enables
  37
  38Phase C3 (`Schlaefli.lean`) references `DihedralAngleData` to state
  39Schläfli's identity. Phase C5 threads both through the final simplicial
  40discharge.
  41
  42Zero `sorry`, zero new `axiom`.
  43-/
  44
  45namespace IndisputableMonolith
  46namespace Geometry
  47namespace DihedralAngle
  48
  49open Real CayleyMenger
  50
  51noncomputable section
  52
  53/-! ## §1. Dihedral angle data -/
  54
  55/-- The data of a dihedral angle: a cosine value in `[-1, 1]`. -/
  56structure DihedralAngleData where
  57  cosine : ℝ
  58  cosine_lb : -1 ≤ cosine
  59  cosine_ub : cosine ≤ 1
  60
  61/-- The dihedral angle itself, via `arccos`. -/
  62def DihedralAngleData.theta (d : DihedralAngleData) : ℝ := Real.arccos d.cosine
  63
  64/-- `θ ∈ [0, π]`. -/
  65theorem theta_nonneg (d : DihedralAngleData) : 0 ≤ d.theta :=
  66  Real.arccos_nonneg d.cosine
  67
  68theorem theta_le_pi (d : DihedralAngleData) : d.theta ≤ Real.pi :=
  69  Real.arccos_le_pi d.cosine
  70
  71/-- `cos θ = cosine` by construction. -/
  72theorem cos_theta (d : DihedralAngleData) : Real.cos d.theta = d.cosine := by
  73  unfold DihedralAngleData.theta
  74  exact Real.cos_arccos d.cosine_lb d.cosine_ub
  75
  76/-! ## §2. Canonical values -/
  77
  78/-- A regular tetrahedron's dihedral angle has cosine `1/3`. -/
  79def regular_tet_dihedral : DihedralAngleData :=
  80  { cosine := 1 / 3
  81  , cosine_lb := by norm_num
  82  , cosine_ub := by norm_num
  83  }
  84
  85/-- The regular-tetrahedron dihedral angle is `arccos(1/3) ≈ 70.53°`. -/
  86theorem regular_tet_dihedral_theta :
  87    regular_tet_dihedral.theta = Real.arccos (1/3) := rfl
  88
  89/-- `arccos(1/3)` lies strictly between 0 and π. -/
  90theorem regular_tet_dihedral_in_open_interval :
  91    0 < regular_tet_dihedral.theta ∧ regular_tet_dihedral.theta < Real.pi := by
  92  refine ⟨?_, ?_⟩
  93  · rw [regular_tet_dihedral_theta]
  94    apply Real.arccos_pos.mpr
  95    norm_num
  96  · rw [regular_tet_dihedral_theta]
  97    have h_le : Real.arccos (1/3) ≤ Real.pi := Real.arccos_le_pi _
  98    have h_ne : Real.arccos (1/3) ≠ Real.pi := by
  99      intro h_eq
 100      rw [Real.arccos_eq_pi] at h_eq
 101      linarith
 102    exact lt_of_le_of_ne h_le h_ne
 103
 104/-- A cube's dihedral angle has cosine `0` (i.e. 90°). -/
 105def cube_dihedral : DihedralAngleData :=
 106  { cosine := 0
 107  , cosine_lb := by norm_num
 108  , cosine_ub := by norm_num
 109  }
 110
 111/-- The cube dihedral is `π / 2` exactly. -/
 112theorem cube_dihedral_theta : cube_dihedral.theta = Real.pi / 2 := by
 113  unfold DihedralAngleData.theta cube_dihedral
 114  simp only
 115  exact Real.arccos_zero
 116
 117/-! ## §3. Flat-sum conditions
 118
 119At a hinge (edge in 3D, 2-face in 4D) embedded in flat Euclidean space,
 120the dihedral angles of the simplices meeting at the hinge sum to `2π`.
 121This is the piecewise-flat analog of "no curvature at this hinge."
 122
 123We formalize this as a condition on a `List DihedralAngleData`. -/
 124
 125/-- The sum of the `theta` values over a list of dihedral data. -/
 126def sumThetas (ds : List DihedralAngleData) : ℝ :=
 127  (ds.map DihedralAngleData.theta).sum
 128
 129/-- The flat-sum condition: the total dihedral angle at a hinge equals `2π`. -/
 130def FlatSumCondition (ds : List DihedralAngleData) : Prop :=
 131  sumThetas ds = 2 * Real.pi
 132
 133/-- The deficit at a hinge is `2π − Σ θ`. -/
 134def deficit (ds : List DihedralAngleData) : ℝ :=
 135  2 * Real.pi - sumThetas ds
 136
 137/-- At a flat hinge, the deficit is zero. -/
 138theorem deficit_eq_zero_of_flat (ds : List DihedralAngleData)
 139    (h : FlatSumCondition ds) : deficit ds = 0 := by
 140  unfold deficit
 141  rw [h]; ring
 142
 143/-- Four cube-dihedral angles (`π/2 + π/2 + π/2 + π/2 = 2π`) sum to `2π`:
 144    the classical "Z³ lattice is flat" statement. -/
 145theorem cubic_lattice_flatSum :
 146    FlatSumCondition [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] := by
 147  unfold FlatSumCondition sumThetas
 148  simp only [List.map, List.sum_cons, List.sum_nil, cube_dihedral_theta]
 149  ring
 150
 151/-- The deficit at a flat cubic hinge is zero (the baseline identity
 152    already present in `ReggeCalculus.cubic_lattice_flat` for the
 153    π/2 × 4 = 2π case, now lifted to the `DihedralAngle` API). -/
 154theorem cubic_lattice_deficit_zero :
 155    deficit [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] = 0 :=
 156  deficit_eq_zero_of_flat _ cubic_lattice_flatSum
 157
 158/-! ## §4. Certificate -/
 159
 160structure DihedralAngleCert where
 161  cube_is_right_angle : cube_dihedral.theta = Real.pi / 2
 162  regular_tet_in_range :
 163    0 < regular_tet_dihedral.theta ∧ regular_tet_dihedral.theta < Real.pi
 164  cubic_flat_sum :
 165    FlatSumCondition [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral]
 166  cubic_deficit_zero :
 167    deficit [cube_dihedral, cube_dihedral, cube_dihedral, cube_dihedral] = 0
 168  theta_in_range : ∀ d : DihedralAngleData, 0 ≤ d.theta ∧ d.theta ≤ Real.pi
 169  cos_theta_eq : ∀ d : DihedralAngleData, Real.cos d.theta = d.cosine
 170
 171theorem dihedralAngleCert : DihedralAngleCert where
 172  cube_is_right_angle := cube_dihedral_theta
 173  regular_tet_in_range := regular_tet_dihedral_in_open_interval
 174  cubic_flat_sum := cubic_lattice_flatSum
 175  cubic_deficit_zero := cubic_lattice_deficit_zero
 176  theta_in_range := fun d => ⟨theta_nonneg d, theta_le_pi d⟩
 177  cos_theta_eq := cos_theta
 178
 179end
 180
 181end DihedralAngle
 182end Geometry
 183end IndisputableMonolith
 184