IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
   3import IndisputableMonolith.Geometry.CayleyMengerPolynomial
   4import IndisputableMonolith.Geometry.ReggeRigorousFoundation
   5import IndisputableMonolith.Geometry.DihedralCayleyMenger
   6
   7/-!
   8# Causal (CDT) Tetrahedron Classes and the Kinematical Wick Rotation (3D)
   9
  10QG Seven-Gaps campaign, Lorentzian-sector lane.  Every prior result of the
  11discrete gravity program (formal and numerical) is Euclidean.  This module
  12builds the first certified Lorentzian layer:
  13
  141. the causal (CDT-style) tetrahedron classes in D = 3, with the
  15   spacelike/timelike edge-type assignment verified combinatorially from the
  16   slice structure (decide-able lemmas);
  172. the Wick rotation as an explicit map on squared edge lengths, proved to be
  18   an involution and proved to act on the causal class as the algebraic
  19   continuation `alpha ↦ -alpha`;
  203. a non-degeneracy theorem for the Euclideanized simplices on an exact,
  21   hand-derived parameter range, with `NonDegenerateTet` instances;
  224. a deficit-angle reality corollary at the physical point `alpha = 1`.
  23
  24## Conventions (3D CDT, Ambjorn-Jurkiewicz-Loll)
  25
  26Spatial slices are 2D triangulated surfaces of equilateral triangles with
  27squared edge length `a^2`.  Spacetime between slices `t` and `t+1` is filled
  28by two tetrahedron types:
  29
  30* type (3,1): three vertices on slice `t`, one on slice `t+1`
  31  (3 spacelike + 3 timelike edges); the time-reflected type (1,3) has the
  32  same edge-length multiset and is covered by the same theorems;
  33* type (2,2): two vertices on each slice (2 spacelike + 4 timelike edges).
  34
  35Spacelike edges carry squared length `a^2`; timelike edges carry squared
  36length `-alpha * a^2` in the Lorentzian regime, `alpha > 0`.  The Wick
  37rotation flips the sign of the timelike squared lengths, i.e. it is the
  38continuation `alpha ↦ -alpha` on the causal class.
  39
  40Vertex/edge indexing follows `Geometry.CayleyMengerPolynomial`: vertices
  41`0,1,2,3`, edges `0=(0,1), 1=(0,2), 2=(0,3), 3=(1,2), 4=(1,3), 5=(2,3)`.
  42Slice assignment: for (3,1) vertices `{0,1,2}` lie on slice `t` and `3` on
  43slice `t+1`; for (2,2) vertices `{0,1}` lie on slice `t` and `{2,3}` on
  44slice `t+1`.
  45
  46## Derived thresholds (hand computation, certified below)
  47
  48With the Cayley-Menger polynomial `cm3` (equal to `288 V^2` on realizable
  49tetrahedra) and the Euclideanized tuples:
  50
  51* type (3,1): `cm3 = 2 * (3*alpha - 1) * a^6`, hence non-degenerate exactly
  52  for `alpha > 1/3` (`alphaMin threeOne = 1/3`); cross-check: the AJL volume
  53  `V(3,1) = (a^3/12) * sqrt (3*alpha - 1)` gives `288 V^2 = 2(3*alpha-1) a^6`;
  54* type (2,2): `cm3 = 4 * (2*alpha - 1) * a^6`, hence non-degenerate exactly
  55  for `alpha > 1/2` (`alphaMin twoTwo = 1/2`); cross-check:
  56  `V(2,2) = (a^3/12) * sqrt (4*alpha - 2)` gives `288 V^2 = 4(2*alpha-1) a^6`.
  57
  58Both types are simultaneously non-degenerate exactly for `alpha > 1/2`, the
  59standard 3d CDT Euclidean-regime bound.  The degeneracy at the threshold is
  60also proved (`cm3 = 0` at `alpha = alphaMin`), so the range is exact.  On the
  61Lorentzian side `cm3 < 0` for all `alpha >= 0`, so the Lorentzian tuples are
  62never Euclidean-realizable and the Wick rotation is genuinely required.
  63
  64## Honesty tiers
  65
  66* THEOREM: every declared theorem in this file is proved with zero sorry,
  67  zero admit, zero new axioms; hypotheses are explicit (`0 < a`,
  68  `alphaMin ty < alpha`, etc.).
  69* MODEL: `CausalTetType`, `sliceOf`, `isTimelike`, `lorentzianSqEdges`,
  70  `euclideanSqEdges`, `wick`, `alphaMin` are definitional encodings of the
  71  standard 3d CDT conventions.
  72* OPEN: the action-level Lorentzian continuation (complex dihedral angles,
  73  the sinh-action sector, boost-angle assignments at timelike hinges) is not
  74  attempted here; see `LorentzianSectorStatus`.  The symbolic-alpha dihedral
  75  reality range (arccos arguments strictly inside `(-1,1)` for all
  76  `alpha > alphaMin`) is also left open: the cofactor denominators are square
  77  roots of degree-2 Cayley-Menger minors, and their symbolic sign control is
  78  a separate fight.  The deficit-angle reality corollary is therefore proved
  79  at the concrete physical point `alpha = 1` (both types), where the
  80  Euclideanized tuples coincide with the regular tetrahedron.
  81
  82## decide usage (all on finite Bool-valued data, none on `ℝ`)
  83
  84`isTimelike_threeOne_eq_crossSlice`, `isTimelike_twoTwo_eq_crossSlice`,
  85`slice_count_threeOne`, `slice_count_twoTwo`, `timelike_count_threeOne`,
  86`spacelike_count_threeOne`, `timelike_count_twoTwo`, `spacelike_count_twoTwo`.
  87No `native_decide` anywhere.
  88-/
  89
  90namespace IndisputableMonolith
  91namespace Gravity
  92namespace SevenGaps
  93namespace CausalSimplexWick
  94
  95open Geometry.CayleyMengerPolynomial
  96open Geometry.ReggeRigorousFoundation
  97open Geometry.DihedralCayleyMenger
  98
  99/-! ## §1. The causal tetrahedron classes (combinatorial layer)
 100
 101MODEL: the two 3d CDT tetrahedron types and their slice structure. -/
 102
 103/-- The two causal tetrahedron types of 3d CDT between adjacent slices.
 104`threeOne` has three vertices on slice `t` and one on slice `t+1` (its time
 105reflection (1,3) has the same edge data); `twoTwo` has two vertices on each
 106slice. -/
 107inductive CausalTetType
 108  | threeOne
 109  | twoTwo
 110
 111/-- Slice membership of each vertex (`false` = slice `t`, `true` = slice
 112`t+1`).  For (3,1): vertices `0,1,2` on slice `t`, vertex `3` on `t+1`.
 113For (2,2): vertices `0,1` on slice `t`, vertices `2,3` on `t+1`. -/
 114def sliceOf : CausalTetType → Fin 4 → Bool
 115  | CausalTetType.threeOne, v => v.val == 3
 116  | CausalTetType.twoTwo, v => (v.val == 2) || (v.val == 3)
 117
 118/-- Edge-type assignment: `true` iff the edge is timelike (connects the two
 119slices).  For (3,1) the timelike edges are `{2,4,5}` (those touching the
 120apex vertex 3); for (2,2) they are `{1,2,3,4}` (the four cross edges). -/
 121def isTimelike : CausalTetType → Fin 6 → Bool
 122  | CausalTetType.threeOne, e => (e.val == 2) || (e.val == 4) || (e.val == 5)
 123  | CausalTetType.twoTwo, e =>
 124      (e.val == 1) || (e.val == 2) || (e.val == 3) || (e.val == 4)
 125
 126/-- THEOREM (by `decide`): for type (3,1), an edge is timelike iff its two
 127endpoints (via the repo edge convention `edgeVertices`) lie on different
 128slices.  This verifies the edge-type table against the slice structure. -/
 129theorem isTimelike_threeOne_eq_crossSlice :
 130    ∀ e : Fin 6,
 131      isTimelike CausalTetType.threeOne e
 132        = (sliceOf CausalTetType.threeOne (edgeVertices e).1
 133            != sliceOf CausalTetType.threeOne (edgeVertices e).2) := by
 134  decide
 135
 136/-- THEOREM (by `decide`): same cross-slice verification for type (2,2). -/
 137theorem isTimelike_twoTwo_eq_crossSlice :
 138    ∀ e : Fin 6,
 139      isTimelike CausalTetType.twoTwo e
 140        = (sliceOf CausalTetType.twoTwo (edgeVertices e).1
 141            != sliceOf CausalTetType.twoTwo (edgeVertices e).2) := by
 142  decide
 143
 144/-- THEOREM (by `decide`): type (3,1) has 3 vertices on slice `t` and 1 on
 145slice `t+1`. -/
 146theorem slice_count_threeOne :
 147    (Finset.univ.filter fun v : Fin 4 =>
 148        sliceOf CausalTetType.threeOne v = false).card = 3
 149      ∧ (Finset.univ.filter fun v : Fin 4 =>
 150        sliceOf CausalTetType.threeOne v = true).card = 1 := by
 151  decide
 152
 153/-- THEOREM (by `decide`): type (2,2) has 2 vertices on each slice. -/
 154theorem slice_count_twoTwo :
 155    (Finset.univ.filter fun v : Fin 4 =>
 156        sliceOf CausalTetType.twoTwo v = false).card = 2
 157      ∧ (Finset.univ.filter fun v : Fin 4 =>
 158        sliceOf CausalTetType.twoTwo v = true).card = 2 := by
 159  decide
 160
 161/-- THEOREM (by `decide`): type (3,1) has exactly 3 timelike edges. -/
 162theorem timelike_count_threeOne :
 163    (Finset.univ.filter fun e : Fin 6 =>
 164      isTimelike CausalTetType.threeOne e = true).card = 3 := by
 165  decide
 166
 167/-- THEOREM (by `decide`): type (3,1) has exactly 3 spacelike edges. -/
 168theorem spacelike_count_threeOne :
 169    (Finset.univ.filter fun e : Fin 6 =>
 170      isTimelike CausalTetType.threeOne e = false).card = 3 := by
 171  decide
 172
 173/-- THEOREM (by `decide`): type (2,2) has exactly 4 timelike edges. -/
 174theorem timelike_count_twoTwo :
 175    (Finset.univ.filter fun e : Fin 6 =>
 176      isTimelike CausalTetType.twoTwo e = true).card = 4 := by
 177  decide
 178
 179/-- THEOREM (by `decide`): type (2,2) has exactly 2 spacelike edges. -/
 180theorem spacelike_count_twoTwo :
 181    (Finset.univ.filter fun e : Fin 6 =>
 182      isTimelike CausalTetType.twoTwo e = false).card = 2 := by
 183  decide
 184
 185noncomputable section
 186
 187/-! ## §2. Lorentzian and Euclideanized squared-edge tuples
 188
 189MODEL: the standard CDT edge-length assignments. -/
 190
 191/-- Lorentzian squared-edge tuple: spacelike edges carry `a^2`, timelike
 192edges carry `-(alpha * a^2)`. -/
 193def lorentzianSqEdges (ty : CausalTetType) (a alpha : ℝ) : SqEdges :=
 194  fun e => if isTimelike ty e then -(alpha * a ^ 2) else a ^ 2
 195
 196/-- Euclideanized squared-edge tuple: spacelike edges carry `a^2`, timelike
 197edges carry `+alpha * a^2` (the image of the Lorentzian tuple under the Wick
 198map, equivalently the continuation `alpha ↦ -alpha`). -/
 199def euclideanSqEdges (ty : CausalTetType) (a alpha : ℝ) : SqEdges :=
 200  fun e => if isTimelike ty e then alpha * a ^ 2 else a ^ 2
 201
 202/-- The Lorentzian causal class: all Lorentzian tuples of the given type
 203with positive lattice spacing and positive asymmetry `alpha`. -/
 204def LorentzianClass (ty : CausalTetType) : Set SqEdges :=
 205  { x | ∃ a alpha : ℝ, 0 < a ∧ 0 < alpha ∧ x = lorentzianSqEdges ty a alpha }
 206
 207/-- THEOREM: all entries of the Euclideanized tuple are positive when
 208`0 < a` and `0 < alpha`. -/
 209theorem euclideanSqEdges_pos (ty : CausalTetType) (a alpha : ℝ)
 210    (ha : 0 < a) (halpha : 0 < alpha) (e : Fin 6) :
 211    0 < euclideanSqEdges ty a alpha e := by
 212  have h2 : 0 < a ^ 2 := pow_pos ha 2
 213  unfold euclideanSqEdges
 214  by_cases h : isTimelike ty e = true
 215  · rw [if_pos h]
 216    exact mul_pos halpha h2
 217  · rw [if_neg h]
 218    exact h2
 219
 220/-! ## §3. The Wick rotation as a map on squared edge lengths -/
 221
 222/-- The Wick map: flip the sign of every timelike squared edge length,
 223leave spacelike squared edge lengths unchanged. -/
 224def wick (ty : CausalTetType) (x : SqEdges) : SqEdges :=
 225  fun e => if isTimelike ty e then -(x e) else x e
 226
 227/-- THEOREM: the Wick map is an involution on all of `SqEdges` (hence in
 228particular on the causal class). -/
 229theorem wick_wick (ty : CausalTetType) (x : SqEdges) :
 230    wick ty (wick ty x) = x := by
 231  funext e
 232  by_cases h : isTimelike ty e = true
 233  · simp only [wick, if_pos h, neg_neg]
 234  · simp only [wick, if_neg h]
 235
 236/-- THEOREM: the Wick map is involutive (Mathlib `Function.Involutive`
 237packaging of `wick_wick`). -/
 238theorem wick_involutive (ty : CausalTetType) :
 239    Function.Involutive (wick ty) :=
 240  fun x => wick_wick ty x
 241
 242/-- THEOREM: on the causal class the Wick map produces exactly the
 243Euclideanized tuple. -/
 244theorem wick_lorentzian (ty : CausalTetType) (a alpha : ℝ) :
 245    wick ty (lorentzianSqEdges ty a alpha) = euclideanSqEdges ty a alpha := by
 246  funext e
 247  by_cases h : isTimelike ty e = true
 248  · simp only [wick, lorentzianSqEdges, euclideanSqEdges, if_pos h, neg_neg]
 249  · simp only [wick, lorentzianSqEdges, euclideanSqEdges, if_neg h]
 250
 251/-- THEOREM: the Euclideanized tuple is the honest algebraic continuation
 252`alpha ↦ -alpha` of the Lorentzian tuple. -/
 253theorem lorentzian_continuation (ty : CausalTetType) (a alpha : ℝ) :
 254    lorentzianSqEdges ty a (-alpha) = euclideanSqEdges ty a alpha := by
 255  funext e
 256  unfold lorentzianSqEdges euclideanSqEdges
 257  by_cases h : isTimelike ty e = true
 258  · rw [if_pos h, if_pos h]
 259    ring
 260  · rw [if_neg h, if_neg h]
 261
 262/-- THEOREM: combining the two, the Wick map acts on the causal class as
 263the continuation `alpha ↦ -alpha`. -/
 264theorem wick_eq_continuation (ty : CausalTetType) (a alpha : ℝ) :
 265    wick ty (lorentzianSqEdges ty a alpha) = lorentzianSqEdges ty a (-alpha) :=
 266  (wick_lorentzian ty a alpha).trans (lorentzian_continuation ty a alpha).symm
 267
 268/-- THEOREM: the Wick image of any member of the Lorentzian causal class is
 269an Euclideanized tuple with the same parameters. -/
 270theorem wick_image_euclidean (ty : CausalTetType) (x : SqEdges)
 271    (hx : x ∈ LorentzianClass ty) :
 272    ∃ a alpha : ℝ, 0 < a ∧ 0 < alpha ∧ wick ty x = euclideanSqEdges ty a alpha := by
 273  simp only [LorentzianClass, Set.mem_setOf_eq] at hx
 274  obtain ⟨a, alpha, ha, halpha, hxeq⟩ := hx
 275  exact ⟨a, alpha, ha, halpha, by rw [hxeq, wick_lorentzian]⟩
 276
 277/-! ## §4. Cayley-Menger determinants of the causal tuples
 278
 279The core computation.  `cm3` is the explicit degree-3 Cayley-Menger
 280polynomial from `Geometry.CayleyMengerPolynomial` with `cm3 = 288 V^2` on
 281realizable tetrahedra.  The repo already provides the uniform scaling law
 282`cm3_scaling : cm3 (fun e => s * x e) = s^3 * cm3 x`; we restate it for the
 283causal tuples (`cm3_euclidean_scale`) and also compute at general `a`
 284directly, so no generality is lost. -/
 285
 286/-- THEOREM: type (3,1) Euclideanized Cayley-Menger determinant,
 287`cm3 = 2 * (3*alpha - 1) * a^6`.  Hand derivation: base `{a0,a1,a3} = a^2`
 288(equilateral spacelike triangle), legs `{a2,a4,a5} = alpha * a^2`; the three
 289balanced terms each contribute `alpha*(1+alpha)*a^6`, the four monomial
 290terms contribute `(1 + 3*alpha^2)*a^6`, leaving `2*(3*alpha - 1)*a^6`. -/
 291theorem cm3_euclidean_threeOne (a alpha : ℝ) :
 292    cm3 (euclideanSqEdges CausalTetType.threeOne a alpha)
 293      = 2 * (3 * alpha - 1) * a ^ 6 := by
 294  have h0 : euclideanSqEdges CausalTetType.threeOne a alpha 0 = a ^ 2 := rfl
 295  have h1 : euclideanSqEdges CausalTetType.threeOne a alpha 1 = a ^ 2 := rfl
 296  have h2 : euclideanSqEdges CausalTetType.threeOne a alpha 2 = alpha * a ^ 2 := rfl
 297  have h3 : euclideanSqEdges CausalTetType.threeOne a alpha 3 = a ^ 2 := rfl
 298  have h4 : euclideanSqEdges CausalTetType.threeOne a alpha 4 = alpha * a ^ 2 := rfl
 299  have h5 : euclideanSqEdges CausalTetType.threeOne a alpha 5 = alpha * a ^ 2 := rfl
 300  unfold cm3
 301  rw [h0, h1, h2, h3, h4, h5]
 302  ring
 303
 304/-- THEOREM: type (2,2) Euclideanized Cayley-Menger determinant,
 305`cm3 = 4 * (2*alpha - 1) * a^6`.  Hand derivation: spacelike pair
 306`{a0,a5} = a^2` (an opposite-edge pair), cross edges
 307`{a1,a2,a3,a4} = alpha * a^2`; the first balanced term contributes
 308`(4*alpha - 2)*a^6`, the other two balanced terms give `2*alpha^2*a^6` each
 309and cancel exactly against the four monomial terms. -/
 310theorem cm3_euclidean_twoTwo (a alpha : ℝ) :
 311    cm3 (euclideanSqEdges CausalTetType.twoTwo a alpha)
 312      = 4 * (2 * alpha - 1) * a ^ 6 := by
 313  have h0 : euclideanSqEdges CausalTetType.twoTwo a alpha 0 = a ^ 2 := rfl
 314  have h1 : euclideanSqEdges CausalTetType.twoTwo a alpha 1 = alpha * a ^ 2 := rfl
 315  have h2 : euclideanSqEdges CausalTetType.twoTwo a alpha 2 = alpha * a ^ 2 := rfl
 316  have h3 : euclideanSqEdges CausalTetType.twoTwo a alpha 3 = alpha * a ^ 2 := rfl
 317  have h4 : euclideanSqEdges CausalTetType.twoTwo a alpha 4 = alpha * a ^ 2 := rfl
 318  have h5 : euclideanSqEdges CausalTetType.twoTwo a alpha 5 = a ^ 2 := rfl
 319  unfold cm3
 320  rw [h0, h1, h2, h3, h4, h5]
 321  ring
 322
 323/-- THEOREM: type (3,1) Lorentzian Cayley-Menger determinant,
 324`cm3 = -(2 * (3*alpha + 1) * a^6)`: strictly negative for `alpha ≥ 0`,
 325`a ≠ 0` (see `lorentzian_cm3_neg_threeOne`). -/
 326theorem cm3_lorentzian_threeOne (a alpha : ℝ) :
 327    cm3 (lorentzianSqEdges CausalTetType.threeOne a alpha)
 328      = -(2 * (3 * alpha + 1) * a ^ 6) := by
 329  have h0 : lorentzianSqEdges CausalTetType.threeOne a alpha 0 = a ^ 2 := rfl
 330  have h1 : lorentzianSqEdges CausalTetType.threeOne a alpha 1 = a ^ 2 := rfl
 331  have h2 : lorentzianSqEdges CausalTetType.threeOne a alpha 2
 332      = -(alpha * a ^ 2) := rfl
 333  have h3 : lorentzianSqEdges CausalTetType.threeOne a alpha 3 = a ^ 2 := rfl
 334  have h4 : lorentzianSqEdges CausalTetType.threeOne a alpha 4
 335      = -(alpha * a ^ 2) := rfl
 336  have h5 : lorentzianSqEdges CausalTetType.threeOne a alpha 5
 337      = -(alpha * a ^ 2) := rfl
 338  unfold cm3
 339  rw [h0, h1, h2, h3, h4, h5]
 340  ring
 341
 342/-- THEOREM: type (2,2) Lorentzian Cayley-Menger determinant,
 343`cm3 = -(4 * (2*alpha + 1) * a^6)`. -/
 344theorem cm3_lorentzian_twoTwo (a alpha : ℝ) :
 345    cm3 (lorentzianSqEdges CausalTetType.twoTwo a alpha)
 346      = -(4 * (2 * alpha + 1) * a ^ 6) := by
 347  have h0 : lorentzianSqEdges CausalTetType.twoTwo a alpha 0 = a ^ 2 := rfl
 348  have h1 : lorentzianSqEdges CausalTetType.twoTwo a alpha 1
 349      = -(alpha * a ^ 2) := rfl
 350  have h2 : lorentzianSqEdges CausalTetType.twoTwo a alpha 2
 351      = -(alpha * a ^ 2) := rfl
 352  have h3 : lorentzianSqEdges CausalTetType.twoTwo a alpha 3
 353      = -(alpha * a ^ 2) := rfl
 354  have h4 : lorentzianSqEdges CausalTetType.twoTwo a alpha 4
 355      = -(alpha * a ^ 2) := rfl
 356  have h5 : lorentzianSqEdges CausalTetType.twoTwo a alpha 5 = a ^ 2 := rfl
 357  unfold cm3
 358  rw [h0, h1, h2, h3, h4, h5]
 359  ring
 360
 361/-- THEOREM: the Euclideanized tuple at spacing `a` is the unit-spacing tuple
 362scaled by `a^2`. -/
 363theorem euclideanSqEdges_scale (ty : CausalTetType) (a alpha : ℝ) :
 364    euclideanSqEdges ty a alpha
 365      = fun e => a ^ 2 * euclideanSqEdges ty 1 alpha e := by
 366  funext e
 367  unfold euclideanSqEdges
 368  by_cases h : isTimelike ty e = true
 369  · rw [if_pos h, if_pos h]
 370    ring
 371  · rw [if_neg h, if_neg h]
 372    ring
 373
 374/-- THEOREM: `a^2` scales out of the causal Cayley-Menger determinant via
 375the repo scaling law `cm3_scaling` (which already existed; nothing new
 376needed). -/
 377theorem cm3_euclidean_scale (ty : CausalTetType) (a alpha : ℝ) :
 378    cm3 (euclideanSqEdges ty a alpha)
 379      = (a ^ 2) ^ 3 * cm3 (euclideanSqEdges ty 1 alpha) := by
 380  rw [euclideanSqEdges_scale ty a alpha]
 381  exact cm3_scaling (euclideanSqEdges ty 1 alpha) (a ^ 2)
 382
 383/-! ## §5. The exact non-degeneracy range (the core theorem) -/
 384
 385/-- The exact non-degeneracy threshold for each causal type:
 386`alphaMin threeOne = 1/3`, `alphaMin twoTwo = 1/2`. -/
 387def alphaMin : CausalTetType → ℝ
 388  | CausalTetType.threeOne => 1 / 3
 389  | CausalTetType.twoTwo => 1 / 2
 390
 391theorem alphaMin_threeOne : alphaMin CausalTetType.threeOne = 1 / 3 := rfl
 392
 393theorem alphaMin_twoTwo : alphaMin CausalTetType.twoTwo = 1 / 2 := rfl
 394
 395theorem alphaMin_pos (ty : CausalTetType) : 0 < alphaMin ty := by
 396  cases ty <;> norm_num [alphaMin]
 397
 398theorem alphaMin_lt_one (ty : CausalTetType) : alphaMin ty < 1 := by
 399  cases ty <;> norm_num [alphaMin]
 400
 401/-- THEOREM (core, exact range): for `0 < a`, the Euclideanized causal
 402tetrahedron is non-degenerate (`cm3 > 0`, equivalently positive squared
 403volume) if and only if `alpha > alphaMin ty`.  The threshold is exact in
 404both directions. -/
 405theorem cm3_euclidean_pos_iff (ty : CausalTetType) (a alpha : ℝ)
 406    (ha : 0 < a) :
 407    0 < cm3 (euclideanSqEdges ty a alpha) ↔ alphaMin ty < alpha := by
 408  have h6 : 0 < a ^ 6 := pow_pos ha 6
 409  cases ty
 410  · rw [cm3_euclidean_threeOne, alphaMin_threeOne]
 411    constructor
 412    · intro h
 413      by_contra hle
 414      push_neg at hle
 415      have hprod : 0 ≤ (1 - 3 * alpha) * a ^ 6 :=
 416        mul_nonneg (by linarith) h6.le
 417      linarith
 418    · intro h
 419      have hprod : 0 < (3 * alpha - 1) * a ^ 6 :=
 420        mul_pos (by linarith) h6
 421      linarith
 422  · rw [cm3_euclidean_twoTwo, alphaMin_twoTwo]
 423    constructor
 424    · intro h
 425      by_contra hle
 426      push_neg at hle
 427      have hprod : 0 ≤ (1 - 2 * alpha) * a ^ 6 :=
 428        mul_nonneg (by linarith) h6.le
 429      linarith
 430    · intro h
 431      have hprod : 0 < (2 * alpha - 1) * a ^ 6 :=
 432        mul_pos (by linarith) h6
 433      linarith
 434
 435/-- THEOREM: non-degeneracy on the derived range (forward direction of the
 436iff, stated for direct use). -/
 437theorem cm3_euclidean_pos (ty : CausalTetType) (a alpha : ℝ)
 438    (ha : 0 < a) (halpha : alphaMin ty < alpha) :
 439    0 < cm3 (euclideanSqEdges ty a alpha) :=
 440  (cm3_euclidean_pos_iff ty a alpha ha).mpr halpha
 441
 442/-- THEOREM: both causal types are simultaneously non-degenerate exactly on
 443`alpha > 1/2`, the standard 3d CDT Euclidean-regime bound. -/
 444theorem cm3_euclidean_pos_joint (a alpha : ℝ)
 445    (ha : 0 < a) (halpha : 1 / 2 < alpha) :
 446    0 < cm3 (euclideanSqEdges CausalTetType.threeOne a alpha)
 447      ∧ 0 < cm3 (euclideanSqEdges CausalTetType.twoTwo a alpha) :=
 448  ⟨cm3_euclidean_pos CausalTetType.threeOne a alpha ha
 449      (by rw [alphaMin_threeOne]; linarith),
 450    cm3_euclidean_pos CausalTetType.twoTwo a alpha ha
 451      (by rw [alphaMin_twoTwo]; linarith)⟩
 452
 453/-- THEOREM (threshold exactness): at `alpha = alphaMin ty` the Euclideanized
 454simplex is degenerate, `cm3 = 0`. -/
 455theorem cm3_euclidean_degenerate_at_min (ty : CausalTetType) (a : ℝ) :
 456    cm3 (euclideanSqEdges ty a (alphaMin ty)) = 0 := by
 457  cases ty
 458  · rw [alphaMin_threeOne, cm3_euclidean_threeOne]
 459    norm_num
 460  · rw [alphaMin_twoTwo, cm3_euclidean_twoTwo]
 461    norm_num
 462
 463/-- THEOREM: the Lorentzian (3,1) tuple always fails the Cayley-Menger
 464non-degeneracy criterion: `cm3 < 0` for all `alpha ≥ 0`, `0 < a`.  Formally
 465this is the cm3 sign fact; "not Euclidean-realizable" is the standard
 466reading via the classical Cayley-Menger realizability theorem (cm3 = 288 V²
 467on realizable tetrahedra), which is used as the interface convention of
 468`NonDegenerateTet`, not re-proved here.  The Wick rotation is genuinely
 469required to reach the Euclidean sector. -/
 470theorem lorentzian_cm3_neg_threeOne (a alpha : ℝ)
 471    (ha : 0 < a) (halpha : 0 ≤ alpha) :
 472    cm3 (lorentzianSqEdges CausalTetType.threeOne a alpha) < 0 := by
 473  rw [cm3_lorentzian_threeOne]
 474  have h6 : 0 < a ^ 6 := pow_pos ha 6
 475  have hprod : 0 < (3 * alpha + 1) * a ^ 6 := mul_pos (by linarith) h6
 476  linarith
 477
 478/-- THEOREM: same for the Lorentzian (2,2) tuple. -/
 479theorem lorentzian_cm3_neg_twoTwo (a alpha : ℝ)
 480    (ha : 0 < a) (halpha : 0 ≤ alpha) :
 481    cm3 (lorentzianSqEdges CausalTetType.twoTwo a alpha) < 0 := by
 482  rw [cm3_lorentzian_twoTwo]
 483  have h6 : 0 < a ^ 6 := pow_pos ha 6
 484  have hprod : 0 < (2 * alpha + 1) * a ^ 6 := mul_pos (by linarith) h6
 485  linarith
 486
 487/-! ## §6. `NonDegenerateTet` instances and the certified Wick composite -/
 488
 489/-- THEOREM (packaged): on the exact range `alpha > alphaMin ty` (with
 490`0 < a`), the Euclideanized causal tetrahedron is a `NonDegenerateTet` of
 491the existing Regge foundation: all squared edges positive and `cm3 > 0`. -/
 492def euclideanCausalTet (ty : CausalTetType) (a alpha : ℝ)
 493    (ha : 0 < a) (halpha : alphaMin ty < alpha) :
 494    NonDegenerateTet where
 495  sqEdge := euclideanSqEdges ty a alpha
 496  sqEdge_pos := fun e =>
 497    euclideanSqEdges_pos ty a alpha ha (lt_trans (alphaMin_pos ty) halpha) e
 498  cm_pos := cm3_euclidean_pos ty a alpha ha halpha
 499
 500/-- THEOREM (composite): the Wick image of the Lorentzian causal tuple is
 501non-degenerate on the exact range.  This is the certified kinematical Wick
 502rotation: Lorentzian class member in, `NonDegenerateTet`-certified Euclidean
 503tetrahedron out (realizability in the cm3-criterion sense above). -/
 504theorem wick_lorentzian_nondegenerate (ty : CausalTetType) (a alpha : ℝ)
 505    (ha : 0 < a) (halpha : alphaMin ty < alpha) :
 506    0 < cm3 (wick ty (lorentzianSqEdges ty a alpha)) := by
 507  rw [wick_lorentzian]
 508  exact cm3_euclidean_pos ty a alpha ha halpha
 509
 510/-- The physical-point (`a = 1`, `alpha = 1`) non-degenerate causal
 511tetrahedron, for either type. -/
 512def physicalCausalTet (ty : CausalTetType) : NonDegenerateTet :=
 513  euclideanCausalTet ty 1 1 one_pos (alphaMin_lt_one ty)
 514
 515/-! ## §7. Deficit-angle reality corollary at the physical point
 516
 517At `alpha = 1` (and unit spacing) both Euclideanized causal types coincide
 518with the regular unit tetrahedron, so the cofactor dihedral cosine is
 519exactly `1/3` at every edge and all dihedral angles are well-defined
 520(arccos arguments strictly inside `(-1,1)`), hence all deficit angles at
 521edges of the Euclideanized causal complex are real.  Downscope note (per
 522the lane ladder): the symbolic-alpha version of this corollary needs sign
 523control of the square-rooted degree-2 Cayley-Menger cofactor minors over the
 524whole range `alpha > alphaMin`; that fight is left OPEN and only the
 525concrete physical point is certified here.  The core non-degeneracy theorem
 526(§5) is symbolic in `alpha` for both types. -/
 527
 528/-- THEOREM: at `alpha = 1`, `a = 1`, both causal types Euclideanize to the
 529regular unit tetrahedron tuple. -/
 530theorem euclideanSqEdges_alpha_one (ty : CausalTetType) :
 531    euclideanSqEdges ty 1 1 = regularUnitSqEdges := by
 532  funext e
 533  simp only [euclideanSqEdges, regularUnitSqEdges]
 534  by_cases h : isTimelike ty e = true
 535  · rw [if_pos h]
 536    norm_num
 537  · rw [if_neg h]
 538    norm_num
 539
 540/-- THEOREM: at the physical point the cofactor dihedral cosine is `1/3` at
 541every edge (both causal types), via the proved regular-tetrahedron cofactor
 542evaluation. -/
 543theorem dihedralCos3Sq_alpha_one (ty : CausalTetType) (e : Fin 6) :
 544    dihedralCos3Sq (euclideanSqEdges ty 1 1) e = 1 / 3 := by
 545  rw [euclideanSqEdges_alpha_one ty]
 546  exact dihedralCos3_regularUnit e
 547
 548/-- THEOREM (deficit-angle reality, physical point): the arccos argument
 549lies strictly inside `(-1, 1)` at every edge, for both causal types. -/
 550theorem dihedralCos3Sq_alpha_one_mem_Ioo (ty : CausalTetType) (e : Fin 6) :
 551    -1 < dihedralCos3Sq (euclideanSqEdges ty 1 1) e
 552      ∧ dihedralCos3Sq (euclideanSqEdges ty 1 1) e < 1 := by
 553  rw [dihedralCos3Sq_alpha_one ty e]
 554  norm_num
 555
 556/-- THEOREM: the Euclidean dihedral angle at every edge of the physical-point
 557causal tetrahedron is `arccos (1/3)`, hence strictly inside `(0, π)`:
 558deficit angles at all edges are real and well-defined. -/
 559theorem dihedralAngle3_physical (ty : CausalTetType) (e : Fin 6) :
 560    dihedralAngle3 (physicalCausalTet ty) e = Real.arccos (1 / 3) :=
 561  congrArg Real.arccos (dihedralCos3Sq_alpha_one ty e)
 562
 563/-- THEOREM: the physical-point dihedral angle lies strictly inside
 564`(0, π)`. -/
 565theorem dihedralAngle3_physical_mem_Ioo (ty : CausalTetType) (e : Fin 6) :
 566    0 < dihedralAngle3 (physicalCausalTet ty) e
 567      ∧ dihedralAngle3 (physicalCausalTet ty) e < Real.pi := by
 568  rw [dihedralAngle3_physical ty e]
 569  have h := Geometry.DihedralAngle.regular_tet_dihedral_in_open_interval
 570  rw [Geometry.DihedralAngle.regular_tet_dihedral_theta] at h
 571  exact h
 572
 573/-! ## §8. Status certificate -/
 574
 575/-- Status flags for the Lorentzian sector gap.  This module certifies the
 576kinematical Wick rotation on the causal class: the causal tetrahedron
 577classes are defined and combinatorially verified, the Wick map is a proved
 578involution acting as `alpha ↦ -alpha` on the class, and the Euclideanized
 579simplices are proved non-degenerate on the exact ranges `alpha > 1/3`
 580(type (3,1)) and `alpha > 1/2` (type (2,2)).  The action-level continuation
 581(complex dihedral angles at timelike hinges, the sinh/boost sector of the
 582Lorentzian Regge action, and the analytic continuation of the action itself)
 583remains OPEN and is deliberately flagged as such below. -/
 584structure LorentzianSectorStatus where
 585  causal_class_defined : Bool
 586  wick_certified_on_class : Bool
 587  euclidean_nondegeneracy_proved : Bool
 588  lorentzian_action_continuation_open : Bool
 589
 590/-- The status of this module's deliverables. -/
 591def lorentzianSectorStatus : LorentzianSectorStatus where
 592  causal_class_defined := true
 593  wick_certified_on_class := true
 594  euclidean_nondegeneracy_proved := true
 595  lorentzian_action_continuation_open := true
 596
 597/-- THEOREM (by `rfl`): the status flags are forced. -/
 598theorem lorentzianSectorStatus_flags :
 599    lorentzianSectorStatus.causal_class_defined = true
 600      ∧ lorentzianSectorStatus.wick_certified_on_class = true
 601      ∧ lorentzianSectorStatus.euclidean_nondegeneracy_proved = true
 602      ∧ lorentzianSectorStatus.lorentzian_action_continuation_open = true :=
 603  ⟨rfl, rfl, rfl, rfl⟩
 604
 605end
 606
 607end CausalSimplexWick
 608end SevenGaps
 609end Gravity
 610end IndisputableMonolith
 611