IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Data.Matrix.Basic
   3import Mathlib.Algebra.BigOperators.Fin
   4import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
   5import Mathlib.Tactic.Linarith
   6import Mathlib.Tactic.Push
   7import IndisputableMonolith.Geometry.CayleyMengerN
   8
   9/-!
  10# Causal (CDT) 4-Simplex Classes and the Kinematical Wick Rotation (4D)
  11
  12QG Seven-Gaps campaign, Lorentzian-sector lane, Phase 3a: the 4D Lorentzian
  13lift of the kernel-checked 3D causal-simplex machinery in
  14`Gravity.SevenGaps.CausalSimplexWick` (conventions mirrored in prose; this
  15module is import-independent of it).  This module builds:
  16
  171. the causal (CDT-style) 4-simplex classes in D = 4, with the
  18   spacelike/timelike edge-type assignment verified combinatorially from the
  19   slice structure (decide-able lemmas);
  202. the Wick rotation as an explicit map on the ten squared edge lengths,
  21   proved to be an involution and proved to act on the causal class as the
  22   algebraic continuation `alpha ↦ -alpha`;
  233. the 4-simplex Cayley-Menger determinant `cm4`, grounded in the existing
  24   dimension-parametric `Geometry.CayleyMengerN.cmDetN` (the bordered 6x6
  25   determinant), evaluated exactly on both causal classes;
  264. the exact Euclidean non-degeneracy thresholds in `alpha` for both types
  27   (in the cm4-positivity criterion), with degeneracy exactly at threshold
  28   and strict cm4 negativity on the Lorentzian side.
  29
  30## Conventions (4D CDT, Ambjorn-Jurkiewicz-Loll)
  31
  32Spatial slices are 3D triangulated manifolds of equilateral tetrahedra with
  33squared edge length `a^2`.  Spacetime between slices `t` and `t+1` is filled
  34by two 4-simplex types:
  35
  36* type (4,1): four vertices on slice `t`, one on slice `t+1`
  37  (6 spacelike + 4 timelike edges); the time-reflected type (1,4) has the
  38  same edge-length multiset and is covered by the same theorems;
  39* type (3,2): three vertices on slice `t`, two on slice `t+1`
  40  (3 + 1 = 4 spacelike + 6 timelike edges); the reflection (2,3) likewise.
  41
  42Spacelike edges carry squared length `a^2`; timelike edges carry squared
  43length `-alpha * a^2` in the Lorentzian regime, `alpha > 0`.  The Wick
  44rotation flips the sign of the timelike squared lengths, i.e. it is the
  45continuation `alpha ↦ -alpha` on the causal class.
  46
  47Vertex/edge indexing: vertices `0,1,2,3,4`; the ten edges are ordered
  48lexicographically,
  49
  50  edge 0 = (0,1), edge 1 = (0,2), edge 2 = (0,3), edge 3 = (0,4),
  51  edge 4 = (1,2), edge 5 = (1,3), edge 6 = (1,4),
  52  edge 7 = (2,3), edge 8 = (2,4), edge 9 = (3,4).
  53
  54Slice assignment: for (4,1) vertices `{0,1,2,3}` lie on slice `t` and `4` on
  55slice `t+1` (timelike edges `{3,6,8,9}`); for (3,2) vertices `{0,1,2}` lie
  56on slice `t` and `{3,4}` on slice `t+1` (timelike edges `{2,3,5,6,7,8}`,
  57spacelike edges `{0,1,4,9}`).
  58
  59## Derived thresholds (symbolic determinant evaluation, certified below)
  60
  61`cm4 x := -(cmDetN of the bordered 6x6 CM matrix)`, normalized so that
  62`simplexVolumeSqN = cm4 / 9216` identically (proved below); on genuinely
  63embeddable 4-simplices this formal expression is the classical `V^2`.
  64Sanity anchor: regular unit 4-simplex `cm4 = 5` (classically
  65V = sqrt 5 / 96, so 9216 V^2 = 5).
  66
  67Evaluated on the Euclideanized causal tuples:
  68
  69* type (4,1): `cm4 = (8*alpha - 3) * a^8`, hence non-degenerate exactly for
  70  `alpha > 3/8` (`alphaMin fourOne = 3/8`); cross-check: the AJL volume
  71  `V(4,1) = (a^4/96) * sqrt (8*alpha - 3)` gives `9216 V^2 = (8*alpha-3) a^8`;
  72* type (3,2): `cm4 = (12*alpha - 7) * a^8`, hence non-degenerate exactly for
  73  `alpha > 7/12` (`alphaMin threeTwo = 7/12`); cross-check:
  74  `V(3,2) = (a^4/96) * sqrt (12*alpha - 7)` gives `9216 V^2 = (12*alpha-7) a^8`.
  75
  76Both types are simultaneously non-degenerate exactly for `alpha > 7/12`, the
  77standard 4d CDT Euclidean-regime bound.  Degeneracy at threshold is proved
  78(`cm4 = 0` at `alpha = alphaMin`), so the range is exact.  On the Lorentzian
  79side `cm4 = -(8*alpha + 3) * a^8` (type (4,1)) and `-(12*alpha + 7) * a^8`
  80(type (3,2)): strictly negative for all `alpha >= 0`.  What is proved is the
  81cm4 sign fact; the classical equivalence "cm4 > 0 iff embeddable in R^4"
  82(which upgrades cm4 negativity to non-realizability) is NOT formalized in
  83this repo for n = 4 (the 3D case has `Geometry/TetrahedronRealization.lean`;
  84no 4D analog exists yet).  Under that classical reading the Lorentzian
  85tuples are never Euclidean-realizable and the Wick rotation is genuinely
  86required.  At the physical point `alpha = 1` both types reduce to the
  87regular 4-simplex tuple, `cm4 = 5 * a^8`.
  88
  89## Honesty tiers
  90
  91* THEOREM: every declared theorem in this file is proved with zero sorry,
  92  zero admit, zero new axioms; hypotheses are explicit (`0 < a`,
  93  `alphaMin ty < alpha`, etc.).  Exception: `causalSimplex4DStatus_flags`
  94  is a documentation record of hand-set booleans, not a mathematical
  95  theorem; it is not counted in this tier.
  96* MODEL: `CausalPentType`, `sliceOf`, `isTimelike`, `lorentzianSqEdges`,
  97  `euclideanSqEdges`, `wick`, `alphaMin`, `NonDegeneratePent` are
  98  definitional encodings of the standard 4d CDT conventions.  "cm4 > 0" is
  99  used throughout as the non-degeneracy criterion; its classical
 100  equivalence to embeddability in R^4 is not formalized here.
 101* OPEN: (a) the 4D Cayley-Menger realizability theorem (cm4 > 0 iff
 102  embeddable in R^4; 3D analog in `Geometry/TetrahedronRealization.lean`);
 103  (b) the action-level Lorentzian continuation in 4D (complex dihedral
 104  angles at timelike triangular hinges, the boost/sinh sector of the 4d
 105  Regge action, and the continuation of the action itself), which is wave
 106  3b and is deliberately not attempted here; see `CausalSimplex4DStatus`.
 107
 108## decide usage (all on finite Bool-valued data, none on `ℝ`)
 109
 110`isTimelike_fourOne_eq_crossSlice`, `isTimelike_threeTwo_eq_crossSlice`,
 111`slice_count_fourOne`, `slice_count_threeTwo`, `timelike_count_fourOne`,
 112`spacelike_count_fourOne`, `timelike_count_threeTwo`,
 113`spacelike_count_threeTwo`.  No `native_decide` anywhere.
 114-/
 115
 116namespace IndisputableMonolith
 117namespace Gravity
 118namespace SevenGaps
 119namespace CausalSimplex4D
 120
 121open Geometry.CayleyMengerN
 122
 123/-! ## §1. The causal 4-simplex classes (combinatorial layer)
 124
 125MODEL: the two 4d CDT 4-simplex types and their slice structure. -/
 126
 127/-- The two causal 4-simplex types of 4d CDT between adjacent slices.
 128`fourOne` has four vertices on slice `t` and one on slice `t+1` (its time
 129reflection (1,4) has the same edge data); `threeTwo` has three vertices on
 130slice `t` and two on slice `t+1` (reflection (2,3) likewise). -/
 131inductive CausalPentType
 132  | fourOne
 133  | threeTwo
 134
 135/-- Squared edge lengths of a 4-simplex, indexed by `Fin 10`
 136(lexicographic edge order, see module docstring). -/
 137abbrev SqEdges10 : Type := Fin 10 → ℝ
 138
 139/-- Edge index → vertex pair for the 4-simplex on vertices `Fin 5`:
 140edges `(0,1),(0,2),(0,3),(0,4),(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)` in
 141lexicographic order. -/
 142def pentEdgeVertices : Fin 10 → Fin 5 × Fin 5
 143  | 0 => (0, 1)
 144  | 1 => (0, 2)
 145  | 2 => (0, 3)
 146  | 3 => (0, 4)
 147  | 4 => (1, 2)
 148  | 5 => (1, 3)
 149  | 6 => (1, 4)
 150  | 7 => (2, 3)
 151  | 8 => (2, 4)
 152  | 9 => (3, 4)
 153
 154/-- Slice membership of each vertex (`false` = slice `t`, `true` = slice
 155`t+1`).  For (4,1): vertices `0,1,2,3` on slice `t`, vertex `4` on `t+1`.
 156For (3,2): vertices `0,1,2` on slice `t`, vertices `3,4` on `t+1`. -/
 157def sliceOf : CausalPentType → Fin 5 → Bool
 158  | CausalPentType.fourOne, v => v.val == 4
 159  | CausalPentType.threeTwo, v => (v.val == 3) || (v.val == 4)
 160
 161/-- Edge-type assignment: `true` iff the edge is timelike (connects the two
 162slices).  For (4,1) the timelike edges are `{3,6,8,9}` (those touching the
 163apex vertex 4); for (3,2) they are `{2,3,5,6,7,8}` (the six cross edges). -/
 164def isTimelike : CausalPentType → Fin 10 → Bool
 165  | CausalPentType.fourOne, e =>
 166      (e.val == 3) || (e.val == 6) || (e.val == 8) || (e.val == 9)
 167  | CausalPentType.threeTwo, e =>
 168      (e.val == 2) || (e.val == 3) || (e.val == 5)
 169        || (e.val == 6) || (e.val == 7) || (e.val == 8)
 170
 171/-- THEOREM (by `decide`): for type (4,1), an edge is timelike iff its two
 172endpoints (via `pentEdgeVertices`) lie on different slices.  This verifies
 173the edge-type table against the slice structure. -/
 174theorem isTimelike_fourOne_eq_crossSlice :
 175    ∀ e : Fin 10,
 176      isTimelike CausalPentType.fourOne e
 177        = (sliceOf CausalPentType.fourOne (pentEdgeVertices e).1
 178            != sliceOf CausalPentType.fourOne (pentEdgeVertices e).2) := by
 179  decide
 180
 181/-- THEOREM (by `decide`): same cross-slice verification for type (3,2). -/
 182theorem isTimelike_threeTwo_eq_crossSlice :
 183    ∀ e : Fin 10,
 184      isTimelike CausalPentType.threeTwo e
 185        = (sliceOf CausalPentType.threeTwo (pentEdgeVertices e).1
 186            != sliceOf CausalPentType.threeTwo (pentEdgeVertices e).2) := by
 187  decide
 188
 189/-- THEOREM (by `decide`): type (4,1) has 4 vertices on slice `t` and 1 on
 190slice `t+1`. -/
 191theorem slice_count_fourOne :
 192    (Finset.univ.filter fun v : Fin 5 =>
 193        sliceOf CausalPentType.fourOne v = false).card = 4
 194      ∧ (Finset.univ.filter fun v : Fin 5 =>
 195        sliceOf CausalPentType.fourOne v = true).card = 1 := by
 196  decide
 197
 198/-- THEOREM (by `decide`): type (3,2) has 3 vertices on slice `t` and 2 on
 199slice `t+1`. -/
 200theorem slice_count_threeTwo :
 201    (Finset.univ.filter fun v : Fin 5 =>
 202        sliceOf CausalPentType.threeTwo v = false).card = 3
 203      ∧ (Finset.univ.filter fun v : Fin 5 =>
 204        sliceOf CausalPentType.threeTwo v = true).card = 2 := by
 205  decide
 206
 207/-- THEOREM (by `decide`): type (4,1) has exactly 4 timelike edges. -/
 208theorem timelike_count_fourOne :
 209    (Finset.univ.filter fun e : Fin 10 =>
 210      isTimelike CausalPentType.fourOne e = true).card = 4 := by
 211  decide
 212
 213/-- THEOREM (by `decide`): type (4,1) has exactly 6 spacelike edges. -/
 214theorem spacelike_count_fourOne :
 215    (Finset.univ.filter fun e : Fin 10 =>
 216      isTimelike CausalPentType.fourOne e = false).card = 6 := by
 217  decide
 218
 219/-- THEOREM (by `decide`): type (3,2) has exactly 6 timelike edges. -/
 220theorem timelike_count_threeTwo :
 221    (Finset.univ.filter fun e : Fin 10 =>
 222      isTimelike CausalPentType.threeTwo e = true).card = 6 := by
 223  decide
 224
 225/-- THEOREM (by `decide`): type (3,2) has exactly 4 spacelike edges
 226(3 within the lower slice triangle plus 1 within the upper slice pair). -/
 227theorem spacelike_count_threeTwo :
 228    (Finset.univ.filter fun e : Fin 10 =>
 229      isTimelike CausalPentType.threeTwo e = false).card = 4 := by
 230  decide
 231
 232noncomputable section
 233
 234/-! ## §2. Lorentzian and Euclideanized squared-edge tuples
 235
 236MODEL: the standard 4d CDT edge-length assignments. -/
 237
 238/-- Lorentzian squared-edge tuple: spacelike edges carry `a^2`, timelike
 239edges carry `-(alpha * a^2)`. -/
 240def lorentzianSqEdges (ty : CausalPentType) (a alpha : ℝ) : SqEdges10 :=
 241  fun e => if isTimelike ty e then -(alpha * a ^ 2) else a ^ 2
 242
 243/-- Euclideanized squared-edge tuple: spacelike edges carry `a^2`, timelike
 244edges carry `+alpha * a^2` (the image of the Lorentzian tuple under the Wick
 245map, equivalently the continuation `alpha ↦ -alpha`). -/
 246def euclideanSqEdges (ty : CausalPentType) (a alpha : ℝ) : SqEdges10 :=
 247  fun e => if isTimelike ty e then alpha * a ^ 2 else a ^ 2
 248
 249/-- The Lorentzian causal class: all Lorentzian tuples of the given type
 250with positive lattice spacing and positive asymmetry `alpha`. -/
 251def LorentzianClass (ty : CausalPentType) : Set SqEdges10 :=
 252  { x | ∃ a alpha : ℝ, 0 < a ∧ 0 < alpha ∧ x = lorentzianSqEdges ty a alpha }
 253
 254/-- THEOREM: all entries of the Euclideanized tuple are positive when
 255`0 < a` and `0 < alpha`. -/
 256theorem euclideanSqEdges_pos (ty : CausalPentType) (a alpha : ℝ)
 257    (ha : 0 < a) (halpha : 0 < alpha) (e : Fin 10) :
 258    0 < euclideanSqEdges ty a alpha e := by
 259  have h2 : 0 < a ^ 2 := pow_pos ha 2
 260  unfold euclideanSqEdges
 261  by_cases h : isTimelike ty e = true
 262  · rw [if_pos h]
 263    exact mul_pos halpha h2
 264  · rw [if_neg h]
 265    exact h2
 266
 267/-- THEOREM: the Euclideanized tuple at spacing `a` is the unit-spacing
 268tuple scaled by `a^2`. -/
 269theorem euclideanSqEdges_scale (ty : CausalPentType) (a alpha : ℝ) :
 270    euclideanSqEdges ty a alpha
 271      = fun e => a ^ 2 * euclideanSqEdges ty 1 alpha e := by
 272  funext e
 273  unfold euclideanSqEdges
 274  by_cases h : isTimelike ty e = true
 275  · rw [if_pos h, if_pos h]
 276    ring
 277  · rw [if_neg h, if_neg h]
 278    ring
 279
 280/-! ## §3. The Wick rotation as a map on squared edge lengths -/
 281
 282/-- The Wick map: flip the sign of every timelike squared edge length,
 283leave spacelike squared edge lengths unchanged. -/
 284def wick (ty : CausalPentType) (x : SqEdges10) : SqEdges10 :=
 285  fun e => if isTimelike ty e then -(x e) else x e
 286
 287/-- THEOREM: the Wick map is an involution on all of `SqEdges10` (hence in
 288particular on the causal class). -/
 289theorem wick_wick (ty : CausalPentType) (x : SqEdges10) :
 290    wick ty (wick ty x) = x := by
 291  funext e
 292  by_cases h : isTimelike ty e = true
 293  · simp only [wick, if_pos h, neg_neg]
 294  · simp only [wick, if_neg h]
 295
 296/-- THEOREM: the Wick map is involutive (Mathlib `Function.Involutive`
 297packaging of `wick_wick`). -/
 298theorem wick_involutive (ty : CausalPentType) :
 299    Function.Involutive (wick ty) :=
 300  fun x => wick_wick ty x
 301
 302/-- THEOREM: on the causal class the Wick map produces exactly the
 303Euclideanized tuple. -/
 304theorem wick_lorentzian (ty : CausalPentType) (a alpha : ℝ) :
 305    wick ty (lorentzianSqEdges ty a alpha) = euclideanSqEdges ty a alpha := by
 306  funext e
 307  by_cases h : isTimelike ty e = true
 308  · simp only [wick, lorentzianSqEdges, euclideanSqEdges, if_pos h, neg_neg]
 309  · simp only [wick, lorentzianSqEdges, euclideanSqEdges, if_neg h]
 310
 311/-- THEOREM: the Euclideanized tuple is the honest algebraic continuation
 312`alpha ↦ -alpha` of the Lorentzian tuple. -/
 313theorem lorentzian_continuation (ty : CausalPentType) (a alpha : ℝ) :
 314    lorentzianSqEdges ty a (-alpha) = euclideanSqEdges ty a alpha := by
 315  funext e
 316  unfold lorentzianSqEdges euclideanSqEdges
 317  by_cases h : isTimelike ty e = true
 318  · rw [if_pos h, if_pos h]
 319    ring
 320  · rw [if_neg h, if_neg h]
 321
 322/-- THEOREM: combining the two, the Wick map acts on the causal class as
 323the continuation `alpha ↦ -alpha`. -/
 324theorem wick_eq_continuation (ty : CausalPentType) (a alpha : ℝ) :
 325    wick ty (lorentzianSqEdges ty a alpha) = lorentzianSqEdges ty a (-alpha) :=
 326  (wick_lorentzian ty a alpha).trans (lorentzian_continuation ty a alpha).symm
 327
 328/-- THEOREM: the Wick image of any member of the Lorentzian causal class is
 329an Euclideanized tuple for some admissible parameters (`0 < a`,
 330`0 < alpha`), namely the witnessing parameters of the class membership. -/
 331theorem wick_image_euclidean (ty : CausalPentType) (x : SqEdges10)
 332    (hx : x ∈ LorentzianClass ty) :
 333    ∃ a alpha : ℝ, 0 < a ∧ 0 < alpha
 334      ∧ wick ty x = euclideanSqEdges ty a alpha := by
 335  simp only [LorentzianClass, Set.mem_setOf_eq] at hx
 336  obtain ⟨a, alpha, ha, halpha, hxeq⟩ := hx
 337  exact ⟨a, alpha, ha, halpha, by rw [hxeq, wick_lorentzian]⟩
 338
 339/-! ## §4. The 4-simplex Cayley-Menger determinant `cm4`
 340
 341`cm4` is grounded in the existing dimension-parametric machinery
 342`Geometry.CayleyMengerN`: the edge tuple is packaged as
 343`SimplexSquaredDistances 4`, and `cm4 := -(cmDetN)` so that `cm4 > 0` on
 344non-degenerate Euclidean 4-simplices (`cm4 = 9216 V^2`, i.e.
 345`simplexVolumeSqN = cm4 / 9216`, proved below). -/
 346
 347/-- Squared-distance table of the 4-simplex from the `Fin 10` edge tuple
 348(lexicographic edge order). -/
 349def pentDistSq (x : SqEdges10) : Fin 5 → Fin 5 → ℝ := fun i j =>
 350  match i.val, j.val with
 351  | 0, 1 => x 0
 352  | 1, 0 => x 0
 353  | 0, 2 => x 1
 354  | 2, 0 => x 1
 355  | 0, 3 => x 2
 356  | 3, 0 => x 2
 357  | 0, 4 => x 3
 358  | 4, 0 => x 3
 359  | 1, 2 => x 4
 360  | 2, 1 => x 4
 361  | 1, 3 => x 5
 362  | 3, 1 => x 5
 363  | 1, 4 => x 6
 364  | 4, 1 => x 6
 365  | 2, 3 => x 7
 366  | 3, 2 => x 7
 367  | 2, 4 => x 8
 368  | 4, 2 => x 8
 369  | 3, 4 => x 9
 370  | 4, 3 => x 9
 371  | _, _ => 0
 372
 373/-- THEOREM: the distance table returns the edge tuple on every edge (the
 374table and the lexicographic edge indexing agree). -/
 375theorem pentDistSq_edge (x : SqEdges10) (e : Fin 10) :
 376    pentDistSq x (pentEdgeVertices e).1 (pentEdgeVertices e).2 = x e := by
 377  fin_cases e <;> rfl
 378
 379/-- The `SimplexSquaredDistances 4` package of an edge tuple. -/
 380def pentDistances (x : SqEdges10) : SimplexSquaredDistances 4 where
 381  distSq := pentDistSq x
 382  symm := by
 383    intro i j
 384    fin_cases i <;> fin_cases j <;> rfl
 385  diag_zero := by
 386    intro i
 387    fin_cases i <;> rfl
 388
 389/-- The 4-simplex Cayley-Menger determinant, sign-normalized so that
 390`cm4 > 0` on non-degenerate Euclidean 4-simplices (`cm4 = 9216 V^2`). -/
 391def cm4 (x : SqEdges10) : ℝ :=
 392  -(cmDetN (pentDistances x))
 393
 394/-- THEOREM: the formal squared 4-volume of the repo's n-dimensional layer
 395is exactly `cm4 / 9216` (`9216 = 2^4 * (4!)^2`), fixing the sign and
 396normalization of `cm4` against `Geometry.CayleyMengerN`. -/
 397theorem simplexVolumeSqN_eq_cm4_div (x : SqEdges10) :
 398    simplexVolumeSqN (pentDistances x) = cm4 x / 9216 := by
 399  unfold simplexVolumeSqN cm4
 400  have h : ((Nat.factorial 4 : ℕ) : ℝ) = 24 := by
 401    norm_num [Nat.factorial]
 402  rw [h]
 403  ring
 404
 405/-! ### The two-parameter causal matrices
 406
 407On a causal tuple all ten edges take one of two values (`p` spacelike,
 408`q` timelike), so the bordered 6x6 CM matrix collapses to an explicit
 409two-parameter matrix per type.  The determinant of each is computed
 410symbolically once, and every causal evaluation follows by substitution. -/
 411
 412/-- The bordered CM matrix of a (4,1) tuple with spacelike value `p` and
 413timelike value `q` (matrix rows/cols `1..5` are vertices `0..4`; the apex
 414vertex 4 is row/col 5). -/
 415def pentMatrix41 (p q : ℝ) : Matrix (Fin 6) (Fin 6) ℝ :=
 416  fun i j =>
 417    match i.val, j.val with
 418    | 0, 0 => 0
 419    | 0, _ => 1
 420    | _, 0 => 1
 421    | 1, 1 => 0
 422    | 2, 2 => 0
 423    | 3, 3 => 0
 424    | 4, 4 => 0
 425    | 5, 5 => 0
 426    | 1, 5 => q
 427    | 5, 1 => q
 428    | 2, 5 => q
 429    | 5, 2 => q
 430    | 3, 5 => q
 431    | 5, 3 => q
 432    | 4, 5 => q
 433    | 5, 4 => q
 434    | _, _ => p
 435
 436/-- The bordered CM matrix of a (3,2) tuple with spacelike value `p` and
 437timelike value `q` (rows/cols `1,2,3` are the lower-slice vertices `0,1,2`;
 438rows/cols `4,5` are the upper-slice vertices `3,4`). -/
 439def pentMatrix32 (p q : ℝ) : Matrix (Fin 6) (Fin 6) ℝ :=
 440  fun i j =>
 441    match i.val, j.val with
 442    | 0, 0 => 0
 443    | 0, _ => 1
 444    | _, 0 => 1
 445    | 1, 1 => 0
 446    | 2, 2 => 0
 447    | 3, 3 => 0
 448    | 4, 4 => 0
 449    | 5, 5 => 0
 450    | 1, 2 => p
 451    | 2, 1 => p
 452    | 1, 3 => p
 453    | 3, 1 => p
 454    | 2, 3 => p
 455    | 3, 2 => p
 456    | 4, 5 => p
 457    | 5, 4 => p
 458    | _, _ => q
 459
 460set_option maxHeartbeats 8000000 in
 461set_option maxRecDepth 16384 in
 462/-- THEOREM (symbolic 6x6 determinant): the (4,1) causal CM determinant is
 463`p^3 * (3*p - 8*q)`.  Kernel-honest expansion of the bordered 6x6
 464determinant. -/
 465theorem det_pentMatrix41 (p q : ℝ) :
 466    Matrix.det (pentMatrix41 p q) = p ^ 3 * (3 * p - 8 * q) := by
 467  unfold pentMatrix41
 468  -- Style note: bare `simp` retained deliberately.  A `simp only` variant
 469  -- with an explicit lemma list was attempted and hit a deterministic
 470  -- whnf timeout even at 8M heartbeats (the default simp set's numeric
 471  -- simprocs are needed to keep the 6x6 expansion tractable).
 472  simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
 473  ring
 474
 475set_option maxHeartbeats 8000000 in
 476set_option maxRecDepth 16384 in
 477/-- THEOREM (symbolic 6x6 determinant): the (3,2) causal CM determinant is
 478`p^3 * (7*p - 12*q)`. -/
 479theorem det_pentMatrix32 (p q : ℝ) :
 480    Matrix.det (pentMatrix32 p q) = p ^ 3 * (7 * p - 12 * q) := by
 481  unfold pentMatrix32
 482  -- Style note: bare `simp` retained deliberately; see det_pentMatrix41.
 483  simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
 484  ring
 485
 486/-- THEOREM: the bordered CM matrix of the Euclideanized (4,1) tuple is the
 487two-parameter matrix at `p = a^2`, `q = alpha * a^2`. -/
 488theorem cmMatrixN_euclidean_fourOne (a alpha : ℝ) :
 489    cmMatrixN (pentDistances (euclideanSqEdges CausalPentType.fourOne a alpha))
 490      = pentMatrix41 (a ^ 2) (alpha * a ^ 2) := by
 491  ext i j
 492  fin_cases i <;> fin_cases j <;> rfl
 493
 494/-- THEOREM: the bordered CM matrix of the Lorentzian (4,1) tuple is the
 495two-parameter matrix at `p = a^2`, `q = -(alpha * a^2)`. -/
 496theorem cmMatrixN_lorentzian_fourOne (a alpha : ℝ) :
 497    cmMatrixN (pentDistances (lorentzianSqEdges CausalPentType.fourOne a alpha))
 498      = pentMatrix41 (a ^ 2) (-(alpha * a ^ 2)) := by
 499  ext i j
 500  fin_cases i <;> fin_cases j <;> rfl
 501
 502/-- THEOREM: the bordered CM matrix of the Euclideanized (3,2) tuple is the
 503two-parameter matrix at `p = a^2`, `q = alpha * a^2`. -/
 504theorem cmMatrixN_euclidean_threeTwo (a alpha : ℝ) :
 505    cmMatrixN (pentDistances (euclideanSqEdges CausalPentType.threeTwo a alpha))
 506      = pentMatrix32 (a ^ 2) (alpha * a ^ 2) := by
 507  ext i j
 508  fin_cases i <;> fin_cases j <;> rfl
 509
 510/-- THEOREM: the bordered CM matrix of the Lorentzian (3,2) tuple is the
 511two-parameter matrix at `p = a^2`, `q = -(alpha * a^2)`. -/
 512theorem cmMatrixN_lorentzian_threeTwo (a alpha : ℝ) :
 513    cmMatrixN (pentDistances (lorentzianSqEdges CausalPentType.threeTwo a alpha))
 514      = pentMatrix32 (a ^ 2) (-(alpha * a ^ 2)) := by
 515  ext i j
 516  fin_cases i <;> fin_cases j <;> rfl
 517
 518/-- THEOREM: type (4,1) Euclideanized Cayley-Menger determinant,
 519`cm4 = (8*alpha - 3) * a^8`.  Cross-check: the AJL volume
 520`V(4,1) = (a^4/96) * sqrt (8*alpha - 3)` gives
 521`9216 V^2 = (8*alpha - 3) * a^8`. -/
 522theorem cm4_euclidean_fourOne (a alpha : ℝ) :
 523    cm4 (euclideanSqEdges CausalPentType.fourOne a alpha)
 524      = (8 * alpha - 3) * a ^ 8 := by
 525  unfold cm4 cmDetN
 526  rw [cmMatrixN_euclidean_fourOne, det_pentMatrix41]
 527  ring
 528
 529/-- THEOREM: type (3,2) Euclideanized Cayley-Menger determinant,
 530`cm4 = (12*alpha - 7) * a^8`.  Cross-check: the AJL volume
 531`V(3,2) = (a^4/96) * sqrt (12*alpha - 7)` gives
 532`9216 V^2 = (12*alpha - 7) * a^8`. -/
 533theorem cm4_euclidean_threeTwo (a alpha : ℝ) :
 534    cm4 (euclideanSqEdges CausalPentType.threeTwo a alpha)
 535      = (12 * alpha - 7) * a ^ 8 := by
 536  unfold cm4 cmDetN
 537  rw [cmMatrixN_euclidean_threeTwo, det_pentMatrix32]
 538  ring
 539
 540/-- THEOREM: type (4,1) Lorentzian Cayley-Menger determinant,
 541`cm4 = -((8*alpha + 3) * a^8)`: strictly negative for `alpha ≥ 0`, `0 < a`
 542(see `lorentzian_cm4_neg_fourOne`). -/
 543theorem cm4_lorentzian_fourOne (a alpha : ℝ) :
 544    cm4 (lorentzianSqEdges CausalPentType.fourOne a alpha)
 545      = -((8 * alpha + 3) * a ^ 8) := by
 546  unfold cm4 cmDetN
 547  rw [cmMatrixN_lorentzian_fourOne, det_pentMatrix41]
 548  ring
 549
 550/-- THEOREM: type (3,2) Lorentzian Cayley-Menger determinant,
 551`cm4 = -((12*alpha + 7) * a^8)`. -/
 552theorem cm4_lorentzian_threeTwo (a alpha : ℝ) :
 553    cm4 (lorentzianSqEdges CausalPentType.threeTwo a alpha)
 554      = -((12 * alpha + 7) * a ^ 8) := by
 555  unfold cm4 cmDetN
 556  rw [cmMatrixN_lorentzian_threeTwo, det_pentMatrix32]
 557  ring
 558
 559/-- THEOREM: `a^2` scales out of the causal Cayley-Menger determinant with
 560weight `(a^2)^4 = a^8`, stated via the two exact evaluations.  The bordered
 561CM determinant of a 4-simplex is homogeneous of degree 4 in the squared
 562distances (the 4D analog of `cm3_scaling` with exponent 3 in 3D). -/
 563theorem cm4_euclidean_scale (ty : CausalPentType) (a alpha : ℝ) :
 564    cm4 (euclideanSqEdges ty a alpha)
 565      = (a ^ 2) ^ 4 * cm4 (euclideanSqEdges ty 1 alpha) := by
 566  cases ty
 567  · rw [cm4_euclidean_fourOne, cm4_euclidean_fourOne]
 568    ring
 569  · rw [cm4_euclidean_threeTwo, cm4_euclidean_threeTwo]
 570    ring
 571
 572/-- THEOREM: at `alpha = 1`, `a = 1`, both causal types Euclideanize to the
 573regular unit 4-simplex tuple (all squared lengths 1). -/
 574theorem euclideanSqEdges_alpha_one (ty : CausalPentType) :
 575    euclideanSqEdges ty 1 1 = fun _ => (1 : ℝ) := by
 576  funext e
 577  unfold euclideanSqEdges
 578  by_cases h : isTimelike ty e = true
 579  · rw [if_pos h]
 580    norm_num
 581  · rw [if_neg h]
 582    norm_num
 583
 584/-- THEOREM (sanity anchor): the regular unit 4-simplex has `cm4 = 5`
 585(classical: `V = sqrt 5 / 96`, so `9216 V^2 = 5`). -/
 586theorem cm4_regular_unit : cm4 (fun _ => (1 : ℝ)) = 5 := by
 587  rw [← euclideanSqEdges_alpha_one CausalPentType.fourOne,
 588    cm4_euclidean_fourOne]
 589  norm_num
 590
 591/-! ## §5. The exact non-degeneracy range (the core theorem) -/
 592
 593/-- The exact non-degeneracy threshold for each causal type:
 594`alphaMin fourOne = 3/8`, `alphaMin threeTwo = 7/12`. -/
 595def alphaMin : CausalPentType → ℝ
 596  | CausalPentType.fourOne => 3 / 8
 597  | CausalPentType.threeTwo => 7 / 12
 598
 599theorem alphaMin_fourOne : alphaMin CausalPentType.fourOne = 3 / 8 := rfl
 600
 601theorem alphaMin_threeTwo : alphaMin CausalPentType.threeTwo = 7 / 12 := rfl
 602
 603theorem alphaMin_pos (ty : CausalPentType) : 0 < alphaMin ty := by
 604  cases ty <;> norm_num [alphaMin]
 605
 606theorem alphaMin_lt_one (ty : CausalPentType) : alphaMin ty < 1 := by
 607  cases ty <;> norm_num [alphaMin]
 608
 609/-- THEOREM (core, exact range): for `0 < a`, the Euclideanized causal
 6104-simplex satisfies the CM positivity criterion `cm4 > 0` if and only if
 611`alpha > alphaMin ty`.  The threshold is exact in both directions.
 612Reading note: `cm4 > 0` is `9216 * simplexVolumeSqN > 0` (proved above);
 613its classical equivalence to embeddability in R^4 is not formalized in
 614this repo for n = 4 (3D analog: `Geometry/TetrahedronRealization.lean`). -/
 615theorem cm4_euclidean_pos_iff (ty : CausalPentType) (a alpha : ℝ)
 616    (ha : 0 < a) :
 617    0 < cm4 (euclideanSqEdges ty a alpha) ↔ alphaMin ty < alpha := by
 618  have h8 : 0 < a ^ 8 := pow_pos ha 8
 619  cases ty
 620  · rw [cm4_euclidean_fourOne, alphaMin_fourOne]
 621    constructor
 622    · intro h
 623      by_contra hle
 624      push_neg at hle
 625      have hprod : 0 ≤ (3 - 8 * alpha) * a ^ 8 :=
 626        mul_nonneg (by linarith) h8.le
 627      linarith
 628    · intro h
 629      have hprod : 0 < (8 * alpha - 3) * a ^ 8 :=
 630        mul_pos (by linarith) h8
 631      linarith
 632  · rw [cm4_euclidean_threeTwo, alphaMin_threeTwo]
 633    constructor
 634    · intro h
 635      by_contra hle
 636      push_neg at hle
 637      have hprod : 0 ≤ (7 - 12 * alpha) * a ^ 8 :=
 638        mul_nonneg (by linarith) h8.le
 639      linarith
 640    · intro h
 641      have hprod : 0 < (12 * alpha - 7) * a ^ 8 :=
 642        mul_pos (by linarith) h8
 643      linarith
 644
 645/-- THEOREM: non-degeneracy on the derived range (forward direction of the
 646iff, stated for direct use). -/
 647theorem cm4_euclidean_pos (ty : CausalPentType) (a alpha : ℝ)
 648    (ha : 0 < a) (halpha : alphaMin ty < alpha) :
 649    0 < cm4 (euclideanSqEdges ty a alpha) :=
 650  (cm4_euclidean_pos_iff ty a alpha ha).mpr halpha
 651
 652/-- THEOREM: both causal types are simultaneously non-degenerate exactly on
 653`alpha > 7/12`, the standard 4d CDT Euclidean-regime bound. -/
 654theorem cm4_euclidean_pos_joint (a alpha : ℝ)
 655    (ha : 0 < a) (halpha : 7 / 12 < alpha) :
 656    0 < cm4 (euclideanSqEdges CausalPentType.fourOne a alpha)
 657      ∧ 0 < cm4 (euclideanSqEdges CausalPentType.threeTwo a alpha) :=
 658  ⟨cm4_euclidean_pos CausalPentType.fourOne a alpha ha
 659      (by rw [alphaMin_fourOne]; linarith),
 660    cm4_euclidean_pos CausalPentType.threeTwo a alpha ha
 661      (by rw [alphaMin_threeTwo]; linarith)⟩
 662
 663/-- THEOREM (threshold exactness): at `alpha = alphaMin ty` the
 664Euclideanized 4-simplex is degenerate, `cm4 = 0`. -/
 665theorem cm4_euclidean_degenerate_at_min (ty : CausalPentType) (a : ℝ) :
 666    cm4 (euclideanSqEdges ty a (alphaMin ty)) = 0 := by
 667  cases ty
 668  · rw [alphaMin_fourOne, cm4_euclidean_fourOne]
 669    norm_num
 670  · rw [alphaMin_threeTwo, cm4_euclidean_threeTwo]
 671    norm_num
 672
 673/-- THEOREM: the Lorentzian (4,1) tuple always fails the Cayley-Menger
 674positivity criterion: `cm4 < 0` for all `alpha ≥ 0`, `0 < a`.  What is
 675proved here is exactly this sign fact.  Upgrading it to "not
 676Euclidean-realizable" needs the classical Cayley-Menger realizability
 677theorem (`cm4 > 0` iff embeddable in R^4), which is not formalized in this
 678repo for n = 4 (3D analog: `Geometry/TetrahedronRealization.lean`).  Under
 679that classical reading the Wick rotation is genuinely required to reach the
 680Euclidean sector. -/
 681theorem lorentzian_cm4_neg_fourOne (a alpha : ℝ)
 682    (ha : 0 < a) (halpha : 0 ≤ alpha) :
 683    cm4 (lorentzianSqEdges CausalPentType.fourOne a alpha) < 0 := by
 684  rw [cm4_lorentzian_fourOne]
 685  have h8 : 0 < a ^ 8 := pow_pos ha 8
 686  have hprod : 0 < (8 * alpha + 3) * a ^ 8 := mul_pos (by linarith) h8
 687  linarith
 688
 689/-- THEOREM: same for the Lorentzian (3,2) tuple. -/
 690theorem lorentzian_cm4_neg_threeTwo (a alpha : ℝ)
 691    (ha : 0 < a) (halpha : 0 ≤ alpha) :
 692    cm4 (lorentzianSqEdges CausalPentType.threeTwo a alpha) < 0 := by
 693  rw [cm4_lorentzian_threeTwo]
 694  have h8 : 0 < a ^ 8 := pow_pos ha 8
 695  have hprod : 0 < (12 * alpha + 7) * a ^ 8 := mul_pos (by linarith) h8
 696  linarith
 697
 698/-! ## §6. `NonDegeneratePent` packaging and the certified Wick composite -/
 699
 700/-- A non-degenerate Euclidean 4-simplex in the cm4 criterion: all squared
 701edges positive and `cm4 > 0` (the 4D analogue of the Regge foundation's
 702`NonDegenerateTet`). -/
 703structure NonDegeneratePent where
 704  sqEdge : SqEdges10
 705  sqEdge_pos : ∀ e, 0 < sqEdge e
 706  cm_pos : 0 < cm4 sqEdge
 707
 708/-- def (packaged witness): on the exact range `alpha > alphaMin ty` (with
 709`0 < a`), the Euclideanized causal 4-simplex packages into a
 710`NonDegeneratePent`: all squared edges positive and `cm4 > 0`.  The
 711mathematical content lives in the two proof fields
 712(`euclideanSqEdges_pos`, `cm4_euclidean_pos`). -/
 713def euclideanCausalPent (ty : CausalPentType) (a alpha : ℝ)
 714    (ha : 0 < a) (halpha : alphaMin ty < alpha) :
 715    NonDegeneratePent where
 716  sqEdge := euclideanSqEdges ty a alpha
 717  sqEdge_pos := fun e =>
 718    euclideanSqEdges_pos ty a alpha ha (lt_trans (alphaMin_pos ty) halpha) e
 719  cm_pos := cm4_euclidean_pos ty a alpha ha halpha
 720
 721/-- THEOREM (composite): the Wick image of the Lorentzian causal tuple
 722satisfies `cm4 > 0` on the exact range.  This is the certified 4D
 723kinematical Wick rotation at the cm4-criterion level: Lorentzian class
 724member in, `cm4 > 0` out (non-degeneracy in the CM positivity sense; the
 725embeddability upgrade is classical and not formalized here). -/
 726theorem wick_lorentzian_nondegenerate (ty : CausalPentType) (a alpha : ℝ)
 727    (ha : 0 < a) (halpha : alphaMin ty < alpha) :
 728    0 < cm4 (wick ty (lorentzianSqEdges ty a alpha)) := by
 729  rw [wick_lorentzian]
 730  exact cm4_euclidean_pos ty a alpha ha halpha
 731
 732/-- def (packaged witness): the physical-point (`a = 1`, `alpha = 1`)
 733non-degenerate causal 4-simplex, for either type. -/
 734def physicalCausalPent (ty : CausalPentType) : NonDegeneratePent :=
 735  euclideanCausalPent ty 1 1 one_pos (alphaMin_lt_one ty)
 736
 737/-! ## §7. Status certificate -/
 738
 739/-- Status flags for the 4D Lorentzian lift.  This module certifies the 4D
 740kinematical layer: the causal 4-simplex classes are defined and
 741combinatorially verified, the exact cm4 thresholds `alpha > 3/8` (type
 742(4,1)) and `alpha > 7/12` (type (3,2)) are proved with degeneracy exactly
 743at threshold, and the Lorentzian tuples are proved to have `cm4 < 0`
 744(strict CM negativity; the embeddability upgrade to non-realizability is
 745classical and not formalized here).  The action-level continuation (complex
 746dihedral angles at timelike triangular hinges, the boost/sinh sector of the
 7474d Regge action) is wave 3b and remains OPEN, deliberately flagged below. -/
 748structure CausalSimplex4DStatus where
 749  four_d_classes_defined : Bool
 750  cm4_thresholds_certified : Bool
 751  lorentzian_cm4_negativity_proved : Bool
 752  action_level_continuation_open : Bool
 753
 754/-- The status of this module's deliverables. -/
 755def causalSimplex4DStatus : CausalSimplex4DStatus where
 756  four_d_classes_defined := true
 757  cm4_thresholds_certified := true
 758  lorentzian_cm4_negativity_proved := true
 759  action_level_continuation_open := true
 760
 761/-- Documentation record (by `rfl`): the flag values as set above.  The
 762mathematics lives in the theorems above, not in these booleans; nothing
 763forces hand-set flags.  Not counted in the THEOREM honesty tier. -/
 764theorem causalSimplex4DStatus_flags :
 765    causalSimplex4DStatus.four_d_classes_defined = true
 766      ∧ causalSimplex4DStatus.cm4_thresholds_certified = true
 767      ∧ causalSimplex4DStatus.lorentzian_cm4_negativity_proved = true
 768      ∧ causalSimplex4DStatus.action_level_continuation_open = true :=
 769  ⟨rfl, rfl, rfl, rfl⟩
 770
 771/-! ## §8. Axiom audit
 772
 773`#print axioms` receipts for the four load-bearing determinant results.
 774Expected output for each: `[propext, Classical.choice, Quot.sound]`
 775(the standard Mathlib trio; no `sorryAx`, no `Lean.ofReduceBool` from
 776`native_decide`, no repo-local axioms).  The output appears as `info`
 777lines in the build log. -/
 778
 779#print axioms det_pentMatrix41
 780#print axioms det_pentMatrix32
 781#print axioms cm4_euclidean_fourOne
 782#print axioms cm4_euclidean_threeTwo
 783
 784end
 785
 786end CausalSimplex4D
 787end SevenGaps
 788end Gravity
 789end IndisputableMonolith
 790