IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.ZqPhaseStructure
   3import IndisputableMonolith.Gravity.SevenGaps.RegulatorRemovalNoGo
   4
   5/-!
   6# Seven Gaps, P2-a: the phased quotient cutoff blocker
   7
   8This module isolates the exact analytic and API obligations for removing the
   9complexity cutoff from the phased quotient path sum.
  10
  11The fixed-cap API can express a family of phase models and hence a sequence of
  12finite quotient sums. Completeness of `ℂ` gives an exact criterion: that
  13sequence has a limit if and only if it is Cauchy.
  14
  15The cap-free exact-shell API gives the panel-locked form. `Zcap phase B` sums
  16the exact quotient shells in `range B`, and `OscillatoryTail phase` uniformly
  17quantifies every sufficiently late contiguous shell block. Exact telescoping
  18proves `CauchySeq (Zcap phase) ↔ OscillatoryTail phase`. This is the
  19cancellation statement that a substrate-derived phase must supply. It is
  20discriminating: the zero phase has an explicit epsilon-one failure witness.
  21
  22One bridge is still absent from the current API. `Zq B` uses the capped
  23quotient `TriangulationClass B`, while the nonduplicating shell decomposition
  24uses `ExactPathClass n`. `CapShellCompatibility` names the smallest required
  25cross-API statement: equality of the two finite sums at every cap. Under that
  26bridge, convergence of the existing phased `Zq` sequence is equivalent to the
  27exact-shell tail-cancellation criterion.
  28
  29All limits here remove a complexity cutoff. They are not mesh refinement and
  30carry no claim about continuum geometry, observations, a convergence rate, a
  31derived measure, or the full-theory ledger.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Gravity
  36namespace SevenGaps
  37namespace ZqContinuumBlocker
  38
  39open PathSumMeasure
  40open QuotientFirstZ
  41open ZqPhaseStructure
  42open ExactShellGaugeUV
  43
  44noncomputable section
  45
  46/-! ## 1. What the current capped `Zq` API can state -/
  47
  48/-- A phase choice at every complexity cap. This supplies no cross-cap
  49coherence by itself. -/
  50abbrev CapPhaseFamily := ∀ B : ℕ, PhaseModel B
  51
  52/-- The finite phased quotient sum at each cap. -/
  53def phasedZqSequence (P : CapPhaseFamily) : ℕ → ℂ :=
  54  fun B => Zq B (phasedWeight (P B))
  55
  56/-- Removal of the complexity cap for the existing capped quotient sums.
  57This is not a mesh-refinement limit. -/
  58def HasPhasedZqComplexityLimit (P : CapPhaseFamily) : Prop :=
  59  ∃ L : ℂ, Filter.Tendsto (phasedZqSequence P) Filter.atTop (nhds L)
  60
  61/-- The exact Cauchy obligation on the existing finite quotient sums. -/
  62def PhasedZqCauchyCriterion (P : CapPhaseFamily) : Prop :=
  63  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ m : ℕ, N ≤ m → ∀ n : ℕ, N ≤ n →
  64    ‖phasedZqSequence P m - phasedZqSequence P n‖ < ε
  65
  66/-- **HEADLINE IFF.** The existing phased quotient sums have a
  67complexity-cutoff limit exactly when their cross-cap differences are Cauchy.
  68This theorem assumes no convergence and no physical continuum interpretation.
  69-/
  70theorem hasPhasedZqComplexityLimit_iff_cauchy (P : CapPhaseFamily) :
  71    HasPhasedZqComplexityLimit P ↔ PhasedZqCauchyCriterion P := by
  72  constructor
  73  · rintro ⟨L, hL⟩
  74    have hC := (Metric.cauchySeq_iff.mp hL.cauchySeq)
  75    intro ε hε
  76    obtain ⟨N, hN⟩ := hC ε hε
  77    refine ⟨N, fun m hm n hn => ?_⟩
  78    simpa only [dist_eq_norm] using hN m hm n hn
  79  · intro h
  80    have hC : CauchySeq (phasedZqSequence P) := by
  81      rw [Metric.cauchySeq_iff]
  82      exact h
  83    exact cauchySeq_tendsto_of_complete hC
  84
  85/-! ## 2. The cap-free exact-shell cutoff and its ordered tails -/
  86
  87/-- The unregulated phased amplitude of exact complexity shell `n`. -/
  88def exactShellAmplitude
  89    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (n : ℕ) : ℂ :=
  90  ∑ c : ExactPathClass n,
  91    (classMu c : ℂ) * Complex.exp (Complex.I * (phase n c : ℂ))
  92
  93/-! ### The binding C1 statement -/
  94
  95/-- The panel-locked exact-shell complexity cutoff. `Zcap phase B` contains
  96exactly the quotient shells with indices in `range B`, hence complexities
  97strictly below `B`. This is a complexity cutoff, not mesh refinement. -/
  98def Zcap (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) : ℂ :=
  99  ∑ n ∈ Finset.range B, exactShellAmplitude phase n
 100
 101/-- The panel-locked oscillatory-tail requirement. Every sufficiently late
 102contiguous block of exact quotient shells must be small, uniformly in both
 103endpoints. No rate and no `Summable` hypothesis are imposed. -/
 104def OscillatoryTail
 105    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
 106  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ m n : ℕ, N ≤ m → m ≤ n →
 107    ‖∑ k ∈ Finset.Ico m n, exactShellAmplitude phase k‖ < ε
 108
 109/-- **C1 EXACT TELESCOPING.** The difference of two exact-shell cutoffs is
 110exactly the intervening contiguous shell block. -/
 111theorem Zcap_telescoping
 112    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) {m n : ℕ} (hmn : m ≤ n) :
 113    Zcap phase n - Zcap phase m =
 114      ∑ k ∈ Finset.Ico m n, exactShellAmplitude phase k := by
 115  exact (Finset.sum_Ico_eq_sub (exactShellAmplitude phase) hmn).symm
 116
 117/-- **C1 HEADLINE.** The exact-shell cutoff sequence is Cauchy if and only if
 118every sufficiently late contiguous shell block is uniformly small. This is a
 119pure complexity-cutoff criterion and assumes no desired convergence. -/
 120theorem cauchySeq_Zcap_iff_oscillatoryTail
 121    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
 122    CauchySeq (Zcap phase) ↔ OscillatoryTail phase := by
 123  constructor
 124  · intro hC
 125    have hMetric := Metric.cauchySeq_iff.mp hC
 126    intro ε hε
 127    obtain ⟨N, hN⟩ := hMetric ε hε
 128    refine ⟨N, fun m n hm hmn => ?_⟩
 129    have hn : N ≤ n := le_trans hm hmn
 130    have hd := hN m hm n hn
 131    rw [dist_eq_norm] at hd
 132    rw [← Zcap_telescoping phase hmn, norm_sub_rev]
 133    exact hd
 134  · intro htail
 135    rw [Metric.cauchySeq_iff]
 136    intro ε hε
 137    obtain ⟨N, hN⟩ := htail ε hε
 138    refine ⟨N, fun m hm n hn => ?_⟩
 139    rcases le_total m n with hmn | hnm
 140    · rw [dist_eq_norm, norm_sub_rev, Zcap_telescoping phase hmn]
 141      exact hN m n hm hmn
 142    · rw [dist_eq_norm, Zcap_telescoping phase hnm]
 143      exact hN n m hn hnm
 144
 145/-- The exact-shell quotient sum through complexity `B`. Each exact complex
 146occurs in one shell, so this avoids cross-cap duplication. -/
 147def exactComplexityCutoff
 148    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) : ℂ :=
 149  ∑ n ∈ Finset.range (B + 1), exactShellAmplitude phase n
 150
 151/-- Existence of the unregulated exact-shell complexity-cutoff limit.
 152This is not a mesh-refinement limit. -/
 153def HasExactComplexityCutoffLimit
 154    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
 155  ∃ L : ℂ, Filter.Tendsto (exactComplexityCutoff phase) Filter.atTop (nhds L)
 156
 157/-- The required oscillatory cancellation: every sufficiently late block of
 158exact shell amplitudes is small. The interval `(m,n]` is represented as
 159`Ico (m+1) (n+1)`. -/
 160def ExactShellTailCancellation
 161    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
 162  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ m n : ℕ, N ≤ m → m ≤ n →
 163    ‖∑ k ∈ Finset.Ico (m + 1) (n + 1), exactShellAmplitude phase k‖ < ε
 164
 165/-- The difference between two exact-shell cutoffs is exactly the intervening
 166ordered shell block. -/
 167theorem exactComplexityCutoff_sub
 168    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) {m n : ℕ} (hmn : m ≤ n) :
 169    exactComplexityCutoff phase n - exactComplexityCutoff phase m =
 170      ∑ k ∈ Finset.Ico (m + 1) (n + 1), exactShellAmplitude phase k := by
 171  exact (Finset.sum_Ico_eq_sub (exactShellAmplitude phase)
 172    (Nat.succ_le_succ hmn)).symm
 173
 174/-- **HEADLINE IFF, ORDERED-TAIL FORM.** The unregulated exact-shell quotient
 175cutoff has a limit exactly when its late shell blocks cancel in norm. This is
 176the analytic premise that a substrate-derived oscillatory phase must prove.
 177-/
 178theorem hasExactComplexityCutoffLimit_iff_tailCancellation
 179    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
 180    HasExactComplexityCutoffLimit phase ↔ ExactShellTailCancellation phase := by
 181  constructor
 182  · rintro ⟨L, hL⟩
 183    have hC := Metric.cauchySeq_iff.mp hL.cauchySeq
 184    intro ε hε
 185    obtain ⟨N, hN⟩ := hC ε hε
 186    refine ⟨N, fun m n hm hmn => ?_⟩
 187    have hn : N ≤ n := le_trans hm hmn
 188    have hd := hN m hm n hn
 189    rw [dist_eq_norm] at hd
 190    rw [← exactComplexityCutoff_sub phase hmn, norm_sub_rev]
 191    exact hd
 192  · intro htail
 193    have hC : CauchySeq (exactComplexityCutoff phase) := by
 194      rw [Metric.cauchySeq_iff]
 195      intro ε hε
 196      obtain ⟨N, hN⟩ := htail ε hε
 197      refine ⟨N, fun m hm n hn => ?_⟩
 198      rcases le_total m n with hmn | hnm
 199      · rw [dist_eq_norm, norm_sub_rev, exactComplexityCutoff_sub phase hmn]
 200        exact hN m n hm hmn
 201      · rw [dist_eq_norm, exactComplexityCutoff_sub phase hnm]
 202        exact hN n m hn hnm
 203    exact cauchySeq_tendsto_of_complete hC
 204
 205/-! ## 3. Concrete zero-phase failure witness -/
 206
 207/-- At zero phase, the unregulated exact shell amplitude is the positive real
 208shell mass. -/
 209theorem exactShellAmplitude_zeroPhase (n : ℕ) :
 210    exactShellAmplitude zeroPhase n = (shellMass n : ℂ) := by
 211  unfold exactShellAmplitude zeroPhase shellMass
 212  rw [Complex.ofReal_sum]
 213  refine Finset.sum_congr rfl fun c _ => ?_
 214  rw [Complex.ofReal_zero, mul_zero, Complex.exp_zero, mul_one]
 215
 216/-- **C1 EPSILON-ONE WITNESS.** Beyond every proposed tail threshold there
 217is a contiguous one-shell block whose zero-phase norm is greater than one.
 218The bridge is direct: `shellMass_lower` concerns the same cap-free exact
 219quotient `ExactPathClass` and the same `classMu` used by
 220`exactShellAmplitude`; it is neither a pre-quotient nor a cap-dependent mass.
 221-/
 222theorem zeroPhase_epsilon_one_failure (N : ℕ) :
 223    ∃ m n : ℕ, N ≤ m ∧ m ≤ n ∧
 224      1 < ‖∑ k ∈ Finset.Ico m n, exactShellAmplitude zeroPhase k‖ := by
 225  let k : ℕ := max 2 N
 226  have hNk : N ≤ k := le_max_right 2 N
 227  have hsingle :
 228      ∑ j ∈ Finset.Ico k (k + 1), exactShellAmplitude zeroPhase j =
 229        exactShellAmplitude zeroPhase k := by
 230    rw [Finset.sum_Ico_eq_sub (exactShellAmplitude zeroPhase)
 231      (Nat.le_succ k), Finset.sum_range_succ, add_sub_cancel_left]
 232  have hk2 : 2 ≤ k := le_max_left 2 N
 233  have hpowN : k ≤ k ^ (3 * k) :=
 234    Nat.le_self_pow (by omega) k
 235  have hpowR : ((k : ℕ) : ℝ) ≤ ((k : ℕ) : ℝ) ^ (3 * k) := by
 236    calc
 237      ((k : ℕ) : ℝ) ≤ ((k ^ (3 * k) : ℕ) : ℝ) := by
 238        exact_mod_cast hpowN
 239      _ = ((k : ℕ) : ℝ) ^ (3 * k) := Nat.cast_pow _ _
 240  have hkR : (1 : ℝ) < (k : ℕ) := by
 241    exact_mod_cast (show 1 < k by omega)
 242  have hmass : (1 : ℝ) < shellMass k := by
 243    have hlower := RegulatorRemovalNoGo.shellMass_lower k
 244    linarith
 245  refine ⟨k, k + 1, hNk, Nat.le_succ k, ?_⟩
 246  rw [hsingle, exactShellAmplitude_zeroPhase, Complex.norm_real,
 247    Real.norm_eq_abs, abs_of_pos (shellMass_pos k)]
 248  exact hmass
 249
 250/-- **NON-VACUITY WITNESS.** Zero phase fails the ordered-tail cancellation
 251criterion. A one-shell late block already has norm greater than one, because
 252the positive shell masses grow at least as `n^(3n)`. -/
 253theorem zeroPhase_not_exactShellTailCancellation :
 254    ¬ ExactShellTailCancellation zeroPhase := by
 255  intro htail
 256  obtain ⟨N, hN⟩ := htail 1 one_pos
 257  let k : ℕ := max 2 N
 258  have hNk : N ≤ k := le_max_right 2 N
 259  have hsingle :
 260      ∑ j ∈ Finset.Ico (k + 1) ((k + 1) + 1),
 261          exactShellAmplitude zeroPhase j =
 262        exactShellAmplitude zeroPhase (k + 1) := by
 263    rw [Finset.sum_Ico_eq_sub (exactShellAmplitude zeroPhase)
 264      (Nat.le_succ (k + 1)), Finset.sum_range_succ, add_sub_cancel_left]
 265  have hsmall := hN k (k + 1) hNk (Nat.le_succ k)
 266  rw [hsingle, exactShellAmplitude_zeroPhase, Complex.norm_real,
 267    Real.norm_eq_abs, abs_of_pos (shellMass_pos (k + 1))] at hsmall
 268  have hk2 : 2 ≤ k := le_max_left 2 N
 269  have hpowN : k + 1 ≤ (k + 1) ^ (3 * (k + 1)) :=
 270    Nat.le_self_pow (by omega) (k + 1)
 271  have hpowR :
 272      ((k + 1 : ℕ) : ℝ) ≤ ((k + 1 : ℕ) : ℝ) ^ (3 * (k + 1)) := by
 273    calc
 274      ((k + 1 : ℕ) : ℝ)
 275          ≤ (((k + 1) ^ (3 * (k + 1)) : ℕ) : ℝ) := by
 276            exact_mod_cast hpowN
 277      _ = ((k + 1 : ℕ) : ℝ) ^ (3 * (k + 1)) := Nat.cast_pow _ _
 278  have hkR : (1 : ℝ) < (k + 1 : ℕ) := by
 279    exact_mod_cast (show 1 < k + 1 by omega)
 280  have hmass : (1 : ℝ) < shellMass (k + 1) := by
 281    have hlower := RegulatorRemovalNoGo.shellMass_lower (k + 1)
 282    linarith
 283  linarith
 284
 285/-- The panel-locked `OscillatoryTail` criterion fails at zero phase, with
 286the explicit epsilon-one witness above. -/
 287theorem zeroPhase_not_oscillatoryTail :
 288    ¬ OscillatoryTail zeroPhase := by
 289  intro htail
 290  obtain ⟨N, hN⟩ := htail 1 one_pos
 291  obtain ⟨m, n, hm, hmn, hlarge⟩ := zeroPhase_epsilon_one_failure N
 292  have hsmall := hN m n hm hmn
 293  linarith
 294
 295/-- Consequently the exact zero-phase `Zcap` sequence is not Cauchy. -/
 296theorem zeroPhase_Zcap_not_cauchy :
 297    ¬ CauchySeq (Zcap zeroPhase) := by
 298  rw [cauchySeq_Zcap_iff_oscillatoryTail]
 299  exact zeroPhase_not_oscillatoryTail
 300
 301/-- Zero phase has no unregulated exact-shell complexity-cutoff limit. -/
 302theorem not_hasExactComplexityCutoffLimit_zeroPhase :
 303    ¬ HasExactComplexityCutoffLimit zeroPhase := by
 304  rw [hasExactComplexityCutoffLimit_iff_tailCancellation]
 305  exact zeroPhase_not_exactShellTailCancellation
 306
 307/-- Zero phase fails both available removal routes: the unregulated
 308complexity cutoff and the positive Gaussian regulator-removal limit. Neither
 309statement is a mesh-refinement or physical-continuum claim. -/
 310theorem zeroPhase_fails_both_removal_routes :
 311    (¬ HasExactComplexityCutoffLimit zeroPhase) ∧
 312      (¬ HasZRSRegulatorRemoval zeroPhase) :=
 313  ⟨not_hasExactComplexityCutoffLimit_zeroPhase,
 314    RegulatorRemovalNoGo.not_hasZRSRegulatorRemoval_zeroPhase⟩
 315
 316/-! ## 4. The smallest missing bridge from capped `Zq` to exact shells -/
 317
 318/-- Cross-API compatibility needed to identify the current capped quotient
 319sum with the nonduplicating exact-shell cutoff. Current definitions do not
 320supply this equality. A construction should come from an equivalence between
 321bounded quotient classes at cap `B` and exact quotient classes in shells
 322`n ≤ B`, preserving the measure and phase. -/
 323structure CapShellCompatibility (P : CapPhaseFamily)
 324    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop where
 325  sum_eq : ∀ B : ℕ,
 326    phasedZqSequence P B = exactComplexityCutoff phase B
 327
 328/-- **BLOCKER CERTIFICATE.** Once the missing cap-to-shell compatibility is
 329supplied, convergence of the existing phased `Zq B` sequence is exactly the
 330ordered-tail cancellation obligation on exact shells. No desired convergence
 331is assumed. -/
 332theorem hasPhasedZqLimit_iff_exactShellTail_of_compatibility
 333    (P : CapPhaseFamily) (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
 334    (hcompat : CapShellCompatibility P phase) :
 335    HasPhasedZqComplexityLimit P ↔ ExactShellTailCancellation phase := by
 336  have hseq : phasedZqSequence P = exactComplexityCutoff phase :=
 337    funext hcompat.sum_eq
 338  unfold HasPhasedZqComplexityLimit
 339  rw [hseq]
 340  exact hasExactComplexityCutoffLimit_iff_tailCancellation phase
 341
 342/-- The zero phase family on the existing capped quotient API. -/
 343def zeroCapPhaseFamily : CapPhaseFamily :=
 344  fun _B =>
 345    { phase := fun _K => 0
 346      invariant := fun _K _K' _h => rfl }
 347
 348/-- A zero-phase capped family cannot both agree with the exact-shell
 349decomposition and have a complexity-cutoff limit. This is a concrete
 350discriminant for any proposed bridge implementation. -/
 351theorem zeroPhase_compatibility_and_limit_impossible :
 352    ¬ (CapShellCompatibility zeroCapPhaseFamily zeroPhase ∧
 353      HasPhasedZqComplexityLimit zeroCapPhaseFamily) := by
 354  rintro ⟨hcompat, hlimit⟩
 355  exact zeroPhase_not_exactShellTailCancellation
 356    ((hasPhasedZqLimit_iff_exactShellTail_of_compatibility
 357      zeroCapPhaseFamily zeroPhase hcompat).mp hlimit)
 358
 359#print axioms Zcap_telescoping
 360#print axioms cauchySeq_Zcap_iff_oscillatoryTail
 361#print axioms zeroPhase_epsilon_one_failure
 362#print axioms zeroPhase_not_oscillatoryTail
 363#print axioms zeroPhase_Zcap_not_cauchy
 364#print axioms hasPhasedZqComplexityLimit_iff_cauchy
 365#print axioms hasExactComplexityCutoffLimit_iff_tailCancellation
 366#print axioms zeroPhase_not_exactShellTailCancellation
 367#print axioms not_hasExactComplexityCutoffLimit_zeroPhase
 368#print axioms zeroPhase_fails_both_removal_routes
 369#print axioms hasPhasedZqLimit_iff_exactShellTail_of_compatibility
 370#print axioms zeroPhase_compatibility_and_limit_impossible
 371
 372end
 373
 374end ZqContinuumBlocker
 375end SevenGaps
 376end Gravity
 377end IndisputableMonolith
 378