IndisputableMonolith.Geometry.SchlaefliN

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   3import IndisputableMonolith.Geometry.CayleyMengerN
   4
   5/-!
   6# Dimension-Parametric Schläfli Interface
   7
   8This module states the n-dimensional Schläfli identity in a finite-index
   9form.  The 3D tetrahedral theorem can later be shown to instantiate this
  10interface at `n = 3`.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Geometry
  15namespace SchlaefliN
  16
  17noncomputable section
  18
  19/-- Abstract hinge data for an n-simplex: a hinge is codimension two, so
  20its measure is an `(n-2)`-volume. -/
  21structure HingeDataN where
  22  measure : ℝ
  23  measure_nonneg : 0 ≤ measure
  24
  25/-- Schläfli derivative data in dimension `n`, over finitely many hinges and
  26edge-length coordinates. -/
  27structure SchlaefliDataN (nH nE : ℕ) where
  28  hinge : Fin nH → HingeDataN
  29  dTheta_dL : Fin nH → Fin nE → ℝ
  30
  31/-- The n-dimensional Schläfli identity:
  32`Σ_h V_{n-2}(h) · ∂θ_h/∂L_e = 0` for every edge coordinate `e`. -/
  33def SchlaefliIdentityN {nH nE : ℕ} (D : SchlaefliDataN nH nE) : Prop :=
  34  ∀ e : Fin nE, ∑ h : Fin nH, (D.hinge h).measure * D.dTheta_dL h e = 0
  35
  36/-- Direct eliminator for the n-dimensional identity. -/
  37theorem schlaefliN_kills_angle_term {nH nE : ℕ}
  38    (D : SchlaefliDataN nH nE) (hS : SchlaefliIdentityN D) (e : Fin nE) :
  39    ∑ h : Fin nH, (D.hinge h).measure * D.dTheta_dL h e = 0 :=
  40  hS e
  41
  42end
  43
  44end SchlaefliN
  45end Geometry
  46end IndisputableMonolith
  47