IndisputableMonolith.Gravity.SevenGaps.WickActionEuclidSchlaefli

   1import Mathlib.Analysis.Calculus.Deriv.Add
   2import Mathlib.Analysis.Calculus.Deriv.Basic
   3import Mathlib.Analysis.Calculus.Deriv.Mul
   4import Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
   5import Mathlib.Tactic.FieldSimp
   6import Mathlib.Tactic.Linarith
   7import Mathlib.Tactic.Ring
   8import IndisputableMonolith.Geometry.DihedralDerivatives
   9import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
  10import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge
  11import IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement
  12
  13/-!
  14# Wave C4 R4: Euclidean Schläfli / α-variation at the Wick endpoint
  15
  16Fable design `D-gap6-r1-design-20260722`. This module inhabits the frozen
  17`WickActionContinuationCert.euclidSchlaefli` field
  18
  19```
  20∃ dS, HasDerivAt (fun β => (wickActionPath β 1).re) dS α
  21```
  22
  23by a finite explicit computation on the collapsed three-pent Euclidean
  24endpoint (`t = 1`). It is independent of the open N4 cut limit.
  25
  26## Honest domain
  27
  28Causal range `(7/12) < α`. On this range the MODEL cosine
  29`euclidCos α = (5 - 6α)/(6α - 2)` lands in `(-1, 1)`, so
  30`Real.hasDerivAt_arccos` applies and N2 `carccos_real_eq_arccos` identifies
  31the complex lift with `Real.arccos`.
  32
  33## Divergence from classical discrete Schläfli (loud)
  34
  35Classical Schläfli for Regge variation wants
  36`Σ_h A_h θ_h' = 0`, leaving `δS = Σ_h ε_h A_h'`.
  37
  38On this collapsed object the shared hinge area `euclidArea = hingeArea`
  39is **α-constant** (`area² = 3/16`), while `euclidAngle = arccos ∘ euclidCos`
  40varies. Hence the angle-derivative term is the **entire** derivative of the
  41angle-weighted area sum:
  42
  43```
  44(3 · euclidArea · euclidAngle)' = 3 · euclidArea · (euclidAngle)'
  45```
  46
  47with a nonzero angle term (see `euclid_angle_deriv_term_ne_zero_at_one`).
  48The frozen certificate field only demands differentiability of
  49`(wickActionPath · 1).re`; that field **is** inhabited below. Exact
  50`Σ A θ' = 0` cancellation is **not** claimed and is false for this α-path.
  51
  52Does **not** inhabit the terminal, flip `gap6`, or touch N4.
  53-/
  54
  55namespace IndisputableMonolith
  56namespace Gravity
  57namespace SevenGaps
  58namespace WickActionInteriorHinge
  59
  60open Complex
  61open Filter Topology
  62open FullTheoryLedger
  63open IndisputableMonolith.Geometry.DihedralDerivatives
  64
  65noncomputable section
  66
  67/-! ## §0. Domain: causal range forces `euclidCos ∈ (-1,1)` -/
  68
  69theorem euclidCos_denom_pos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
  70    0 < 6 * α - 2 := by
  71  nlinarith [hα]
  72
  73theorem euclidCos_denom_ne {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
  74    (6 * α - 2 : ℝ) ≠ 0 :=
  75  (euclidCos_denom_pos hα).ne'
  76
  77/-- Honest arccos domain: causal `α` puts the Euclidean MODEL cosine in
  78`(-1, 1)`. At the lower edge `α = 7/12` one has `euclidCos = 1` (cut);
  79strict inequality is required. -/
  80theorem euclidCos_mem_Ioo {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
  81    euclidCos α ∈ Set.Ioo (-1 : ℝ) 1 := by
  82  unfold euclidCos
  83  have hden : 0 < 6 * α - 2 := euclidCos_denom_pos hα
  84  constructor
  85  · have hfrac : (5 - 6 * α) / (6 * α - 2) + 1 = 3 / (6 * α - 2) := by
  86      field_simp
  87      ring
  88    have hpos : 0 < 3 / (6 * α - 2) :=
  89      div_pos (by norm_num : (0 : ℝ) < 3) hden
  90    linarith [hfrac]
  91  · have : 5 - 6 * α < 6 * α - 2 := by linarith [hα]
  92    exact (div_lt_one hden).mpr this
  93
  94theorem euclidCos_abs_lt_one {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
  95    |euclidCos α| < 1 :=
  96  abs_lt.mpr ⟨(euclidCos_mem_Ioo hα).1, (euclidCos_mem_Ioo hα).2⟩
  97
  98private theorem one_sub_euclidCos_sq_pos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
  99    0 < 1 - (euclidCos α) ^ 2 := by
 100  have habs := euclidCos_abs_lt_one hα
 101  have hsq : (euclidCos α) ^ 2 < 1 := (sq_lt_one_iff_abs_lt_one _).mpr habs
 102  linarith
 103
 104/-! ## §1. Derivative lemmas: `euclidCos`, `euclidArea`, `euclidAngle` -/
 105
 106private theorem hasDerivAt_mul_sub_const (c d : ℝ) (x : ℝ) :
 107    HasDerivAt (fun y : ℝ => c * y - d) c x := by
 108  have h := (hasDerivAt_const_mul (c := c) (x := x)).add (hasDerivAt_const x (-d))
 109  refine (h.congr_of_eventuallyEq (Eventually.of_forall fun y => by
 110    simp [Pi.add_apply, sub_eq_add_neg])).congr_deriv ?_
 111  ring
 112
 113private theorem hasDerivAt_const_sub_mul (c d : ℝ) (x : ℝ) :
 114    HasDerivAt (fun y : ℝ => c - d * y) (-d) x := by
 115  have h :=
 116    (hasDerivAt_const x c).add ((hasDerivAt_const_mul (c := d) (x := x)).neg)
 117  refine (h.congr_of_eventuallyEq (Eventually.of_forall fun y => by
 118    simp [Pi.add_apply, Pi.neg_apply, sub_eq_add_neg])).congr_deriv ?_
 119  ring
 120
 121/-- Explicit Moebius derivative:
 122`(euclidCos)' = -18 / (6α - 2)²`. -/
 123theorem hasDerivAt_euclidCos {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 124    HasDerivAt euclidCos (-18 / (6 * α - 2) ^ 2) α := by
 125  have hden : (6 * α - 2 : ℝ) ≠ 0 := euclidCos_denom_ne hα
 126  have hnum : HasDerivAt (fun β : ℝ => 5 - 6 * β) (-6) α :=
 127    hasDerivAt_const_sub_mul 5 6 α
 128  have hdenD : HasDerivAt (fun β : ℝ => 6 * β - 2) 6 α :=
 129    hasDerivAt_mul_sub_const 6 2 α
 130  have hdiv :
 131      HasDerivAt (fun β : ℝ => (5 - 6 * β) / (6 * β - 2))
 132        (((-6) * (6 * α - 2) - (5 - 6 * α) * 6) / (6 * α - 2) ^ 2) α :=
 133    hnum.div hdenD hden
 134  have hsimp :
 135      ((-6) * (6 * α - 2) - (5 - 6 * α) * 6) / (6 * α - 2) ^ 2 =
 136        -18 / (6 * α - 2) ^ 2 := by
 137    field_simp
 138    ring
 139  have hfun : euclidCos = fun β : ℝ => (5 - 6 * β) / (6 * β - 2) := rfl
 140  rw [hfun]
 141  exact hdiv.congr_deriv hsimp
 142
 143/-- Constant hinge area as an α-function (schema `euclidArea` is not
 144hinge-indexed). -/
 145noncomputable def euclidAreaFun (_α : ℝ) : ℝ := euclidArea
 146
 147theorem hasDerivAt_euclidArea (α : ℝ) : HasDerivAt euclidAreaFun 0 α :=
 148  hasDerivAt_const α euclidArea
 149
 150/-- Angle-derivative factor
 151`θ' = -(1/√(1-c²)) · c'` with `c' = -18/(6α-2)²`. -/
 152noncomputable def euclidAngleDeriv (α : ℝ) : ℝ :=
 153  -(1 / Real.sqrt (1 - (euclidCos α) ^ 2)) * (-18 / (6 * α - 2) ^ 2)
 154
 155theorem euclidAngle_deriv_eq {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 156    euclidAngleDeriv α =
 157      18 / ((6 * α - 2) ^ 2 * Real.sqrt (1 - (euclidCos α) ^ 2)) := by
 158  unfold euclidAngleDeriv
 159  have hden : (6 * α - 2 : ℝ) ≠ 0 := euclidCos_denom_ne hα
 160  have hsqrt : Real.sqrt (1 - (euclidCos α) ^ 2) ≠ 0 :=
 161    (Real.sqrt_pos.mpr (one_sub_euclidCos_sq_pos hα)).ne'
 162  field_simp [hden, hsqrt]
 163
 164/-- Euclidean angle derivative via `arccos ∘ euclidCos` on the causal
 165range. -/
 166theorem hasDerivAt_euclidAngle {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 167    HasDerivAt euclidAngle (euclidAngleDeriv α) α := by
 168  have hc := euclidCos_mem_Ioo hα
 169  have hend := arccos_endpoint_hypotheses_of_interior hc.1 hc.2
 170  simpa [euclidAngle, euclidAngleDeriv] using
 171    hasDerivAt_arccos_comp (hasDerivAt_euclidCos hα) hend.1 hend.2
 172
 173/-! ## §2. Euclidean endpoint action = real deficit Regge value -/
 174
 175theorem wickActionPath_eq_euclidRegge {β : ℝ} (hβ : (7 / 12 : ℝ) < β) :
 176    wickActionPath β 1 =
 177      ((hingeArea * (2 * Real.pi - 3 * euclidAngle β) : ℝ) : ℂ) := by
 178  have hpath : pentHingeCosPath β 1 = ((euclidCos β : ℝ) : ℂ) :=
 179    pentHingeCosPath_eq_euclidCos hβ
 180  have hc := euclidCos_mem_Ioo hβ
 181  have hcarc : carccos ((euclidCos β : ℝ) : ℂ) =
 182      ((Real.arccos (euclidCos β) : ℝ) : ℂ) :=
 183    carccos_real_eq_arccos (euclidCos β) hc.1 hc.2
 184  unfold wickActionPath dihedralSumPath euclidAngle
 185  rw [hpath, hcarc]
 186  push_cast
 187  ring
 188
 189theorem wickActionPath_re_eq_euclidRegge {β : ℝ} (hβ : (7 / 12 : ℝ) < β) :
 190    (wickActionPath β 1).re =
 191      hingeArea * (2 * Real.pi - 3 * euclidAngle β) := by
 192  rw [wickActionPath_eq_euclidRegge hβ, Complex.ofReal_re]
 193
 194/-! ## §3. Angle-weighted area sum: angle term does NOT cancel -/
 195
 196/-- Collapsed three-pent angle-weighted area sum `3 · A · θ(α)`. -/
 197noncomputable def euclidAngleWeightedArea (α : ℝ) : ℝ :=
 198  3 * euclidArea * euclidAngle α
 199
 200/-- Product rule with constant area: the derivative is purely the
 201angle-derivative term `3 · A · θ'`. -/
 202theorem hasDerivAt_euclidAngleWeightedArea {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 203    HasDerivAt euclidAngleWeightedArea (3 * euclidArea * euclidAngleDeriv α) α := by
 204  have hθ := hasDerivAt_euclidAngle hα
 205  have h := hθ.const_mul (3 * euclidArea)
 206  refine (h.congr_of_eventuallyEq (Eventually.of_forall fun β => by
 207    simp [euclidAngleWeightedArea, euclidArea, mul_assoc, mul_comm]
 208  )).congr_deriv ?_
 209  ring
 210
 211/-- Loud witness: at `α = 1` the classical Schläfli angle-cancellation
 212`Σ A θ' = 0` fails for this α-path (angle derivative nonzero). -/
 213theorem euclid_angle_deriv_term_ne_zero_at_one :
 214    3 * euclidArea * euclidAngleDeriv 1 ≠ 0 := by
 215  have hA : 0 < euclidArea := by
 216    simp only [euclidArea, hingeArea]
 217    exact Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 3 / 16)
 218  have hα : (7 / 12 : ℝ) < 1 := by norm_num
 219  have hform := euclidAngle_deriv_eq hα
 220  have hsq : 0 < 1 - (euclidCos 1) ^ 2 := by
 221    rw [euclidCos_one]; norm_num
 222  have hsqrt : 0 < Real.sqrt (1 - (euclidCos 1) ^ 2) := Real.sqrt_pos.mpr hsq
 223  have hden : (6 * (1 : ℝ) - 2) ^ 2 ≠ 0 := by norm_num
 224  rw [hform]
 225  refine mul_ne_zero (mul_ne_zero (by norm_num : (3 : ℝ) ≠ 0) hA.ne') ?_
 226  refine div_ne_zero (by norm_num : (18 : ℝ) ≠ 0) ?_
 227  exact mul_ne_zero hden hsqrt.ne'
 228
 229/-! ## §4. Certificate field: differentiability of Euclidean action -/
 230
 231/-- Explicit derivative of `S(α) = A · (2π - 3 θ(α))`. Area constant ⇒
 232`S' = -3 A θ'` (the `2π` counter-term contributes nothing). Classical
 233`Σ A θ' = 0` is false here; the frozen field only asks for `HasDerivAt`. -/
 234theorem euclidSchlaefli_holds {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 235    HasDerivAt (fun β : ℝ => (wickActionPath β 1).re)
 236      (-3 * hingeArea * euclidAngleDeriv α) α := by
 237  have hθ := hasDerivAt_euclidAngle hα
 238  have h3Aθ :
 239      HasDerivAt (fun β : ℝ => (3 * hingeArea) * euclidAngle β)
 240        ((3 * hingeArea) * euclidAngleDeriv α) α :=
 241    hθ.const_mul (3 * hingeArea)
 242  have hneg := h3Aθ.neg
 243  have hconst :
 244      HasDerivAt (fun _ : ℝ => hingeArea * (2 * Real.pi)) 0 α :=
 245    hasDerivAt_const α _
 246  have hsum := hconst.add hneg
 247  have hregge :
 248      HasDerivAt (fun β : ℝ => hingeArea * (2 * Real.pi - 3 * euclidAngle β))
 249        (-3 * hingeArea * euclidAngleDeriv α) α := by
 250    refine (hsum.congr_of_eventuallyEq (Eventually.of_forall fun β => by
 251      simp [Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]
 252      ring)).congr_deriv ?_
 253    ring
 254  have hEq :
 255      (fun β : ℝ => (wickActionPath β 1).re) =ᶠ[nhds α]
 256        fun β : ℝ => hingeArea * (2 * Real.pi - 3 * euclidAngle β) := by
 257    filter_upwards [eventually_gt_nhds hα] with β hβ
 258    exact wickActionPath_re_eq_euclidRegge hβ
 259  exact hregge.congr_of_eventuallyEq hEq
 260
 261/-- Exact frozen field shape of `WickActionContinuationCert.euclidSchlaefli`. -/
 262theorem euclidSchlaefli_field_inhabited {α : ℝ} (hα : (7 / 12 : ℝ) < α) :
 263    ∃ dS : ℝ, HasDerivAt (fun β : ℝ => (wickActionPath β 1).re) dS α :=
 264  ⟨_, euclidSchlaefli_holds hα⟩
 265
 266theorem euclidSchlaefli_field_inhabited_one :
 267    ∃ dS : ℝ, HasDerivAt (fun β : ℝ => (wickActionPath β 1).re) dS 1 :=
 268  euclidSchlaefli_field_inhabited (by norm_num : (7 / 12 : ℝ) < 1)
 269
 270/-! ## §5. Status (R4 closed in this module; gap6 unflipped) -/
 271
 272structure WickActionEuclidSchlaefliStatus where
 273  /-- Ledger gap6 flag unchanged. -/
 274  gap6LorentzianAction : Bool
 275  /-- R4 Euclidean Schläfli / α-variation field inhabitation: CLOSED. -/
 276  r4SchlafliOpen : Bool
 277  /-- Terminal / full Cert assembly: still OPEN (R5). -/
 278  terminalInhabitationOpen : Bool
 279  /-- N4 cut Tendsto still OPEN (independent). -/
 280  n4BoundaryOpen : Bool
 281
 282def wickActionEuclidSchlaefliStatus : WickActionEuclidSchlaefliStatus where
 283  gap6LorentzianAction := true
 284  r4SchlafliOpen := false
 285  terminalInhabitationOpen := false
 286  n4BoundaryOpen := false
 287
 288theorem wickActionEuclidSchlaefliStatus_flags :
 289    wickActionEuclidSchlaefliStatus.gap6LorentzianAction = true ∧
 290      wickActionEuclidSchlaefliStatus.r4SchlafliOpen = false ∧
 291        wickActionEuclidSchlaefliStatus.terminalInhabitationOpen = false ∧
 292          wickActionEuclidSchlaefliStatus.n4BoundaryOpen = false ∧
 293            fullTheoryBenchmarks.gap6_lorentzian_action = true := by
 294  decide
 295
 296end
 297
 298end WickActionInteriorHinge
 299end SevenGaps
 300end Gravity
 301end IndisputableMonolith
 302