IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFamilyThreshold

   1import Mathlib.Tactic.Linarith
   2import Mathlib.Tactic.NormNum
   3import IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D
   4import IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly
   5
   6/-!
   7# Work item 5 (outcome b): Wick continuation threshold is complex-dependent
   8
   9Pillar 1 strengthen campaign, 2026-07-25. The action-level Wick certificate
  10(`WickActionContinuationCertV2`) hardcodes the causal range `α > 7/12` on one
  11fixed three-pent one-hinge complex of type `threeTwo`. Referees correctly
  12objected that this does not generalize as a complex-independent constant.
  13
  14This module converts that scope caveat into a structural finding: the
  15kinematical Wick Euclidean-admission threshold for causal 4-simplices is
  16already type-dependent in `CausalSimplex4D.alphaMin`, with
  17
  18* `alphaMin fourOne = 3/8`,
  19* `alphaMin threeTwo = 7/12`,
  20
  21and these are exact (iff) gates for `cm4 > 0` after Wick. The action-level
  22hardcoded `7/12` is therefore the `threeTwo` member of this threshold
  23function, not a universal constant. Outcome (a) (action-level continuation
  24for a genuine multi-complex family) is not attempted here: the CertV2
  25surface is specialized to the collapsed threeTwo one-hinge Möbius path, and
  26generalizing that analytic chain is a separate campaign.
  27
  28Two statements carry the weight, and they point opposite ways, which is the
  29honest picture. `universal_sufficient_threshold_eq_max` says `7/12` *is* a
  30complex-independent **sufficient** threshold: above it every type in the class
  31continues, because it is the maximum of the two type thresholds.
  32`no_common_typewise_exact_threshold` says it is not a complex-independent
  33**exact** gate: no constant is equivalent to admission for every type, since
  34`fourOne` continues down to `3/8`. So the hardcoded constant is defensible as a
  35sufficient condition and indefensible as a threshold, and the window
  36`(3/8, 7/12)` is where the difference is visible.
  37
  38The action-level consequence is `no_certV2_in_fourOne_only_window`: in that
  39window a `fourOne` simplex admits Euclidean continuation and no
  40`WickActionContinuationCertV2` exists at all, since the certificate's
  41`causalRange` field is `7/12 < α` by construction.
  42
  43Honesty:
  44* THEOREM: every declared theorem below is sorry-free; axioms are the
  45  standard Mathlib trio only.
  46* SCOPE: kinematical Wick Euclidean admission (`cm4 > 0` after `wick` of the
  47  Lorentzian causal tuple). This is the gate that decides which causal
  48  complexes admit Euclidean continuation; it is not a re-proof of the
  49  action-level `carccos` cut-limit chain.
  50* STRENGTH: the class has exactly two members, the two CDT causal 4-simplex
  51  types, so "non-constant threshold" is witnessed by one pair `(3/8, 7/12)`
  52  and the gap window `(3/8, 7/12)` is a single interval, not a family trend.
  53  Two members suffice to refute universality and do not establish a law.
  54  `alphaMin` and `cm4_euclidean_pos_iff` were both already banked; what is new
  55  here is the non-existence statement, the window, and the projection of the
  56  certificate's constant.
  57* OPEN, and this is why the referee objection is **not** closed: the
  58  action-level `WickActionContinuationCertV2` chain remains proved only on the
  59  collapsed `threeTwo` one-hinge Möbius path. Extending the `carccos` branch
  60  and cut-limit control to `fourOne` is the repair the referee actually asked
  61  for, and it is not attempted here. Kinematical non-degeneracy supplies none
  62  of that analytic content.
  63-/
  64
  65namespace IndisputableMonolith
  66namespace Gravity
  67namespace SevenGaps
  68namespace WickActionComplexFamilyThreshold
  69
  70open CausalSimplex4D
  71
  72noncomputable section
  73
  74/-! ## §1. Common class and general threshold function -/
  75
  76/-- Index of the class whose Wick Euclidean-admission threshold is tracked: the
  77two CDT causal 4-simplex types.
  78
  79Read this honestly. It is a one-field wrapper over a two-constructor enum. It
  80carries no simplices, no incidence, and no gluing, so it is a label for "which
  81causal type", not a model of a complex. The geometric content lives entirely in
  82`lorentzianSqEdges` and `cm4`, which the threshold theorems below call. -/
  83structure CausalWickComplex where
  84  ty : CausalPentType
  85
  86/-- The two inhabitants of the common class. -/
  87def fourOneComplex : CausalWickComplex := ⟨CausalPentType.fourOne⟩
  88
  89def threeTwoComplex : CausalWickComplex := ⟨CausalPentType.threeTwo⟩
  90
  91/-- General threshold function on the common class: the exact cm4
  92non-degeneracy gate after Wick Euclideanization. -/
  93def wickContinuationThreshold (K : CausalWickComplex) : ℝ :=
  94  alphaMin K.ty
  95
  96/-- Type-level form of the same threshold function (convenient for
  97quantification over `CausalPentType`). -/
  98def wickContinuationThresholdOf (ty : CausalPentType) : ℝ :=
  99  alphaMin ty
 100
 101theorem wickContinuationThreshold_eq_alphaMin (K : CausalWickComplex) :
 102    wickContinuationThreshold K = alphaMin K.ty :=
 103  rfl
 104
 105theorem wickContinuationThreshold_fourOne :
 106    wickContinuationThreshold fourOneComplex = (3 / 8 : ℝ) := by
 107  simp only [wickContinuationThreshold, fourOneComplex, alphaMin_fourOne]
 108
 109theorem wickContinuationThreshold_threeTwo :
 110    wickContinuationThreshold threeTwoComplex = (7 / 12 : ℝ) := by
 111  simp only [wickContinuationThreshold, threeTwoComplex, alphaMin_threeTwo]
 112
 113/-! ## §2. The thresholds differ -/
 114
 115/-- THEOREM (outcome b, core): the two members of the common class have
 116provably different continuation thresholds. -/
 117theorem wickContinuationThresholds_differ :
 118    wickContinuationThreshold fourOneComplex ≠
 119      wickContinuationThreshold threeTwoComplex := by
 120  rw [wickContinuationThreshold_fourOne, wickContinuationThreshold_threeTwo]
 121  norm_num
 122
 123/-- Strict inequality form used by gap witnesses. -/
 124theorem wickContinuationThreshold_fourOne_lt_threeTwo :
 125    wickContinuationThreshold fourOneComplex <
 126      wickContinuationThreshold threeTwoComplex := by
 127  rw [wickContinuationThreshold_fourOne, wickContinuationThreshold_threeTwo]
 128  norm_num
 129
 130/-- The class has at least two distinct inhabitants (distinct types). -/
 131theorem causalWickComplex_two_inhabitants :
 132    fourOneComplex.ty ≠ threeTwoComplex.ty := by
 133  simp only [fourOneComplex, threeTwoComplex]
 134  intro h
 135  cases h
 136
 137/-! ## §3. Exact gate: admission iff above the type's threshold -/
 138
 139/-- Kinematical Wick Euclidean admission: after Wick of the Lorentzian
 140causal tuple, the cm4 positivity criterion holds. -/
 141def WickEuclideanAdmissible (ty : CausalPentType) (a α : ℝ) : Prop :=
 142  0 < cm4 (wick ty (lorentzianSqEdges ty a α))
 143
 144/-- THEOREM: for every causal type and every positive spacelike scale, Wick
 145Euclidean admission holds if and only if the CDT ratio strictly exceeds that
 146type's threshold. This is the general threshold function made load-bearing. -/
 147theorem wickEuclideanAdmissible_iff (ty : CausalPentType) (a α : ℝ)
 148    (ha : 0 < a) :
 149    WickEuclideanAdmissible ty a α ↔
 150      wickContinuationThresholdOf ty < α := by
 151  unfold WickEuclideanAdmissible wickContinuationThresholdOf
 152  rw [wick_lorentzian]
 153  exact cm4_euclidean_pos_iff ty a α ha
 154
 155/-- Forward direction packaged for direct use. -/
 156theorem wickEuclideanAdmissible_of_gt_threshold (ty : CausalPentType)
 157    (a α : ℝ) (ha : 0 < a)
 158    (hα : wickContinuationThresholdOf ty < α) :
 159    WickEuclideanAdmissible ty a α :=
 160  (wickEuclideanAdmissible_iff ty a α ha).mpr hα
 161
 162/-- Degeneracy exactly at threshold (exactness of the gate). -/
 163theorem wickEuclideanAdmissible_false_at_threshold (ty : CausalPentType)
 164    (a : ℝ) (ha : 0 < a) :
 165    ¬ WickEuclideanAdmissible ty a (wickContinuationThresholdOf ty) := by
 166  intro h
 167  have hiff := (wickEuclideanAdmissible_iff ty a
 168    (wickContinuationThresholdOf ty) ha).mp h
 169  exact lt_irrefl _ hiff
 170
 171/-! ## §4. Gap witness: one ratio admits fourOne and rejects threeTwo -/
 172
 173/-- THEOREM (outcome b, structural witness): there exists a CDT ratio at which
 174the fourOne complex admits Wick Euclidean continuation and the threeTwo
 175complex does not. Concrete value `α = 1/2`, which lies strictly between
 176`3/8` and `7/12`. -/
 177theorem wickThreshold_gap_witness :
 178    ∃ α : ℝ,
 179      wickContinuationThreshold fourOneComplex < α ∧
 180        α < wickContinuationThreshold threeTwoComplex ∧
 181          (∀ a : ℝ, 0 < a → WickEuclideanAdmissible CausalPentType.fourOne a α) ∧
 182            ∀ a : ℝ, 0 < a →
 183              ¬ WickEuclideanAdmissible CausalPentType.threeTwo a α := by
 184  refine ⟨(1 / 2 : ℝ), ?_, ?_, ?_, ?_⟩
 185  · rw [wickContinuationThreshold_fourOne]; norm_num
 186  · rw [wickContinuationThreshold_threeTwo]; norm_num
 187  · intro a ha
 188    exact wickEuclideanAdmissible_of_gt_threshold CausalPentType.fourOne a (1 / 2)
 189      ha (by simp only [wickContinuationThresholdOf, alphaMin_fourOne]; norm_num)
 190  · intro a ha hAdm
 191    have hiff :=
 192      (wickEuclideanAdmissible_iff CausalPentType.threeTwo a (1 / 2) ha).mp hAdm
 193    simp only [wickContinuationThresholdOf, alphaMin_threeTwo] at hiff
 194    linarith
 195
 196/-! ## §5. No complex-independent threshold exists -/
 197
 198/-- The threshold function is not constant on the class. -/
 199theorem wickContinuationThresholdOf_not_constant :
 200    ¬ ∃ c : ℝ, ∀ ty : CausalPentType, wickContinuationThresholdOf ty = c := by
 201  rintro ⟨c, h⟩
 202  have h41 := h CausalPentType.fourOne
 203  have h32 := h CausalPentType.threeTwo
 204  simp only [wickContinuationThresholdOf, alphaMin_fourOne, alphaMin_threeTwo]
 205    at h41 h32
 206  rw [← h32] at h41
 207  norm_num at h41
 208
 209/-- **THEOREM.** No single real constant is *equivalent* to Wick Euclidean
 210admission for every causal type. Read the name literally: this refutes a
 211constant **exact** gate, and it does not refute a constant sufficient one, which
 212§6 supplies. A number written as "the" continuation threshold is a fact about
 213one type. -/
 214theorem no_common_typewise_exact_threshold :
 215    ¬ ∃ c : ℝ, ∀ (ty : CausalPentType) (a α : ℝ), 0 < a →
 216      (WickEuclideanAdmissible ty a α ↔ c < α) := by
 217  rintro ⟨c, h⟩
 218  have hone : (0 : ℝ) < 1 := one_pos
 219  have hadm41 : WickEuclideanAdmissible CausalPentType.fourOne 1 (1 / 2) :=
 220    wickEuclideanAdmissible_of_gt_threshold CausalPentType.fourOne 1 (1 / 2) hone
 221      (by simp only [wickContinuationThresholdOf, alphaMin_fourOne]; norm_num)
 222  have hc : c < 1 / 2 :=
 223    (h CausalPentType.fourOne 1 (1 / 2) hone).mp hadm41
 224  have hadm32 : WickEuclideanAdmissible CausalPentType.threeTwo 1 (1 / 2) :=
 225    (h CausalPentType.threeTwo 1 (1 / 2) hone).mpr hc
 226  have hlt :=
 227    (wickEuclideanAdmissible_iff CausalPentType.threeTwo 1 (1 / 2) hone).mp hadm32
 228  simp only [wickContinuationThresholdOf, alphaMin_threeTwo] at hlt
 229  linarith
 230
 231/-! ## §6. The constant `7/12` is sufficient for the class, exact for one type -/
 232
 233/-- Arithmetic identification of the constant with the `threeTwo` threshold.
 234This is a numeric fact about two rationals; it is **not** evidence that the
 235certificate's constant was derived from `alphaMin`. In
 236`WickActionCertAssembly` the field `causalRange : 7/12 < α` is a hardcoded
 237literal. The projection theorem `certV2_above_threeTwo_threshold` in §7 is what
 238actually connects the two. -/
 239theorem hardcodedConstant_eq_threeTwo_threshold :
 240    (7 / 12 : ℝ) = wickContinuationThreshold threeTwoComplex :=
 241  wickContinuationThreshold_threeTwo.symm
 242
 243/-- THEOREM: that constant is strictly larger than the fourOne threshold, so a
 244complex-independent reading of `7/12` as *the* threshold overstates the fourOne
 245gate. -/
 246theorem hardcodedConstant_gt_fourOne_threshold :
 247    wickContinuationThreshold fourOneComplex < (7 / 12 : ℝ) := by
 248  rw [hardcodedConstant_eq_threeTwo_threshold]
 249  exact wickContinuationThreshold_fourOne_lt_threeTwo
 250
 251/-- **THEOREM: `7/12` is a genuine complex-independent SUFFICIENT threshold.**
 252Joint admission of both types is equivalent to `7/12 < α`, which is the maximum
 253of the two type thresholds. This is the positive companion of
 254`no_common_typewise_exact_threshold`, and it is why the hardcoded constant is
 255defensible as a sufficient condition even though it is not the threshold. -/
 256theorem joint_wickEuclideanAdmissible_iff (a α : ℝ) (ha : 0 < a) :
 257    (WickEuclideanAdmissible CausalPentType.fourOne a α ∧
 258      WickEuclideanAdmissible CausalPentType.threeTwo a α) ↔
 259      (7 / 12 : ℝ) < α := by
 260  constructor
 261  · intro ⟨_, h32⟩
 262    have := (wickEuclideanAdmissible_iff CausalPentType.threeTwo a α ha).mp h32
 263    simpa [wickContinuationThresholdOf, alphaMin_threeTwo] using this
 264  · intro hα
 265    exact ⟨
 266      wickEuclideanAdmissible_of_gt_threshold CausalPentType.fourOne a α ha
 267        (by simp only [wickContinuationThresholdOf, alphaMin_fourOne]; linarith),
 268      wickEuclideanAdmissible_of_gt_threshold CausalPentType.threeTwo a α ha
 269        (by simp only [wickContinuationThresholdOf, alphaMin_threeTwo]; exact hα)⟩
 270
 271/-- Named form of the same fact: the complex-independent sufficient threshold is
 272the maximum of the type thresholds. -/
 273theorem universal_sufficient_threshold_eq_max (a α : ℝ) (ha : 0 < a) :
 274    (WickEuclideanAdmissible CausalPentType.fourOne a α ∧
 275      WickEuclideanAdmissible CausalPentType.threeTwo a α) ↔
 276      max (wickContinuationThreshold fourOneComplex)
 277        (wickContinuationThreshold threeTwoComplex) < α := by
 278  rw [joint_wickEuclideanAdmissible_iff a α ha,
 279    max_eq_right (le_of_lt wickContinuationThreshold_fourOne_lt_threeTwo),
 280    wickContinuationThreshold_threeTwo]
 281
 282/-! ## §7. Projecting the certificate's own constant -/
 283
 284/-- **THEOREM: every action-level certificate lives strictly above the
 285`threeTwo` kinematical threshold.** This consumes the certificate's
 286`causalRange` field, so unlike the arithmetic identification in §6 it is a
 287statement about `WickActionContinuationCertV2` itself. -/
 288theorem certV2_above_threeTwo_threshold {α : ℝ}
 289    (h : WickActionInteriorHinge.WickActionContinuationCertV2 α) :
 290    wickContinuationThreshold threeTwoComplex < α := by
 291  rw [wickContinuationThreshold_threeTwo]
 292  exact h.causalRange
 293
 294/-- **THEOREM: the window is real at the action level too.** For any CDT ratio
 295strictly between the two thresholds, a `fourOne` simplex admits Euclidean
 296continuation and no action-level certificate exists. This is the precise sense
 297in which `7/12` is a scope boundary of the certificate rather than of the
 298geometry. -/
 299theorem no_certV2_in_fourOne_only_window {α : ℝ}
 300    (h2 : α < wickContinuationThreshold threeTwoComplex) :
 301    ¬ WickActionInteriorHinge.WickActionContinuationCertV2 α := by
 302  intro h
 303  exact absurd (certV2_above_threeTwo_threshold h) (not_lt.mpr (le_of_lt h2))
 304
 305/-- Concrete witness of that window at `α = 1/2`: `fourOne` continues for every
 306positive spacelike scale, and no certificate exists. -/
 307theorem fourOne_only_window_witness :
 308    (∀ a : ℝ, 0 < a → WickEuclideanAdmissible CausalPentType.fourOne a (1 / 2)) ∧
 309      ¬ WickActionInteriorHinge.WickActionContinuationCertV2 (1 / 2) := by
 310  refine ⟨fun a ha => ?_, ?_⟩
 311  · exact wickEuclideanAdmissible_of_gt_threshold CausalPentType.fourOne a (1 / 2)
 312      ha (by simp only [wickContinuationThresholdOf, alphaMin_fourOne]; norm_num)
 313  · refine no_certV2_in_fourOne_only_window ?_
 314    rw [wickContinuationThreshold_threeTwo]
 315    norm_num
 316
 317end
 318
 319/-! ## Axiom audit
 320
 321Expected for each: `[propext, Classical.choice, Quot.sound]`. -/
 322
 323#print axioms wickContinuationThreshold_eq_alphaMin
 324#print axioms wickContinuationThreshold_fourOne
 325#print axioms wickContinuationThreshold_threeTwo
 326#print axioms wickContinuationThresholds_differ
 327#print axioms wickContinuationThreshold_fourOne_lt_threeTwo
 328#print axioms causalWickComplex_two_inhabitants
 329#print axioms wickEuclideanAdmissible_iff
 330#print axioms wickEuclideanAdmissible_of_gt_threshold
 331#print axioms wickEuclideanAdmissible_false_at_threshold
 332#print axioms wickThreshold_gap_witness
 333#print axioms wickContinuationThresholdOf_not_constant
 334#print axioms no_common_typewise_exact_threshold
 335#print axioms hardcodedConstant_eq_threeTwo_threshold
 336#print axioms hardcodedConstant_gt_fourOne_threshold
 337#print axioms joint_wickEuclideanAdmissible_iff
 338#print axioms universal_sufficient_threshold_eq_max
 339#print axioms certV2_above_threeTwo_threshold
 340#print axioms no_certV2_in_fourOne_only_window
 341#print axioms fourOne_only_window_witness
 342
 343end WickActionComplexFamilyThreshold
 344end SevenGaps
 345end Gravity
 346end IndisputableMonolith
 347