IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlocker

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseSubstrate
   2
   3/-!
   4# Wave C1 R4 hardening: tick-phase tail blocker / eventual-balance repair
   5
   6Hardens the R4 residual named in
   7`plans/QG_WaveC1_Gap2_Residual_DAG_Draft_20260722.txt` after the
   8cross-family design correction to the R2 receipt:
   9
  10* (a) Generic bridge: all-shell `TickFiberMassBalanced` makes every
  11  `exactShellAmplitude` identically zero, so contiguous-block sums vanish
  12  and yield `ExactShellTailCancellation` / `OscillatoryTail`.
  13* (b) Finite-head impossibility: shell `0` is a singleton class, so
  14  `classMu`-mass concentrates in one tick fiber for every `tau`;
  15  therefore `¬ ∃ tau, TickFiberMassBalanced tau`.
  16* (c) Eventual-balance repair: `EventuallyTickFiberMassBalanced` kills all
  17  late amplitudes; the finite head is irrelevant to `OscillatoryTail`.
  18* (d) Signature-level blocker target `SignatureFin8OscillatoryTailBlocker`
  19  (defined; neither proved nor assumed).
  20
  21## Divergence from the R2 receipt assessment
  22
  23The R2 module docstring claimed per-shell equidistribution /
  24`ShellAmplitudeVanishes` is insufficient for contiguous-block
  25cancellation. That is true for the *asymptotic* form of
  26`ShellAmplitudeVanishes` (late shells merely small). It is false for
  27*identically zero* amplitudes: under all-shell mass balance every shell
  28amplitude is definitionally zero, so every contiguous block sum is zero.
  29No extra estimate is required for the lift.
  30
  31## What stays OPEN
  32
  33The R4 residual itself: existence of a substrate phase (escaping the
  34dead classes) with `OscillatoryTail`. The sharper terminal candidate
  35`SignatureFin8OscillatoryTailBlocker` is defined here but not proved.
  36
  37Does NOT flip `gap2_continuum_and_measure`. No `sorry`, `admit`, new
  38axiom, or `native_decide`.
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Gravity
  43namespace SevenGaps
  44namespace Gap2TickPhaseTailBlocker
  45
  46open ExactShellGaugeUV
  47open ZqContinuumBlocker
  48open Gap2TickPhaseSubstrate
  49
  50noncomputable section
  51
  52/-! ## §1. Shell-0 singleton (finite-head geometry) -/
  53
  54private theorem shellSig_zero_eq (s : ShellSig 0) : s = isolatedSig 0 := by
  55  apply Subtype.ext
  56  apply Prod.ext
  57  · exact Fin.eq_zero _
  58  · apply Prod.ext <;> exact Fin.eq_zero _
  59
  60private theorem exactComplex_zero_eq (K : ExactComplex 0 0 0) :
  61    K = isolatedVertices 0 := by
  62  cases K with | mk e t =>
  63  have he : e = (isolatedVertices 0).edgeVerts := funext fun i => i.elim0
  64  have ht : t = (isolatedVertices 0).tetVerts := funext fun i => i.elim0
  65  rw [he, ht]
  66
  67/-- Every class at shell `0` equals the unique empty-complex class. -/
  68theorem exactPathClass_zero_eq (c : ExactPathClass 0) : c = isolatedClass 0 := by
  69  cases c with | mk s q =>
  70  have hs : s = isolatedSig 0 := shellSig_zero_eq s
  71  subst hs
  72  refine Sigma.ext rfl ?_
  73  simp only [heq_eq_eq]
  74  refine Quotient.inductionOn q fun K => ?_
  75  rw [exactComplex_zero_eq K]
  76  rfl
  77
  78/-- **Finite-head fact.** The exact complexity shell at level `0` is a
  79singleton: only the empty signature `(0,0,0)` and its unique class. -/
  80theorem exactPathClass_zero_subsingleton : Subsingleton (ExactPathClass 0) :=
  81  ⟨fun a b => by rw [exactPathClass_zero_eq a, exactPathClass_zero_eq b]⟩
  82
  83private theorem finset_univ_exactPathClass_zero :
  84    (Finset.univ : Finset (ExactPathClass 0)) = {isolatedClass 0} := by
  85  ext c
  86  simp only [Finset.mem_univ, Finset.mem_singleton, true_iff]
  87  exact exactPathClass_zero_eq c
  88
  89/-- For any tick assignment, shell-0 `classMu` mass sits in exactly one
  90tick fiber (the tick of the unique class); the other seven fibers are empty. -/
  91theorem tickFiberMass_shell_zero
  92    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (p : Fin 8) :
  93    tickFiberMass tau 0 p =
  94      if tau 0 (isolatedClass 0) = p then classMu (isolatedClass 0) else 0 := by
  95  unfold tickFiberMass tickFiber
  96  rw [finset_univ_exactPathClass_zero, Finset.filter_singleton]
  97  split_ifs with h
  98  · simp
  99  · simp
 100
 101/-- Design-named packaging of the shell-0 degeneracy used by the
 102all-shell balance impossibility. -/
 103theorem exactPathClass_zero_subsingleton_or_the_precise_finite_head_fact :
 104    Subsingleton (ExactPathClass 0) ∧
 105      ∀ tau : ∀ n : ℕ, ExactPathClass n → Fin 8,
 106        ∃ p : Fin 8,
 107          tickFiberMass tau 0 p = classMu (isolatedClass 0) ∧
 108            ∀ q : Fin 8, q ≠ p → tickFiberMass tau 0 q = 0 := by
 109  refine ⟨exactPathClass_zero_subsingleton, fun tau => ?_⟩
 110  refine ⟨tau 0 (isolatedClass 0), ?_, ?_⟩
 111  · simp [tickFiberMass_shell_zero]
 112  · intro q hq
 113    rw [tickFiberMass_shell_zero]
 114    simp [show tau 0 (isolatedClass 0) ≠ q from Ne.symm hq]
 115
 116private lemma fin8_add_one_ne (p : Fin 8) : p + 1 ≠ p := by
 117  intro h
 118  have hv := congrArg Fin.val h
 119  have hp : p.val < 8 := p.isLt
 120  simp only [Fin.val_add] at hv
 121  have : (p.val + 1) % 8 ≠ p.val := by omega
 122  exact this hv
 123
 124/-- **THEOREM.** No Fin-8 tick assignment is mass-balanced on every shell.
 125Cause: shell `0` concentrates all positive `classMu` mass in a single fiber. -/
 126theorem no_tickFiberMassBalanced :
 127    ¬ ∃ tau : ∀ n : ℕ, ExactPathClass n → Fin 8, TickFiberMassBalanced tau := by
 128  rintro ⟨tau, hbal⟩
 129  let p : Fin 8 := tau 0 (isolatedClass 0)
 130  let q : Fin 8 := p + 1
 131  have hpq : p ≠ q := (fin8_add_one_ne p).symm
 132  have hm_p : tickFiberMass tau 0 p = classMu (isolatedClass 0) := by
 133    simp [tickFiberMass_shell_zero, p]
 134  have hm_q : tickFiberMass tau 0 q = 0 := by
 135    have hne : tau 0 (isolatedClass 0) ≠ q := hpq
 136    rw [tickFiberMass_shell_zero]
 137    simp [hne]
 138  have heq := hbal 0 p q
 139  rw [hm_p, hm_q] at heq
 140  exact (ne_of_gt (classMu_pos (isolatedClass 0))) heq
 141
 142/-! ## §2. Generic bridge: balance ⇒ identical zero amplitudes ⇒ cancellation -/
 143
 144/-- Per-shell form of the root-of-unity cancellation (no all-shell hyp). -/
 145theorem exactShellAmplitude_eq_zero_of_massBalanced_at
 146    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (n : ℕ)
 147    (hbal : ∀ p q : Fin 8, tickFiberMass tau n p = tickFiberMass tau n q) :
 148    exactShellAmplitude (tickDerivedPhase tau) n = 0 := by
 149  rw [exactShellAmplitude_tick_fiberwise]
 150  have hconst : ∀ p : Fin 8, tickFiberMass tau n p = tickFiberMass tau n 0 :=
 151    fun p => hbal p 0
 152  calc ∑ p : Fin 8, (tickFiberMass tau n p : ℂ) * tickRoot p
 153      = ∑ p : Fin 8, (tickFiberMass tau n 0 : ℂ) * tickRoot p := by
 154        refine Finset.sum_congr rfl fun p _ => ?_
 155        rw [hconst p]
 156    _ = (tickFiberMass tau n 0 : ℂ) * ∑ p : Fin 8, tickRoot p := by
 157        rw [Finset.mul_sum]
 158    _ = (tickFiberMass tau n 0 : ℂ) * 0 := by rw [sum_tickRoots_eq_zero]
 159    _ = 0 := by ring
 160
 161private theorem sum_amp_eq_zero_of_amps_zero
 162    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
 163    {s : Finset ℕ}
 164    (h : ∀ k ∈ s, exactShellAmplitude phase k = 0) :
 165    ∑ k ∈ s, exactShellAmplitude phase k = 0 :=
 166  Finset.sum_eq_zero h
 167
 168/-- **BRIDGE (generic).** All-shell tick-fiber mass balance forces every
 169exact-shell amplitude to vanish identically; contiguous late-block sums of
 170zeros are zero, hence `ExactShellTailCancellation`. No extra estimate. -/
 171theorem tickFiberMassBalanced_implies_exactShellTailCancellation
 172    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8)
 173    (hbal : TickFiberMassBalanced tau) :
 174    ExactShellTailCancellation (tickDerivedPhase tau) := by
 175  intro ε hε
 176  refine ⟨0, fun m n _hm _hmn => ?_⟩
 177  have hamp :
 178      ∀ k ∈ Finset.Ico (m + 1) (n + 1),
 179        exactShellAmplitude (tickDerivedPhase tau) k = 0 :=
 180    fun k _ => exactShellAmplitude_eq_zero_of_massBalanced tau hbal k
 181  rw [sum_amp_eq_zero_of_amps_zero _ hamp, norm_zero]
 182  exact hε
 183
 184/-- Same bridge for the panel-locked `OscillatoryTail` indexing
 185(`Ico m n` rather than ordered `Ico (m+1) (n+1)`). -/
 186theorem tickFiberMassBalanced_implies_oscillatoryTail
 187    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8)
 188    (hbal : TickFiberMassBalanced tau) :
 189    OscillatoryTail (tickDerivedPhase tau) := by
 190  intro ε hε
 191  refine ⟨0, fun m n _hm _hmn => ?_⟩
 192  have hamp :
 193      ∀ k ∈ Finset.Ico m n,
 194        exactShellAmplitude (tickDerivedPhase tau) k = 0 :=
 195    fun k _ => exactShellAmplitude_eq_zero_of_massBalanced tau hbal k
 196  rw [sum_amp_eq_zero_of_amps_zero _ hamp, norm_zero]
 197  exact hε
 198
 199/-- Identically-zero amplitudes lift to full `ExactShellTailCancellation`
 200(the honest extra hypothesis beyond the asymptotic vanishing Prop). -/
 201theorem exactShellTailCancellation_of_identically_zero_amplitudes
 202    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
 203    (hzero : ∀ n : ℕ, exactShellAmplitude phase n = 0) :
 204    ExactShellTailCancellation phase := by
 205  intro ε hε
 206  refine ⟨0, fun m n _hm _hmn => ?_⟩
 207  have hamp :
 208      ∀ k ∈ Finset.Ico (m + 1) (n + 1), exactShellAmplitude phase k = 0 :=
 209    fun k _ => hzero k
 210  rw [sum_amp_eq_zero_of_amps_zero _ hamp, norm_zero]
 211  exact hε
 212
 213/-! ## §3. Eventual (tail) balance repair -/
 214
 215/-- Honest credit-bearing repair of all-shell balance: equal fiber mass
 216from some shell onward. The finite head may be unbalanced. -/
 217def EventuallyTickFiberMassBalanced
 218    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) : Prop :=
 219  ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
 220    ∀ p q : Fin 8, tickFiberMass tau n p = tickFiberMass tau n q
 221
 222/-- **THEOREM.** Eventual mass balance kills every late shell amplitude;
 223`OscillatoryTail` only constrains late contiguous blocks, so the finite
 224head is irrelevant. -/
 225theorem eventuallyTickFiberMassBalanced_implies_oscillatoryTail
 226    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8)
 227    (hbal : EventuallyTickFiberMassBalanced tau) :
 228    OscillatoryTail (tickDerivedPhase tau) := by
 229  obtain ⟨N, hN⟩ := hbal
 230  intro ε hε
 231  refine ⟨N, fun m n hm _hmn => ?_⟩
 232  have hamp :
 233      ∀ k ∈ Finset.Ico m n,
 234        exactShellAmplitude (tickDerivedPhase tau) k = 0 := by
 235    intro k hk
 236    have hkN : N ≤ k :=
 237      le_trans hm (Finset.mem_Ico.mp hk).1
 238    exact exactShellAmplitude_eq_zero_of_massBalanced_at tau k (hN k hkN)
 239  rw [sum_amp_eq_zero_of_amps_zero _ hamp, norm_zero]
 240  exact hε
 241
 242theorem eventuallyTickFiberMassBalanced_implies_exactShellTailCancellation
 243    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8)
 244    (hbal : EventuallyTickFiberMassBalanced tau) :
 245    ExactShellTailCancellation (tickDerivedPhase tau) := by
 246  obtain ⟨N, hN⟩ := hbal
 247  intro ε hε
 248  refine ⟨N, fun m n hm _hmn => ?_⟩
 249  have hamp :
 250      ∀ k ∈ Finset.Ico (m + 1) (n + 1),
 251        exactShellAmplitude (tickDerivedPhase tau) k = 0 := by
 252    intro k hk
 253    have hk_ge : m + 1 ≤ k := (Finset.mem_Ico.mp hk).1
 254    have hkN : N ≤ k := le_trans (Nat.le_succ_of_le hm) hk_ge
 255    exact exactShellAmplitude_eq_zero_of_massBalanced_at tau k (hN k hkN)
 256  rw [sum_amp_eq_zero_of_amps_zero _ hamp, norm_zero]
 257  exact hε
 258
 259/-! ## §4. Signature-level tick class and blocker target -/
 260
 261/-- Tick assignments that factor through the shell signature
 262`(v,e,t)` (no quotient-internal incidence data). -/
 263def ShellSigTick (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) : Prop :=
 264  ∃ sigma : ∀ n : ℕ, ShellSig n → Fin 8,
 265    ∀ n : ℕ, ∀ c : ExactPathClass n, tau n c = sigma n c.1
 266
 267/-- **DEFINED, neither proved nor assumed.** Sharpened R4 terminal
 268candidate: no signature-factoring Fin-8 tick yields
 269`OscillatoryTail` on the derived phase.
 270
 271Honest status: this Prop is stated precisely as the credit-bearing
 272blocker target. Proving it needs the fiber-mass computation for all
 273signature ticks (a separate campaign). It is not assumed anywhere in
 274this module, and the R4 residual (a substrate phase with
 275`OscillatoryTail`) remains OPEN. -/
 276def SignatureFin8OscillatoryTailBlocker : Prop :=
 277  ¬ ∃ tau : ∀ n : ℕ, ExactPathClass n → Fin 8,
 278      ShellSigTick tau ∧ OscillatoryTail (tickDerivedPhase tau)
 279
 280/-! ## §5. Status (no continuum flip) -/
 281
 282structure Gap2TickPhaseTailBlockerStatus where
 283  allShellBalanceImpossible : Bool
 284  eventualBalanceBridgeLanded : Bool
 285  signatureBlockerDefinedUnproved : Bool
 286  r4ResidualOpen : Bool
 287  gap2ContinuumAndMeasure : Bool
 288
 289def gap2TickPhaseTailBlockerStatus : Gap2TickPhaseTailBlockerStatus where
 290  allShellBalanceImpossible := true
 291  eventualBalanceBridgeLanded := true
 292  signatureBlockerDefinedUnproved := true
 293  r4ResidualOpen := true
 294  gap2ContinuumAndMeasure := false
 295
 296theorem gap2TickPhaseTailBlockerStatus_flags :
 297    gap2TickPhaseTailBlockerStatus.allShellBalanceImpossible = true ∧
 298      gap2TickPhaseTailBlockerStatus.eventualBalanceBridgeLanded = true ∧
 299      gap2TickPhaseTailBlockerStatus.signatureBlockerDefinedUnproved = true ∧
 300      gap2TickPhaseTailBlockerStatus.r4ResidualOpen = true ∧
 301      gap2TickPhaseTailBlockerStatus.gap2ContinuumAndMeasure = false := by
 302  decide
 303
 304end
 305
 306end Gap2TickPhaseTailBlocker
 307end SevenGaps
 308end Gravity
 309end IndisputableMonolith
 310