IndisputableMonolith.Geometry.RealisabilityCone

   1import IndisputableMonolith.Geometry.CayleyMengerMatrix
   2
   3/-!
   4# Reallisability Cone for Tetrahedral Squared Edges
   5
   6This module defines the open domain on which the tetrahedral
   7Cayley-Menger and dihedral-angle formulas are intended to be used.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Geometry
  12namespace RealisabilityCone
  13
  14open CayleyMengerPolynomial
  15open CayleyMengerMatrix
  16
  17noncomputable section
  18
  19/-- Basic open tetrahedral cone: positive squared edge lengths and positive
  20Cayley-Menger determinant.  Later phases strengthen this with face-minor
  21positivity as needed by cofactor denominators. -/
  22def RealisableTetCone : Set SqEdges :=
  23  {a | (∀ i : Fin 6, 0 < a i) ∧ 0 < cm3 a}
  24
  25/-- Membership unpacking: all squared edges are positive. -/
  26theorem RealisableTetCone.edge_pos {a : SqEdges} (ha : a ∈ RealisableTetCone) :
  27    ∀ i : Fin 6, 0 < a i :=
  28  ha.1
  29
  30/-- Membership unpacking: Cayley-Menger determinant is positive. -/
  31theorem RealisableTetCone.cm_pos {a : SqEdges} (ha : a ∈ RealisableTetCone) :
  32    0 < cm3 a :=
  33  ha.2
  34
  35/-- The regular unit tetrahedron lies in the basic realisability cone. -/
  36theorem regularUnit_mem_realisableTetCone :
  37    regularUnitSqEdges ∈ RealisableTetCone := by
  38  constructor
  39  · intro i
  40    unfold regularUnitSqEdges
  41    norm_num
  42  · rw [cm3_regular_unit]
  43    norm_num
  44
  45/-- The right-angle unit tetrahedron lies in the basic realisability cone. -/
  46theorem rightAngleUnit_mem_realisableTetCone :
  47    rightAngleUnitSqEdges ∈ RealisableTetCone := by
  48  constructor
  49  · intro i
  50    unfold rightAngleUnitSqEdges
  51    fin_cases i <;> norm_num
  52  · rw [cm3_rightAngle_unit]
  53    norm_num
  54
  55end
  56
  57end RealisabilityCone
  58end Geometry
  59end IndisputableMonolith
  60