IndisputableMonolith.Gravity.SevenGaps.ZqShellBalanceBlocker

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker
   3
   4/-!
   5# Seven Gaps, P2.4: exact-shell phase-balance blocker
   6
   7This module attacks the phase obligation in
   8`ZqContinuumBlocker.OscillatoryTail` without assuming cancellation.
   9
  10The current carrier facts prove finite exact shells, positive class masses,
  11large shell mass, and one fixed-cap pairing witness. They do not provide a
  12substrate action that resolves phases inside every late shell. The theorems
  13below isolate that missing content.
  14
  15* `ShellAmplitudeVanishes` is the weakest shell-local necessary condition:
  16  every individual late exact-shell amplitude must tend to zero.
  17  `OscillatoryTail` implies it by taking one-shell blocks.
  18* `eventuallyZeroPhase_not_oscillatoryTail` proves that changing only
  19  finitely many shells cannot help. In particular, a finite-cap pairing
  20  certificate cannot imply the uniform tail condition.
  21* `shellConstant_not_oscillatoryTail` proves that any phase which is
  22  constant inside each shell fails, even if that shell phase varies
  23  arbitrarily with complexity. The norm of its shell amplitude is exactly
  24  the diverging positive shell mass.
  25
  26Thus the minimal missing P2.4 input is genuine asymptotic intra-shell
  27balance: at least `ShellAmplitudeVanishes`, and in fact the stronger uniform
  28contiguous-block control of `OscillatoryTail`. Neither relabeling invariance,
  29finite-cap pairing, nor a complexity-only phase supplies it.
  30
  31All limits here concern the complexity cutoff. They are not mesh refinement
  32and make no geometric-continuum claim. No full-theory flag is changed.
  33
  34No `sorry`, `admit`, new axiom, or `native_decide`.
  35-/
  36
  37namespace IndisputableMonolith
  38namespace Gravity
  39namespace SevenGaps
  40namespace ZqShellBalanceBlocker
  41
  42open ExactShellGaugeUV
  43open ZqContinuumBlocker
  44
  45noncomputable section
  46
  47/-! ## 1. The minimal shell-local necessary premise -/
  48
  49/-- The shell-local balance condition forced by any uniform oscillatory
  50tail: individual exact-shell amplitudes tend to zero. This condition is
  51necessary but does not by itself control accumulation over long blocks. -/
  52def ShellAmplitudeVanishes
  53    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
  54  ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
  55    ‖exactShellAmplitude phase n‖ < ε
  56
  57/-- A one-shell contiguous block is exactly its shell amplitude. -/
  58theorem one_shell_block
  59    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (n : ℕ) :
  60    ∑ k ∈ Finset.Ico n (n + 1), exactShellAmplitude phase k =
  61      exactShellAmplitude phase n := by
  62  rw [Finset.sum_Ico_eq_sub (exactShellAmplitude phase) (Nat.le_succ n),
  63    Finset.sum_range_succ, add_sub_cancel_left]
  64
  65/-- **NECESSARY BALANCE THEOREM.** Uniform late-block cancellation forces
  66the individual exact-shell amplitudes to vanish. -/
  67theorem oscillatoryTail_implies_shellAmplitudeVanishes
  68    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
  69    (htail : OscillatoryTail phase) :
  70    ShellAmplitudeVanishes phase := by
  71  intro ε hε
  72  obtain ⟨N, hN⟩ := htail ε hε
  73  refine ⟨N, fun n hn => ?_⟩
  74  have hsmall := hN n (n + 1) hn (Nat.le_succ n)
  75  rw [one_shell_block] at hsmall
  76  exact hsmall
  77
  78/-! ## 2. Finite-cap cancellation cannot imply the tail condition -/
  79
  80/-- Two exact-shell phases agree from some shell onward. -/
  81def EventuallyAgrees
  82    (phase ψ : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
  83  ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ c, phase n c = ψ n c
  84
  85/-- Exact shell amplitudes agree when all class phases agree on that shell. -/
  86theorem exactShellAmplitude_congr
  87    {phase ψ : ∀ n : ℕ, ExactPathClass n → ℝ} {n : ℕ}
  88    (h : ∀ c, phase n c = ψ n c) :
  89    exactShellAmplitude phase n = exactShellAmplitude ψ n := by
  90  unfold exactShellAmplitude
  91  refine Finset.sum_congr rfl fun c _ => ?_
  92  rw [h c]
  93
  94/-- One direction of tail transport along eventual phase agreement. -/
  95theorem oscillatoryTail_of_eventuallyAgrees
  96    {phase ψ : ∀ n : ℕ, ExactPathClass n → ℝ}
  97    (hagree : EventuallyAgrees phase ψ)
  98    (hphase : OscillatoryTail phase) : OscillatoryTail ψ := by
  99  obtain ⟨N₀, hN₀⟩ := hagree
 100  intro ε hε
 101  obtain ⟨N, hN⟩ := hphase ε hε
 102  refine ⟨max N N₀, fun m n hm hmn => ?_⟩
 103  have hmN : N ≤ m := le_trans (le_max_left N N₀) hm
 104  have hmN₀ : N₀ ≤ m := le_trans (le_max_right N N₀) hm
 105  have heq :
 106      ∑ k ∈ Finset.Ico m n, exactShellAmplitude ψ k =
 107        ∑ k ∈ Finset.Ico m n, exactShellAmplitude phase k := by
 108    refine Finset.sum_congr rfl fun k hk => ?_
 109    have hmk : m ≤ k := (Finset.mem_Ico.mp hk).1
 110    exact (exactShellAmplitude_congr
 111      (fun c => (hN₀ k (le_trans hmN₀ hmk) c).symm))
 112  rw [heq]
 113  exact hN m n hmN hmn
 114
 115/-- Eventual phase agreement preserves the uniform tail condition. -/
 116theorem oscillatoryTail_congr_eventually
 117    {phase ψ : ∀ n : ℕ, ExactPathClass n → ℝ}
 118    (hagree : EventuallyAgrees phase ψ) :
 119    OscillatoryTail phase ↔ OscillatoryTail ψ := by
 120  obtain ⟨N₀, hN₀⟩ := hagree
 121  constructor
 122  · exact oscillatoryTail_of_eventuallyAgrees ⟨N₀, hN₀⟩
 123  · exact oscillatoryTail_of_eventuallyAgrees
 124      ⟨N₀, fun n hn c => (hN₀ n hn c).symm⟩
 125
 126/-- A phase which differs from zero only on finitely many shells. This is
 127the exact abstract shape of any finite-cap phase repair. -/
 128def EventuallyZeroPhase
 129    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
 130  EventuallyAgrees phase zeroPhase
 131
 132/-- **FINITE-CAP NO-GO.** No phase modification supported on only finitely
 133many exact shells can satisfy the uniform oscillatory-tail condition. -/
 134theorem eventuallyZeroPhase_not_oscillatoryTail
 135    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
 136    (hzero : EventuallyZeroPhase phase) :
 137    ¬ OscillatoryTail phase := by
 138  intro htail
 139  have hz : OscillatoryTail zeroPhase :=
 140    (oscillatoryTail_congr_eventually hzero).mp htail
 141  exact zeroPhase_not_oscillatoryTail hz
 142
 143/-- A phase change confined below cap `B` agrees with zero on every shell
 144at or above `B`. -/
 145def SupportedBelow
 146    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) : Prop :=
 147  ∀ n : ℕ, B ≤ n → ∀ c, phase n c = 0
 148
 149/-- A fixed-cap cancellation witness cannot be promoted to a uniform tail
 150theorem merely by extending it by zero phase beyond the witnessed cap. -/
 151theorem supportedBelow_not_oscillatoryTail
 152    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ)
 153    (hsupp : SupportedBelow phase B) :
 154    ¬ OscillatoryTail phase :=
 155  eventuallyZeroPhase_not_oscillatoryTail phase
 156    ⟨B, fun n hn c => by
 157      rw [hsupp n hn c]
 158      rfl⟩
 159
 160/-! ## 3. Complexity-only phases cannot balance a shell -/
 161
 162/-- A phase is shell-constant when it does not distinguish classes inside
 163any exact complexity shell. It may still vary arbitrarily with `n`. -/
 164def ShellConstant
 165    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : Prop :=
 166  ∀ n : ℕ, ∀ c, phase n c = phase n (isolatedClass n)
 167
 168/-- For a shell-constant phase, the full shell amplitude is its positive
 169shell mass times one common unit phase. No intra-shell cancellation occurs. -/
 170theorem exactShellAmplitude_shellConstant
 171    {phase : ∀ n : ℕ, ExactPathClass n → ℝ}
 172    (hconst : ShellConstant phase) (n : ℕ) :
 173    exactShellAmplitude phase n =
 174      (shellMass n : ℂ) *
 175        Complex.exp (Complex.I * (phase n (isolatedClass n) : ℂ)) := by
 176  unfold exactShellAmplitude shellMass
 177  rw [Complex.ofReal_sum, Finset.sum_mul]
 178  refine Finset.sum_congr rfl fun c _ => ?_
 179  rw [hconst n c]
 180
 181/-- The norm of a shell-constant amplitude is exactly the shell mass. -/
 182theorem norm_exactShellAmplitude_shellConstant
 183    {phase : ∀ n : ℕ, ExactPathClass n → ℝ}
 184    (hconst : ShellConstant phase) (n : ℕ) :
 185    ‖exactShellAmplitude phase n‖ = shellMass n := by
 186  rw [exactShellAmplitude_shellConstant hconst n, norm_mul,
 187    Complex.norm_real, Real.norm_eq_abs, abs_of_pos (shellMass_pos n),
 188    Complex.norm_exp_I_mul_ofReal, mul_one]
 189
 190/-- Every shell of complexity at least two has mass strictly above one. -/
 191theorem one_lt_shellMass_of_two_le {n : ℕ} (hn : 2 ≤ n) :
 192    (1 : ℝ) < shellMass n := by
 193  have hpowN : n ≤ n ^ (3 * n) :=
 194    Nat.le_self_pow (by omega) n
 195  have hpowR : ((n : ℕ) : ℝ) ≤ ((n : ℕ) : ℝ) ^ (3 * n) := by
 196    calc
 197      ((n : ℕ) : ℝ) ≤ ((n ^ (3 * n) : ℕ) : ℝ) := by
 198        exact_mod_cast hpowN
 199      _ = ((n : ℕ) : ℝ) ^ (3 * n) := Nat.cast_pow n (3 * n)
 200  have hnR : (1 : ℝ) < (n : ℕ) := by
 201    exact_mod_cast (show 1 < n by omega)
 202  have hlower := RegulatorRemovalNoGo.shellMass_lower n
 203  linarith
 204
 205/-- A shell-constant phase fails even the weakest shell-local necessary
 206balance condition. -/
 207theorem shellConstant_not_shellAmplitudeVanishes
 208    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
 209    (hconst : ShellConstant phase) :
 210    ¬ ShellAmplitudeVanishes phase := by
 211  intro hv
 212  obtain ⟨N, hN⟩ := hv 1 one_pos
 213  let n : ℕ := max 2 N
 214  have hnN : N ≤ n := le_max_right 2 N
 215  have hn2 : 2 ≤ n := le_max_left 2 N
 216  have hsmall := hN n hnN
 217  rw [norm_exactShellAmplitude_shellConstant hconst n] at hsmall
 218  exact (not_lt_of_ge (one_lt_shellMass_of_two_le hn2).le) hsmall
 219
 220/-- **COMPLEXITY-PHASE NO-GO.** Any phase that only sees shell complexity
 221fails `OscillatoryTail`, regardless of how its common shell phase varies. -/
 222theorem shellConstant_not_oscillatoryTail
 223    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
 224    (hconst : ShellConstant phase) :
 225    ¬ OscillatoryTail phase := by
 226  intro htail
 227  exact shellConstant_not_shellAmplitudeVanishes phase hconst
 228    (oscillatoryTail_implies_shellAmplitudeVanishes phase htail)
 229
 230/-! ## 4. Certified P2.4 blocker package -/
 231
 232/-- The certified P2.4 blocker: uniform tails require shell-local
 233vanishing; finite-shell repairs and complexity-only phases cannot supply it.
 234The remaining premise is asymptotic intra-shell phase balance from richer
 235substrate structure. -/
 236theorem p24_shell_balance_blocker_certificate :
 237    (∀ phase : ∀ n : ℕ, ExactPathClass n → ℝ,
 238      OscillatoryTail phase → ShellAmplitudeVanishes phase) ∧
 239    (∀ phase : ∀ n : ℕ, ExactPathClass n → ℝ,
 240      EventuallyZeroPhase phase → ¬ OscillatoryTail phase) ∧
 241    (∀ phase : ∀ n : ℕ, ExactPathClass n → ℝ,
 242      ShellConstant phase → ¬ OscillatoryTail phase) :=
 243  ⟨oscillatoryTail_implies_shellAmplitudeVanishes,
 244    eventuallyZeroPhase_not_oscillatoryTail,
 245    shellConstant_not_oscillatoryTail⟩
 246
 247#print axioms oscillatoryTail_implies_shellAmplitudeVanishes
 248#print axioms eventuallyZeroPhase_not_oscillatoryTail
 249#print axioms supportedBelow_not_oscillatoryTail
 250#print axioms shellConstant_not_shellAmplitudeVanishes
 251#print axioms shellConstant_not_oscillatoryTail
 252#print axioms p24_shell_balance_blocker_certificate
 253
 254end
 255
 256end ZqShellBalanceBlocker
 257end SevenGaps
 258end Gravity
 259end IndisputableMonolith
 260