IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete

   1import Mathlib.Data.Complex.Basic
   2import Mathlib.Analysis.Complex.Basic
   3import IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst
   4import IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
   5import IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges
   6
   7/-!
   8# Hinge-Data Wick Continuation, Complete Over Both Causal Types (Lane B3)
   9
  10QG Seven-Gaps campaign, lane B of the finishing charter, third deliverable:
  11the conjunction of the per-type certificates into a single completeness
  12statement over BOTH causal 4-simplex types and ALL twenty hinges.
  13
  14## Honest scope (MANDATED disclosure; read before citing this theorem)
  15
  16This is a **hinge-DATA continuation**: what is certified is the continuation
  17of the dihedral cosines and areas-squared of the triangular hinges of a
  18SINGLE causal 4-simplex of each type, along the canonical upper-half-plane
  19arc at the physical point `a = 1`, `alpha = 1`.  It is NOT an action-level
  20continuation.  The ACTION-LEVEL continuation (deficit angles summed over
  21the simplices sharing an interior hinge, hence the continued Regge action
  22itself) remains **OPEN**: it requires a genuine three-or-more-pent
  23interior-hinge simplicial complex, which is the C12 lane's prerequisite
  24question and is not touched here.  NO `FullTheoryLedger` flag is changed by
  25this module; `causalSimplex4DStatus.action_level_continuation_open` remains
  26`true`.
  27
  28## What the three packaged theorems state
  29
  30`wick_hinge_data_continuation_complete` (COSINE continuation) states, for
  31every unordered vertex pair `{p, q}` of `Fin 5` (equivalently every
  32triangular hinge, the complementary triple) and BOTH causal types:
  33
  34* fourOne: `BranchRegularOn` on the FULL open arc interior, continuity of
  35  the split-form cosine on the CLOSED interval `[0,1]`, and the Euclidean
  36  endpoint value `-(1/4)` (from `WickFourOneAllHinges`, B1);
  37* threeTwo: the same three certificates (from `WickThreeTwoHinges`, B2).
  38
  39`wick_hinge_areaSq_closed_forms_complete` (AREAS-SQUARED) states the
  40closed form of the area-squared of ALL twenty hinges, for every `z`:
  41`3/16` on the all-spacelike classes, `z/4 - 1/16` on the classes with
  42timelike edges (cut avoidance on the open interior is
  43`WickFourOneAllHinges.fourOne_areaSq_interior_off_cut`, the same two
  44closed forms).
  45
  46`wick_product_form_kills_memorialized` (KILL certificates) packages the
  47two exact product-form crossings: the diagonal-cofactor PRODUCT lands ON
  48the `csqrt` cut at interior arc parameters, value `-40` at `tStarMixed`
  49(mixed class, `Re z = 5/12`) and `-48` at `t = 2/3` exactly (upper-pair
  50class).  These memorialize the gate FAIL of the single-sqrt product
  51transcription; the split-sqrt form is the repaired convention.
  52
  53Endpoint honesty (inherited, not weakened here): branch certificates are
  54interior-only because several hinge data sit exactly ON a cut at the
  55Lorentzian endpoint (fourOne timelike-class cofactor `-8`; timelike-shape
  56`areaSq = -5/16`; the threeTwo spacelike hinge cosine `-11/8` ON the arccos
  57cut).  All are ALLOWED endpoint contacts under the executed gate
  58(`state/qg_full_theory/wick_arc_trace/RESULTS.txt`); the endpoint VALUES
  59are exact because each split cosine is proved continuous on `[0,1]`.
  60The Lorentzian endpoint carries the documented split-form sign factor
  61(`WickActionComplexFirst.lorentzian_endpoint_sign_factor`); no unrestricted
  62equality with the real Lorentzian formula is claimed.
  63
  64## Honesty tiers
  65
  66* MODEL: nothing new; all definitions inherited from
  67  `WickActionComplexFirst`, `WickFourOneAllHinges`, `WickThreeTwoHinges`.
  68* THEOREM: `wick_hinge_data_continuation_complete`,
  69  `wick_hinge_areaSq_closed_forms_complete`,
  70  `wick_product_form_kills_memorialized` (kernel-checked conjunctions of
  71  the B1 and B2 results; sorry-free).
  72* OPEN: the action-level continuation (C12 lane), exactly as flagged in
  73  `CausalSimplex4D.causalSimplex4DStatus`.
  74-/
  75
  76namespace IndisputableMonolith
  77namespace Gravity
  78namespace SevenGaps
  79namespace WickHingeDataComplete
  80
  81open CausalSimplex4D
  82open WickActionComplexFirst
  83open WickFourOneAllHinges
  84open WickThreeTwoHinges
  85
  86/-- THEOREM (B3 headline, hinge-DATA continuation, complete): for EVERY
  87triangular hinge (every unordered opposite vertex pair `{p, q}`, both
  88orientations) of BOTH causal 4-simplex types, at the physical point
  89`a = 1`, `alpha = 1`, the split-form complex-first Wick continuation is
  90(i) branch-regular on the FULL open arc interior `Set.Ioo 0 1` and
  91(ii) a continuous path on the CLOSED interval `[0, 1]` ending at the
  92Euclidean regular-4-simplex cosine `-(1/4)`.
  93
  94SCOPE: hinge data (dihedral cosines and areas-squared of single-simplex
  95hinges) ONLY.  The action-level continuation stays OPEN (the C12
  96three-pent interior-hinge complex is its prerequisite); no
  97`FullTheoryLedger` flag is touched by this result. -/
  98theorem wick_hinge_data_continuation_complete :
  99    ∀ p q : Fin 5, p ≠ q →
 100      (BranchRegularOn
 101          (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q
 102          (Set.Ioo 0 1)
 103        ∧ ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
 104        ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ))
 105      ∧ (BranchRegularOn
 106          (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
 107          (Set.Ioo 0 1)
 108        ∧ ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
 109        ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ)) := by
 110  intro p q hpq
 111  obtain ⟨h41cont, h41end⟩ :=
 112    wick_boundary_continuation_fourOne_allHinges p q hpq
 113  obtain ⟨h32branch, h32cont, h32end⟩ :=
 114    wick_continuation_threeTwo_hinges p q hpq
 115  exact ⟨⟨branchRegular_fourOne_allHinges p q hpq, h41cont, h41end⟩,
 116    ⟨h32branch, h32cont, h32end⟩⟩
 117
 118/-- THEOREM (B3, areas-squared complete): the closed forms of ALL twenty
 119hinge areas-squared, both causal types, for every `z`: `3/16` on the
 120all-spacelike classes, `z/4 - 1/16` on every class with timelike edges.
 121Cut avoidance on the open arc interior is
 122`WickFourOneAllHinges.fourOne_areaSq_interior_off_cut` (identical two
 123closed forms; the `-5/16` Lorentzian endpoint contact is the documented
 124allowed contact). -/
 125theorem wick_hinge_areaSq_closed_forms_complete (z : ℂ) :
 126    (hingeAreaSqC (hingeEdgesC z) 0 1 2 = (3 / 16 : ℂ)
 127        ∧ hingeAreaSqC (hingeEdgesC z) 0 1 3 = (3 / 16 : ℂ)
 128        ∧ hingeAreaSqC (hingeEdgesC z) 0 2 3 = (3 / 16 : ℂ)
 129        ∧ hingeAreaSqC (hingeEdgesC z) 1 2 3 = (3 / 16 : ℂ))
 130      ∧ (hingeAreaSqC (hingeEdgesC z) 0 1 4 = z / 4 - 1 / 16
 131        ∧ hingeAreaSqC (hingeEdgesC z) 0 2 4 = z / 4 - 1 / 16
 132        ∧ hingeAreaSqC (hingeEdgesC z) 0 3 4 = z / 4 - 1 / 16
 133        ∧ hingeAreaSqC (hingeEdgesC z) 1 2 4 = z / 4 - 1 / 16
 134        ∧ hingeAreaSqC (hingeEdgesC z) 1 3 4 = z / 4 - 1 / 16
 135        ∧ hingeAreaSqC (hingeEdgesC z) 2 3 4 = z / 4 - 1 / 16)
 136      ∧ (hingeAreaSqC (hingeEdges32C z) 0 1 2 = (3 / 16 : ℂ)
 137        ∧ hingeAreaSqC (hingeEdges32C z) 0 1 3 = z / 4 - 1 / 16
 138        ∧ hingeAreaSqC (hingeEdges32C z) 0 1 4 = z / 4 - 1 / 16
 139        ∧ hingeAreaSqC (hingeEdges32C z) 0 2 3 = z / 4 - 1 / 16
 140        ∧ hingeAreaSqC (hingeEdges32C z) 0 2 4 = z / 4 - 1 / 16
 141        ∧ hingeAreaSqC (hingeEdges32C z) 1 2 3 = z / 4 - 1 / 16
 142        ∧ hingeAreaSqC (hingeEdges32C z) 1 2 4 = z / 4 - 1 / 16
 143        ∧ hingeAreaSqC (hingeEdges32C z) 0 3 4 = z / 4 - 1 / 16
 144        ∧ hingeAreaSqC (hingeEdges32C z) 1 3 4 = z / 4 - 1 / 16
 145        ∧ hingeAreaSqC (hingeEdges32C z) 2 3 4 = z / 4 - 1 / 16) :=
 146  ⟨fourOne_areaSq_spacelike z, fourOne_areaSq_timelike z,
 147    threeTwo_areaSq_closed z⟩
 148
 149/-- THEOREM (B3, kill certificates memorialized): the two product-form
 150gate FAIL events as one kernel statement: at interior arc parameters the
 151diagonal-cofactor PRODUCT sits ON the `csqrt` branch cut with the exact
 152values `-40` (mixed class, `tStarMixed`) and `-48` (upper-pair class,
 153`t = 2/3` exactly).  The single-sqrt product transcription stays KILLED;
 154the split-sqrt form is the repaired convention. -/
 155theorem wick_product_form_kills_memorialized :
 156    (tStarMixed ∈ Set.Ioo (0 : ℝ) 1
 157      ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 1 1
 158          * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 4 4
 159          = -40
 160      ∧ (-40 : ℂ) ∉ Complex.slitPlane)
 161      ∧ ((2 / 3 : ℝ) ∈ Set.Ioo (0 : ℝ) 1
 162      ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 1 1
 163          * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 2 2
 164          = -48
 165      ∧ (-48 : ℂ) ∉ Complex.slitPlane) :=
 166  ⟨product_form_crossing_threeTwo_mixed, product_form_crossing_threeTwo_upper⟩
 167
 168/-- Documentation theorem (by `rfl` on the hand-set status record): the
 169action-level continuation flag of the kinematical layer is still OPEN.
 170This module proves hinge-data continuation and deliberately does NOT
 171change that status. -/
 172theorem action_level_still_open :
 173    causalSimplex4DStatus.action_level_continuation_open = true := rfl
 174
 175/-! ## Axiom audit
 176
 177Expected: `[propext, Classical.choice, Quot.sound]`. -/
 178
 179#print axioms wick_hinge_data_continuation_complete
 180#print axioms wick_hinge_areaSq_closed_forms_complete
 181#print axioms wick_product_form_kills_memorialized
 182
 183end WickHingeDataComplete
 184end SevenGaps
 185end Gravity
 186end IndisputableMonolith
 187