IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency

   1import IndisputableMonolith.Gravity.SevenGaps.ThreePentInteriorHingeWitness
   2import IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D
   3
   4/-!
   5# Three-Pent Causal Consistency: an explicit admissible causal edge-length
   6# assignment on the minimal interior-hinge complex (gap6-a, W3-2)
   7
   8QG full-theory campaign, Wave 3 lane W3-2.  `ThreePentInteriorHingeWitness`
   9proved the minimal genuine interior hinge exists COMBINATORIALLY and its
  10honest-scope clause named exactly what was missing: consistent causal edge
  11lengths around the cycle.  This module supplies them.
  12
  13## The assignment (MODEL data, one global function)
  14
  15Slice structure on the six vertices: the hinge triangle `{0,1,2}` lies on
  16slice `t` (`slice6 = false`), the three link vertices `{3,4,5}` on slice
  17`t+1` (`slice6 = true`).  ONE global squared-length function on vertex
  18pairs (`causalSqLength`): same-slice pairs carry `a^2` (spacelike),
  19cross-slice pairs carry `-(alpha * a^2)` (timelike).  Because every pent
  20pulls its edge tuple back from this single function, cycle consistency is
  21structural: adjacent pents agree on shared faces by construction
  22(`shared_face_consistency` states it as a kernel theorem).
  23
  24## What is proved (THEOREM)
  25
  26* `induced_pentA_eq` / `induced_pentB_eq` / `induced_pentC_eq` — the
  27  heart: each of the three pents, enumerated by its order-preserving
  28  vertex chart, pulls the global assignment back to EXACTLY the standard
  29  CDT Lorentzian (3,2) tuple `lorentzianSqEdges threeTwo a alpha` of the
  30  kernel-checked `CausalSimplex4D` layer.  The three-pent complex is
  31  literally three standard causal (3,2) pents glued around the hinge.
  32* `pent_charts_cover` / `pent_charts_injective` /
  33  `pent_slices_match` — the charts enumerate the witness module's own
  34  pents (`decide`), injectively, and carry slice `t`/`t+1` exactly onto
  35  the (3,2) slice structure of `CausalSimplex4D.sliceOf`.
  36* `threePent_lorentzian_class` — each induced tuple is a member of the
  37  Lorentzian causal class (`LorentzianClass threeTwo`).
  38* `threePent_lorentzian_cm4_neg` — per-pent Lorentzian Cayley-Menger
  39  certificate: `cm4 = -((12*alpha + 7) * a^8) < 0` on every pent
  40  (`0 < a`, `0 ≤ alpha`).
  41* `threePent_euclidean_admissible` — per-pent Euclidean admissibility
  42  after Wick: `cm4 (wick threeTwo ·) > 0` for every pent on the EXACT
  43  CDT range `alpha > 7/12` (`alphaMin threeTwo`); thresholds inherited
  44  exact from `CausalSimplex4D`.
  45* `hinge_edges_spacelike` / `link_edges_spacelike` /
  46  `cross_edges_timelike` — causal-type certificates: the hinge triangle
  47  and the link cycle `3-4-5-3` are spacelike, all nine hinge-to-link
  48  edges timelike.
  49* `physical_point_regular` — non-vacuity anchor: at `a = 1`, `alpha = 1`
  50  every pent Wick-rotates to the regular unit 4-simplex, `cm4 = 5`.
  51* `threePent_causal_assignment` — the packaged headline: on `0 < a`,
  52  `7/12 < alpha`, the explicit assignment simultaneously presents all
  53  three pents as admissible causal (3,2) simplices.
  54
  55## Consequence for the campaign (existence-only; critic-tightened scope)
  56
  57Gap6-a in its EXISTENTIAL reading is CLOSED POSITIVE: an admissible
  58causal edge-length assignment on the minimal interior-hinge complex
  59EXISTS explicitly, so the certified-NON-EXISTENCE branch of the W3-2
  60lane (which would have stopped gap6-b) does not fire.  What is realized
  61is THE symmetric standard CDT slab assignment (lengths depend only on
  62same-slice vs cross-slice); the classification of ASYMMETRIC assignments
  63around the hinge cycle, and any monodromy obstruction theory for
  64non-standard per-pent data, are NOT addressed and remain open questions
  65outside this lane's contract.  The action-level continuation lane
  66(gap6-b, W4-3 `WickActionInteriorHinge`) now has a concrete causal
  67object to attack: three (3,2) pents whose hinge data continuation
  68certificates are already landed per pent (`WickThreeTwoHinges`, B2).
  69This module does NOT do gap6-b and does NOT touch any
  70`FullTheoryLedger` flag; `gap6_lorentzian_action` stays `false`.
  71
  72## Inherited disclosure (binding, from `CausalSimplex4D`)
  73
  74"Admissible" is the Cayley-Menger positivity criterion `cm4 > 0` after
  75Wick (equivalently `9216 * V^2 > 0`), the exact 4d CDT regime.  The
  76classical equivalence "cm4 > 0 iff embeddable in R^4" is NOT formalized
  77in this repo for n = 4; under that classical reading the Euclideanized
  78pents are genuine nondegenerate 4-simplices.  The dihedral ANGLE VALUES
  79around the hinge (needed for the deficit) are gap6-b's business, not
  80claimed here.
  81
  82No `sorry`, no `admit`, no new axioms, no `native_decide` (`decide`
  83only, on finite Bool/Finset data), no `: True` or `Nonempty`-only
  84headline.  Expected axiom footprint of every theorem: the standard trio
  85`[propext, Classical.choice, Quot.sound]`.  Receipts at end of file.
  86-/
  87
  88namespace IndisputableMonolith
  89namespace Gravity
  90namespace SevenGaps
  91namespace ThreePentCausalConsistency
  92
  93open CausalSimplex4D
  94
  95noncomputable section
  96
  97/-! ## §1. The global causal assignment (MODEL) -/
  98
  99/-- Slice membership of the six vertices: hinge `{0,1,2}` on slice `t`
 100(`false`), link vertices `{3,4,5}` on slice `t+1` (`true`). -/
 101def slice6 : Fin 6 → Bool
 102  | 0 => false | 1 => false | 2 => false
 103  | 3 => true | 4 => true | 5 => true
 104
 105/-- THE global causal squared-length assignment on vertex pairs:
 106same-slice pairs are spacelike (`a^2`), cross-slice pairs timelike
 107(`-(alpha * a^2)`).  Every pent pulls its edge tuple back from this ONE
 108function, so shared faces agree by construction. -/
 109def causalSqLength (a alpha : ℝ) (u v : Fin 6) : ℝ :=
 110  if slice6 u != slice6 v then -(alpha * a ^ 2) else a ^ 2
 111
 112/-- The assignment is symmetric in its vertex pair. -/
 113theorem causalSqLength_symm (a alpha : ℝ) (u v : Fin 6) :
 114    causalSqLength a alpha u v = causalSqLength a alpha v u := by
 115  unfold causalSqLength
 116  cases hu : slice6 u <;> cases hv : slice6 v <;> simp
 117
 118/-! ## §2. The three pent charts and their incidence certificates -/
 119
 120/-- Vertex chart of pent `A = {0,1,2,3,4}` (order-preserving). -/
 121def pentAVert : Fin 5 → Fin 6
 122  | 0 => 0 | 1 => 1 | 2 => 2 | 3 => 3 | 4 => 4
 123
 124/-- Vertex chart of pent `B = {0,1,2,4,5}` (order-preserving). -/
 125def pentBVert : Fin 5 → Fin 6
 126  | 0 => 0 | 1 => 1 | 2 => 2 | 3 => 4 | 4 => 5
 127
 128/-- Vertex chart of pent `C = {0,1,2,3,5}` (order-preserving). -/
 129def pentCVert : Fin 5 → Fin 6
 130  | 0 => 0 | 1 => 1 | 2 => 2 | 3 => 3 | 4 => 5
 131
 132/-- THEOREM (by `decide`): the three charts enumerate exactly the witness
 133module's pents. -/
 134theorem pent_charts_cover :
 135    Finset.univ.image pentAVert = ThreePentInteriorHingeWitness.pentA
 136      ∧ Finset.univ.image pentBVert = ThreePentInteriorHingeWitness.pentB
 137      ∧ Finset.univ.image pentCVert = ThreePentInteriorHingeWitness.pentC := by
 138  decide
 139
 140/-- THEOREM (by `decide`): each chart is injective (five distinct
 141vertices; genuine 4-simplices). -/
 142theorem pent_charts_injective :
 143    Function.Injective pentAVert ∧ Function.Injective pentBVert
 144      ∧ Function.Injective pentCVert := by
 145  decide
 146
 147/-- THEOREM (by `decide`): every chart carries the global slice structure
 148exactly onto the (3,2) slice structure of the causal 4-simplex layer —
 149each pent has its `{0,1,2}` face on slice `t` and its residual pair on
 150slice `t+1`, which is the (3,2) causal type. -/
 151theorem pent_slices_match :
 152    (∀ v : Fin 5, slice6 (pentAVert v) = sliceOf CausalPentType.threeTwo v)
 153      ∧ (∀ v : Fin 5,
 154        slice6 (pentBVert v) = sliceOf CausalPentType.threeTwo v)
 155      ∧ (∀ v : Fin 5,
 156        slice6 (pentCVert v) = sliceOf CausalPentType.threeTwo v) := by
 157  decide
 158
 159/-! ## §3. The induced edge tuples ARE the standard causal (3,2) tuples -/
 160
 161/-- The squared-edge tuple a pent chart pulls back from the global
 162assignment. -/
 163def inducedSqEdges (verts : Fin 5 → Fin 6) (a alpha : ℝ) :
 164    SqEdges10 :=
 165  fun e =>
 166    causalSqLength a alpha (verts (pentEdgeVertices e).1)
 167      (verts (pentEdgeVertices e).2)
 168
 169/-- Shared-face consistency, structurally: whenever two charts send edge
 170indices to the same global vertex pair (in either order), the induced
 171squared lengths agree.  This is the "consistent around the cycle"
 172statement: there is one global length per edge of the complex, full
 173stop. -/
 174theorem shared_face_consistency (a alpha : ℝ) (P Q : Fin 5 → Fin 6)
 175    (e e' : Fin 10)
 176    (h : (P (pentEdgeVertices e).1 = Q (pentEdgeVertices e').1
 177          ∧ P (pentEdgeVertices e).2 = Q (pentEdgeVertices e').2)
 178        ∨ (P (pentEdgeVertices e).1 = Q (pentEdgeVertices e').2
 179          ∧ P (pentEdgeVertices e).2 = Q (pentEdgeVertices e').1)) :
 180    inducedSqEdges P a alpha e = inducedSqEdges Q a alpha e' := by
 181  unfold inducedSqEdges
 182  rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩
 183  · rw [h1, h2]
 184  · rw [h1, h2, causalSqLength_symm]
 185
 186/-- **THEOREM (consistency core, pent A): the induced tuple of pent A is
 187EXACTLY the standard CDT Lorentzian (3,2) tuple.** -/
 188theorem induced_pentA_eq (a alpha : ℝ) :
 189    inducedSqEdges pentAVert a alpha =
 190      lorentzianSqEdges CausalPentType.threeTwo a alpha := by
 191  funext e
 192  fin_cases e <;> rfl
 193
 194/-- **THEOREM (consistency core, pent B).** -/
 195theorem induced_pentB_eq (a alpha : ℝ) :
 196    inducedSqEdges pentBVert a alpha =
 197      lorentzianSqEdges CausalPentType.threeTwo a alpha := by
 198  funext e
 199  fin_cases e <;> rfl
 200
 201/-- **THEOREM (consistency core, pent C).** -/
 202theorem induced_pentC_eq (a alpha : ℝ) :
 203    inducedSqEdges pentCVert a alpha =
 204      lorentzianSqEdges CausalPentType.threeTwo a alpha := by
 205  funext e
 206  fin_cases e <;> rfl
 207
 208/-! ## §4. Per-pent certificates (Lorentzian class, Cayley-Menger, Wick) -/
 209
 210/-- THEOREM: each induced tuple is a member of the Lorentzian causal
 211class of type (3,2). -/
 212theorem threePent_lorentzian_class (a alpha : ℝ) (ha : 0 < a)
 213    (halpha : 0 < alpha) :
 214    inducedSqEdges pentAVert a alpha ∈ LorentzianClass CausalPentType.threeTwo
 215      ∧ inducedSqEdges pentBVert a alpha
 216          ∈ LorentzianClass CausalPentType.threeTwo
 217      ∧ inducedSqEdges pentCVert a alpha
 218          ∈ LorentzianClass CausalPentType.threeTwo :=
 219  ⟨⟨a, alpha, ha, halpha, induced_pentA_eq a alpha⟩,
 220    ⟨a, alpha, ha, halpha, induced_pentB_eq a alpha⟩,
 221    ⟨a, alpha, ha, halpha, induced_pentC_eq a alpha⟩⟩
 222
 223/-- THEOREM (per-pent Lorentzian Cayley-Menger certificate): every pent
 224of the complex has `cm4 = -((12*alpha + 7) * a^8) < 0` — the strict CM
 225negativity of a genuine Lorentzian (3,2) simplex. -/
 226theorem threePent_lorentzian_cm4_neg (a alpha : ℝ) (ha : 0 < a)
 227    (halpha : 0 ≤ alpha) :
 228    cm4 (inducedSqEdges pentAVert a alpha) < 0
 229      ∧ cm4 (inducedSqEdges pentBVert a alpha) < 0
 230      ∧ cm4 (inducedSqEdges pentCVert a alpha) < 0 := by
 231  rw [induced_pentA_eq, induced_pentB_eq, induced_pentC_eq]
 232  have h := lorentzian_cm4_neg_threeTwo a alpha ha halpha
 233  exact ⟨h, h, h⟩
 234
 235/-- THEOREM (per-pent Euclidean admissibility): on the EXACT 4d CDT
 236range `alpha > 7/12` (with `0 < a`), the Wick image of every pent
 237satisfies the Cayley-Menger positivity criterion `cm4 > 0` — all three
 238pents Euclideanize to nondegenerate 4-simplices simultaneously. -/
 239theorem threePent_euclidean_admissible (a alpha : ℝ) (ha : 0 < a)
 240    (halpha : 7 / 12 < alpha) :
 241    0 < cm4 (wick CausalPentType.threeTwo (inducedSqEdges pentAVert a alpha))
 242      ∧ 0 < cm4 (wick CausalPentType.threeTwo
 243          (inducedSqEdges pentBVert a alpha))
 244      ∧ 0 < cm4 (wick CausalPentType.threeTwo
 245          (inducedSqEdges pentCVert a alpha)) := by
 246  rw [induced_pentA_eq, induced_pentB_eq, induced_pentC_eq]
 247  have h := wick_lorentzian_nondegenerate CausalPentType.threeTwo a alpha ha
 248    (by rw [alphaMin_threeTwo]; exact halpha)
 249  exact ⟨h, h, h⟩
 250
 251/-! ## §5. Causal-type certificates on the complex -/
 252
 253/-- THEOREM: the three hinge edges `{0,1}, {0,2}, {1,2}` are spacelike
 254(squared length `a^2`). -/
 255theorem hinge_edges_spacelike (a alpha : ℝ) :
 256    causalSqLength a alpha 0 1 = a ^ 2
 257      ∧ causalSqLength a alpha 0 2 = a ^ 2
 258      ∧ causalSqLength a alpha 1 2 = a ^ 2 :=
 259  ⟨rfl, rfl, rfl⟩
 260
 261/-- THEOREM: the three link-cycle edges `{3,4}, {4,5}, {3,5}` (one per
 262pent: the residual pair) are spacelike (squared length `a^2`) — the
 263hinge link `3-4-5-3` is a spacelike cycle on slice `t+1`. -/
 264theorem link_edges_spacelike (a alpha : ℝ) :
 265    causalSqLength a alpha 3 4 = a ^ 2
 266      ∧ causalSqLength a alpha 4 5 = a ^ 2
 267      ∧ causalSqLength a alpha 3 5 = a ^ 2 :=
 268  ⟨rfl, rfl, rfl⟩
 269
 270/-- THEOREM: all nine hinge-to-link edges are timelike (squared length
 271`-(alpha * a^2)`). -/
 272theorem cross_edges_timelike (a alpha : ℝ) :
 273    ∀ u v : Fin 6, u ∈ GluedPentsHingeWitness.hinge →
 274      v ∈ ThreePentInteriorHingeWitness.linkVerts →
 275      causalSqLength a alpha u v = -(alpha * a ^ 2) := by
 276  intro u v hu hv
 277  fin_cases u <;> fin_cases v <;>
 278    first
 279      | rfl
 280      | exact absurd hu (by decide)
 281      | exact absurd hv (by decide)
 282
 283/-! ## §6. Physical-point anchor and the packaged headline -/
 284
 285/-- THEOREM (non-vacuity anchor): at the physical point `a = 1`,
 286`alpha = 1`, every pent of the complex Wick-rotates to the regular unit
 2874-simplex, `cm4 = 5`. -/
 288theorem physical_point_regular :
 289    wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)
 290        = (fun _ => (1 : ℝ))
 291      ∧ cm4 (wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)) = 5
 292      ∧ wick CausalPentType.threeTwo (inducedSqEdges pentBVert 1 1)
 293          = (fun _ => (1 : ℝ))
 294      ∧ wick CausalPentType.threeTwo (inducedSqEdges pentCVert 1 1)
 295          = (fun _ => (1 : ℝ)) := by
 296  have hA : wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)
 297      = (fun _ => (1 : ℝ)) := by
 298    rw [induced_pentA_eq, wick_lorentzian,
 299      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
 300  have hB : wick CausalPentType.threeTwo (inducedSqEdges pentBVert 1 1)
 301      = (fun _ => (1 : ℝ)) := by
 302    rw [induced_pentB_eq, wick_lorentzian,
 303      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
 304  have hC : wick CausalPentType.threeTwo (inducedSqEdges pentCVert 1 1)
 305      = (fun _ => (1 : ℝ)) := by
 306    rw [induced_pentC_eq, wick_lorentzian,
 307      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
 308  exact ⟨hA, by rw [hA]; exact cm4_regular_unit, hB, hC⟩
 309
 310/-- **GAP6-A HEADLINE (THEOREM): an explicit admissible causal
 311edge-length assignment on the minimal three-pent interior-hinge complex
 312EXISTS.**  On the exact 4d CDT range (`0 < a`, `alpha > 7/12`), the ONE
 313global assignment `causalSqLength` presents all three pents
 314simultaneously as standard Lorentzian (3,2) simplices (consistency
 315core), members of the Lorentzian causal class, with strict Lorentzian
 316CM negativity and Euclidean CM admissibility after Wick, per pent.
 317EXISTENCE-ONLY SCOPE: this realizes the symmetric standard CDT slab
 318assignment; it does not classify asymmetric assignments or hinge-cycle
 319monodromy.  The certified-non-existence branch of the W3-2 lane does
 320not fire; gap6-b may proceed against this concrete object. -/
 321theorem threePent_causal_assignment (a alpha : ℝ) (ha : 0 < a)
 322    (halpha : 7 / 12 < alpha) :
 323    (inducedSqEdges pentAVert a alpha
 324          = lorentzianSqEdges CausalPentType.threeTwo a alpha
 325        ∧ inducedSqEdges pentBVert a alpha
 326          = lorentzianSqEdges CausalPentType.threeTwo a alpha
 327        ∧ inducedSqEdges pentCVert a alpha
 328          = lorentzianSqEdges CausalPentType.threeTwo a alpha)
 329      ∧ (inducedSqEdges pentAVert a alpha
 330            ∈ LorentzianClass CausalPentType.threeTwo
 331        ∧ inducedSqEdges pentBVert a alpha
 332            ∈ LorentzianClass CausalPentType.threeTwo
 333        ∧ inducedSqEdges pentCVert a alpha
 334            ∈ LorentzianClass CausalPentType.threeTwo)
 335      ∧ (cm4 (inducedSqEdges pentAVert a alpha) < 0
 336        ∧ cm4 (inducedSqEdges pentBVert a alpha) < 0
 337        ∧ cm4 (inducedSqEdges pentCVert a alpha) < 0)
 338      ∧ (0 < cm4 (wick CausalPentType.threeTwo
 339            (inducedSqEdges pentAVert a alpha))
 340        ∧ 0 < cm4 (wick CausalPentType.threeTwo
 341            (inducedSqEdges pentBVert a alpha))
 342        ∧ 0 < cm4 (wick CausalPentType.threeTwo
 343            (inducedSqEdges pentCVert a alpha))) := by
 344  have halpha0 : 0 < alpha := lt_trans (by norm_num) halpha
 345  exact ⟨⟨induced_pentA_eq a alpha, induced_pentB_eq a alpha,
 346      induced_pentC_eq a alpha⟩,
 347    threePent_lorentzian_class a alpha ha halpha0,
 348    threePent_lorentzian_cm4_neg a alpha ha halpha0.le,
 349    threePent_euclidean_admissible a alpha ha halpha⟩
 350
 351/-! ## §7. Axiom audit
 352
 353Expected for each: `[propext, Classical.choice, Quot.sound]` (no
 354`sorryAx`, no `Lean.ofReduceBool`, no repo-local axioms). -/
 355
 356#print axioms induced_pentA_eq
 357#print axioms induced_pentB_eq
 358#print axioms induced_pentC_eq
 359#print axioms shared_face_consistency
 360#print axioms threePent_lorentzian_cm4_neg
 361#print axioms threePent_euclidean_admissible
 362#print axioms threePent_causal_assignment
 363#print axioms physical_point_regular
 364
 365end
 366
 367end ThreePentCausalConsistency
 368end SevenGaps
 369end Gravity
 370end IndisputableMonolith
 371