IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement

   1import Mathlib.Analysis.SpecialFunctions.Arcosh
   2import Mathlib.Analysis.SpecialFunctions.Complex.Log
   3import Mathlib.Tactic.Linarith
   4import Mathlib.Tactic.LinearCombination
   5import Mathlib.Tactic.Ring
   6import Mathlib.Tactic.FieldSimp
   7import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
   8import IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges
   9
  10/-!
  11# Wave C4 N3+N4: Moebius confinement + Lorentzian cut-boundary value
  12
  13Fable design `D-gap6-r1-design-20260722`, session 2.
  14
  15* **N3** (α-family, causal range): Moebius collapse, MODEL path equality,
  16  `Im < 0` confinement, `branchRegularSum` field shape. CLOSED.
  17* **N4**: cut-boundary Tendsto resisted after honest effort (Mathlib
  18  one-sided log/csqrt filter API). Design-authorized fallback: named Props
  19  `carccos_tendsto_at_cut_one` / `lorentzAnchor_one` / family Prop left open;
  20  decoy `lorentz_endpoint_not_real` and `rapidityPinned_one` CLOSED.
  21  Re-scopes R5 toward the sharper-blocker packaging path if the limit stays open.
  22
  23Does **not** inhabit the terminal, flip gap6, or touch Schläfli.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Gravity
  28namespace SevenGaps
  29namespace WickActionInteriorHinge
  30
  31open Complex
  32open Filter Topology
  33open CausalSimplex4D
  34open WickActionComplexFirst
  35open WickThreeTwoHinges
  36
  37noncomputable section
  38
  39/-! ## §N3a. Arc lemmas -/
  40
  41theorem continuationEdgesC_threeTwo (α t : ℝ) :
  42    continuationEdgesC CausalPentType.threeTwo 1 α t =
  43      hingeEdges32C (arcZ 1 α t) := by
  44  funext e
  45  unfold continuationEdgesC hingeEdges32C
  46  by_cases h : isTimelike CausalPentType.threeTwo e = true
  47  · rw [if_pos h, if_pos h]
  48  · rw [if_neg h, if_neg h]
  49    norm_num
  50
  51theorem normSq_arcZ_one (α t : ℝ) :
  52    Complex.normSq (arcZ 1 α t) = α ^ 2 := by
  53  unfold arcZ
  54  simp only [pow_two, mul_one]
  55  have hexp :
  56      Complex.normSq (Complex.exp (((Real.pi * (1 - t) : ℝ) : ℂ) * I)) = 1 := by
  57    have hre := Complex.exp_ofReal_mul_I_re (Real.pi * (1 - t))
  58    have him := Complex.exp_ofReal_mul_I_im (Real.pi * (1 - t))
  59    rw [Complex.normSq_apply, hre, him, ← pow_two, ← pow_two]
  60    exact Real.cos_sq_add_sin_sq (Real.pi * (1 - t))
  61  rw [Complex.normSq_mul, hexp, mul_one, Complex.normSq_ofReal]
  62
  63theorem denom_ne_of_causal {α : ℝ} (hα : (7 / 12 : ℝ) < α) (t : ℝ) :
  64    6 * arcZ 1 α t - 2 ≠ 0 := by
  65  intro h
  66  have hpos : 0 < α := lt_trans (by norm_num : (0 : ℝ) < 7 / 12) hα
  67  have h6 : (6 : ℂ) * arcZ 1 α t = 2 := by linear_combination h
  68  have hns :
  69      Complex.normSq ((6 : ℂ) * arcZ 1 α t) = Complex.normSq (2 : ℂ) := by
  70    rw [h6]
  71  rw [Complex.normSq_mul, normSq_arcZ_one, Complex.normSq_ofNat,
  72    Complex.normSq_ofNat] at hns
  73  have hα2 : α ^ 2 = (1 / 9 : ℝ) := by
  74    have : (36 : ℝ) * α ^ 2 = 4 := by convert hns using 1 <;> ring
  75    nlinarith
  76  have hgt : (1 / 9 : ℝ) < α ^ 2 := by
  77    have h13 : (1 / 3 : ℝ) < α :=
  78      lt_trans (by norm_num : (1 / 3 : ℝ) < 7 / 12) hα
  79    nlinarith [mul_self_lt_mul_self (by norm_num : (0 : ℝ) ≤ 1 / 3) h13]
  80  exact absurd hα2 (ne_of_gt hgt)
  81
  82theorem arcZ_im_eq (α t : ℝ) :
  83    (arcZ 1 α t).im = α * Real.sin (Real.pi * (1 - t)) := by
  84  unfold arcZ
  85  simp only [pow_two, mul_one]
  86  rw [mul_im, ofReal_re, ofReal_im, Complex.exp_ofReal_mul_I_im,
  87    Complex.exp_ofReal_mul_I_re]
  88  ring
  89
  90theorem arcZ_im_pos_of_causal {α t : ℝ} (hα : (7 / 12 : ℝ) < α)
  91    (ht : t ∈ Set.Ioo (0 : ℝ) 1) : 0 < (arcZ 1 α t).im := by
  92  have hpos : 0 < α := lt_trans (by norm_num : (0 : ℝ) < 7 / 12) hα
  93  rw [arcZ_im_eq]
  94  refine mul_pos hpos ?_
  95  apply Real.sin_pos_of_pos_of_lt_pi
  96  · exact mul_pos Real.pi_pos (by linarith [ht.2])
  97  · calc Real.pi * (1 - t) < Real.pi * 1 :=
  98        mul_lt_mul_of_pos_left (by linarith [ht.1]) Real.pi_pos
  99    _ = Real.pi := mul_one _
 100
 101/-! ## §N3b. Moebius + MODEL path equality -/
 102
 103theorem pentHingeCosPath_eq_moebius {α : ℝ} (hα : (7 / 12 : ℝ) < α)
 104    (t : ℝ) :
 105    pentHingeCosPath α t =
 106      (5 - 6 * arcZ 1 α t) / (6 * arcZ 1 α t - 2) := by
 107  unfold pentHingeCosPath dihedralCosSplitC dihedralDenomSplitC
 108  rw [continuationEdgesC_threeTwo]
 109  have hv3 : cmVertexIndexC 3 = 4 := rfl
 110  have hv4 : cmVertexIndexC 4 = 5 := rfl
 111  rw [hv3, hv4, cof32_d4, cof32_d5, cof32_45,
 112    csqrt_mul_self (denom_ne_of_causal hα t)]
 113
 114theorem pentHingeCosPath_eq_moebius_one (t : ℝ) :
 115    pentHingeCosPath 1 t = (5 - 6 * zArc t) / (6 * zArc t - 2) := by
 116  simpa [zArc] using
 117    pentHingeCosPath_eq_moebius (by norm_num : (7 / 12 : ℝ) < 1) t
 118
 119theorem pentHingeCosPath_one_eq_threeTwo :
 120    pentHingeCosPath 1 = threeTwoCosPath 3 4 := rfl
 121
 122theorem euclidCos_one : euclidCos 1 = -(1 / 4) := by
 123  unfold euclidCos; norm_num
 124
 125theorem lorentzCos_one : lorentzCos 1 = -(11 / 8) := by
 126  unfold lorentzCos; norm_num
 127
 128theorem pentHingeCosPath_eq_euclidCos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 129    pentHingeCosPath α 1 = ((euclidCos α : ℝ) : ℂ) := by
 130  rw [pentHingeCosPath_eq_moebius hα, arcZ_one, euclidCos]
 131  simp [ofReal_div, ofReal_sub, ofReal_mul, ofReal_ofNat]
 132
 133theorem pentHingeCosPath_eq_lorentzCos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 134    pentHingeCosPath α 0 = ((lorentzCos α : ℝ) : ℂ) := by
 135  rw [pentHingeCosPath_eq_moebius hα, arcZ_zero]
 136  have hreal :
 137      ((5 - 6 * (-α)) / (6 * (-α) - 2) : ℝ) = lorentzCos α := by
 138    unfold lorentzCos
 139    have h1 : (5 - 6 * (-α) : ℝ) = 5 + 6 * α := by ring
 140    have h2 : (6 * (-α) - 2 : ℝ) = -(2 + 6 * α) := by ring
 141    rw [h1, h2, div_neg]
 142  simp only [pow_two, mul_one]
 143  -- `(5 - 6 * ↑(-α)) / ... = ↑((5 - 6 * (-α)) / ...)` by ofReal homomorphism
 144  have hcast :
 145      (5 - 6 * ((-α : ℝ) : ℂ)) / (6 * ((-α : ℝ) : ℂ) - 2) =
 146        ((((5 - 6 * (-α)) / (6 * (-α) - 2)) : ℝ) : ℂ) := by
 147    norm_cast
 148  rw [hcast, hreal]
 149
 150theorem pentHingeCosPath_one_zero :
 151    pentHingeCosPath 1 0 = ((lorentzCos 1 : ℝ) : ℂ) :=
 152  pentHingeCosPath_eq_lorentzCos (by norm_num)
 153
 154theorem pentHingeCosPath_one_one :
 155    pentHingeCosPath 1 1 = ((euclidCos 1 : ℝ) : ℂ) :=
 156  pentHingeCosPath_eq_euclidCos (by norm_num)
 157
 158/-! ## §N3c. Half-plane confinement -/
 159
 160theorem im_pentHingeCosPath_eq {α : ℝ} (hα : (7 / 12 : ℝ) < α) (t : ℝ) :
 161    (pentHingeCosPath α t).im =
 162      (-18 * (arcZ 1 α t).im) / Complex.normSq (6 * arcZ 1 α t - 2) := by
 163  rw [pentHingeCosPath_eq_moebius hα]
 164  have hnum :
 165      (5 - 6 * arcZ 1 α t).im * (6 * arcZ 1 α t - 2).re -
 166        (5 - 6 * arcZ 1 α t).re * (6 * arcZ 1 α t - 2).im =
 167        -18 * (arcZ 1 α t).im := by
 168    simp only [sub_im, sub_re, mul_im, mul_re, re_ofNat, im_ofNat]
 169    ring
 170  rw [div_im, div_sub_div_same, hnum]
 171
 172theorem im_pentHingeCosPath_neg {α : ℝ} (hα : (7 / 12 : ℝ) < α)
 173    {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
 174    (pentHingeCosPath α t).im < 0 := by
 175  rw [im_pentHingeCosPath_eq hα]
 176  have hy : 0 < (arcZ 1 α t).im := arcZ_im_pos_of_causal hα ht
 177  exact div_neg_of_neg_of_pos
 178    (mul_neg_of_neg_of_pos (by norm_num) hy)
 179    (Complex.normSq_pos.mpr (denom_ne_of_causal hα t))
 180
 181theorem im_pentHingeCosPath_neg_one {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
 182    (pentHingeCosPath 1 t).im < 0 :=
 183  im_pentHingeCosPath_neg (by norm_num) ht
 184
 185/-! ## §N3d. branchRegularSum field shape -/
 186
 187theorem branchRegularSum_of_causal {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 188    ∀ t ∈ Set.Ioo (0 : ℝ) 1,
 189      OffArccosCut (pentHingeCosPath α t) ∧
 190        (1 - pentHingeCosPath α t ^ 2) ∈ slitPlane ∧
 191          (pentHingeCosPath α t + I * csqrt (1 - pentHingeCosPath α t ^ 2)) ∈
 192            slitPlane := by
 193  intro t ht
 194  have hoff : OffArccosCut (pentHingeCosPath α t) :=
 195    Or.inl (im_pentHingeCosPath_neg hα ht).ne
 196  exact ⟨hoff, offArccosCut_slitPlane _ hoff⟩
 197
 198theorem branchRegularSum_one :
 199    ∀ t ∈ Set.Ioo (0 : ℝ) 1,
 200      OffArccosCut (pentHingeCosPath 1 t) ∧
 201        (1 - pentHingeCosPath 1 t ^ 2) ∈ slitPlane ∧
 202          (pentHingeCosPath 1 t + I * csqrt (1 - pentHingeCosPath 1 t ^ 2)) ∈
 203            slitPlane :=
 204  branchRegularSum_of_causal (by norm_num)
 205
 206/-! ## §N4. Cut-boundary fallback (named Props) + closed decoy/rapidity -/
 207
 208/-- N4 missing limit at `α = 1` (design fallback: precisely-stated Prop). -/
 209def carccos_tendsto_at_cut_one : Prop :=
 210  Tendsto (fun t => carccos (pentHingeCosPath 1 t))
 211    (nhdsWithin (0 : ℝ) (Set.Ioi 0))
 212    (nhds ((↑(lorentzAngleRe 1) : ℂ) + I * ↑(lorentzRapidity 1)))
 213
 214/-- Family cut-boundary Prop (open; scope reduction). -/
 215def carccos_tendsto_at_cut_family : Prop :=
 216  ∀ α : ℝ, (7 / 12 : ℝ) < α →
 217    Tendsto (fun t => carccos (pentHingeCosPath α t))
 218      (nhdsWithin (0 : ℝ) (Set.Ioi 0))
 219      (nhds ((↑(lorentzAngleRe α) : ℂ) + I * ↑(lorentzRapidity α)))
 220
 221/-- `lorentzAnchor` field shape at `α = 1` (open; depends on cut Tendsto). -/
 222def lorentzAnchor_one : Prop :=
 223  Tendsto (wickActionPath 1) (nhdsWithin (0 : ℝ) (Set.Ioi 0))
 224    (nhds
 225      (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe 1) : ℝ) : ℂ) -
 226        I * ((hingeArea * (3 * lorentzRapidity 1) : ℝ) : ℂ)))
 227
 228theorem rapidityPinned_one : lorentzRapidity 1 ≠ 0 := by
 229  unfold lorentzRapidity
 230  rw [lorentzCos_one, abs_neg, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 11 / 8)]
 231  exact (Real.arcosh_pos (by norm_num : (1 : ℝ) < 11 / 8)).ne'
 232
 233theorem lorentz_endpoint_im_eq :
 234    (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe 1) : ℝ) : ℂ) -
 235        I * ((hingeArea * (3 * lorentzRapidity 1) : ℝ) : ℂ)).im =
 236      -(3 * hingeArea * lorentzRapidity 1) := by
 237  simp [sub_im, mul_im, I_re, I_im]
 238  ring
 239
 240/-- Decoy falsifier: Lorentzian endpoint action imaginary part nonzero. -/
 241theorem lorentz_endpoint_not_real :
 242    (((hingeArea * (2 * Real.pi - 3 * lorentzAngleRe 1) : ℝ) : ℂ) -
 243        I * ((hingeArea * (3 * lorentzRapidity 1) : ℝ) : ℂ)).im ≠ 0 := by
 244  rw [lorentz_endpoint_im_eq]
 245  have hA : 0 < hingeArea :=
 246    Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 3 / 16)
 247  have hR : 0 < lorentzRapidity 1 := by
 248    unfold lorentzRapidity
 249    rw [lorentzCos_one, abs_neg, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 11 / 8)]
 250    exact Real.arcosh_pos (by norm_num : (1 : ℝ) < 11 / 8)
 251  have hpos : 0 < 3 * hingeArea * lorentzRapidity 1 :=
 252    mul_pos (mul_pos (by norm_num : (0 : ℝ) < 3) hA) hR
 253  exact neg_ne_zero.mpr hpos.ne'
 254
 255
 256end
 257
 258end WickActionInteriorHinge
 259end SevenGaps
 260end Gravity
 261end IndisputableMonolith
 262