IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridge

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridge
   2
   3/-!
   4# Gap2 R4: antipodal mass-balance bridge (sufficiency half)
   5
   6Banks the mechanical sufficiency half of the antipodal weakening
   7(design `D-qg-gap2-r4-antipodal-design-20260723` /
   8`plans/QG_Gap2_R4_Antipodal_Design_20260723.html`):
   9
  10* `EventuallyTickFiberAntipodalMassBalanced`: equal `classMu` mass on
  11  opposite Fin-8 fibers `p` and `p+4` from some shell onward.
  12* Antipodal balance kills late shell amplitudes by pairwise cancellation
  13  (`tickRoot (p+4) = -tickRoot p`), with no rational-independence argument.
  14* Hence `OscillatoryTail` on the tick-derived phase (mirror of the full
  15  eventual-balance bridge in `Gap2TickPhaseTailBlocker`).
  16* `TailAntipodalShift`: mu-preserving tail automorphisms rotating tick
  17  by `+4`; implies antipodal balance (mirror of `TailFiberShift`).
  18* Weakening chain: `TailFiberShift → TailAntipodalShift` (compose `+1`
  19  four times) and full eventual balance → antipodal balance.
  20
  21## Status
  22
  23R4 stays OPEN (`TailAntipodalShift` uninhabited). Does NOT flip
  24`gap2_continuum_and_measure`. The converse (vanishing forces antipodal
  25balance via Q-independence of `1` and `√2` on rational masses) is
  26deliberately deferred. No `sorry`, `admit`, new axiom, or `native_decide`.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Gravity
  31namespace SevenGaps
  32namespace Gap2AntipodalBalanceBridge
  33
  34open ExactShellGaugeUV
  35open ZqContinuumBlocker
  36open Gap2TickPhaseSubstrate
  37open Gap2TickPhaseTailBlocker
  38open Gap2TailFiberShiftBridge
  39
  40noncomputable section
  41
  42/-! ## §1. Antipodal eventual mass balance -/
  43
  44/-- Honest weakening of eventual full Fin-8 balance: opposite fibers
  45`p` and `p+4` carry equal `classMu` mass from some shell onward. -/
  46def EventuallyTickFiberAntipodalMassBalanced
  47    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) : Prop :=
  48  ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
  49    ∀ p : Fin 8, tickFiberMass tau n p = tickFiberMass tau n (p + 4)
  50
  51/-- Full eventual balance specializes to antipodal balance. -/
  52theorem eventuallyTickFiberMassBalanced_implies_antipodal
  53    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8)
  54    (hbal : EventuallyTickFiberMassBalanced tau) :
  55    EventuallyTickFiberAntipodalMassBalanced tau := by
  56  obtain ⟨N, hN⟩ := hbal
  57  refine ⟨N, fun n hn p => hN n hn p (p + 4)⟩
  58
  59/-! ## §2. Root arithmetic: `tickRoot (p+4) = -tickRoot p` -/
  60
  61private lemma exp_two_pi_I_mul_nat (q : ℕ) :
  62    Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (q : ℂ)) = 1 := by
  63  -- In this Mathlib pin: `exp_nat_mul z q : exp (↑q * z) = exp z ^ q`.
  64  have hpow :
  65      Complex.exp ((q : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) =
  66        Complex.exp (2 * (Real.pi : ℂ) * Complex.I) ^ q :=
  67    Complex.exp_nat_mul (2 * (Real.pi : ℂ) * Complex.I) q
  68  have hcomm :
  69      (q : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) =
  70        2 * (Real.pi : ℂ) * Complex.I * (q : ℂ) := by
  71    ring
  72  calc
  73    Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (q : ℂ))
  74        = Complex.exp ((q : ℂ) * (2 * (Real.pi : ℂ) * Complex.I)) := by
  75          rw [hcomm]
  76      _ = Complex.exp (2 * (Real.pi : ℂ) * Complex.I) ^ q := hpow
  77      _ = (1 : ℂ) ^ q := by rw [Complex.exp_two_pi_mul_I]
  78      _ = 1 := one_pow q
  79
  80private lemma exp_eighth_period (n : ℕ) :
  81    Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (n : ℂ) / 8) =
  82      Complex.exp (2 * (Real.pi : ℂ) * Complex.I * ((n % 8 : ℕ) : ℂ) / 8) := by
  83  have hn : n = 8 * (n / 8) + n % 8 := (Nat.div_add_mod n 8).symm
  84  have harg :
  85      (2 * (Real.pi : ℂ) * Complex.I * (n : ℂ) / 8) =
  86        2 * (Real.pi : ℂ) * Complex.I * ((n / 8 : ℕ) : ℂ) +
  87          2 * (Real.pi : ℂ) * Complex.I * ((n % 8 : ℕ) : ℂ) / 8 := by
  88    have hnC : (n : ℂ) = ((8 * (n / 8) + n % 8 : ℕ) : ℂ) := by
  89      exact congrArg Nat.cast hn
  90    rw [hnC]
  91    push_cast
  92    ring
  93  calc
  94    Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (n : ℂ) / 8)
  95        = Complex.exp
  96            (2 * (Real.pi : ℂ) * Complex.I * ((n / 8 : ℕ) : ℂ) +
  97              2 * (Real.pi : ℂ) * Complex.I * ((n % 8 : ℕ) : ℂ) / 8) := by
  98          rw [harg]
  99      _ = Complex.exp (2 * (Real.pi : ℂ) * Complex.I * ((n / 8 : ℕ) : ℂ)) *
 100            Complex.exp
 101              (2 * (Real.pi : ℂ) * Complex.I * ((n % 8 : ℕ) : ℂ) / 8) :=
 102          Complex.exp_add _ _
 103      _ = 1 *
 104            Complex.exp
 105              (2 * (Real.pi : ℂ) * Complex.I * ((n % 8 : ℕ) : ℂ) / 8) := by
 106          rw [exp_two_pi_I_mul_nat]
 107      _ = Complex.exp
 108            (2 * (Real.pi : ℂ) * Complex.I * ((n % 8 : ℕ) : ℂ) / 8) := by
 109          ring
 110
 111/-- Opposite 8th-root characters negate: `ω^{p+4} = -ω^p`. -/
 112theorem tickRoot_add_four (p : Fin 8) : tickRoot (p + 4) = -tickRoot p := by
 113  unfold tickRoot
 114  have hval : ((p + 4 : Fin 8) : ℕ) = (p.val + 4) % 8 := by
 115    rw [Fin.val_add]
 116    rfl
 117  rw [hval, ← exp_eighth_period (p.val + 4)]
 118  have hsplit :
 119      Complex.exp
 120          (2 * (Real.pi : ℂ) * Complex.I * ((p.val + 4 : ℕ) : ℂ) / 8) =
 121        Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (p.val : ℂ) / 8) *
 122          Complex.exp ((Real.pi : ℂ) * Complex.I) := by
 123    rw [← Complex.exp_add]
 124    congr 1
 125    push_cast
 126    ring
 127  rw [hsplit, Complex.exp_pi_mul_I, mul_neg_one]
 128
 129/-! ## §3. Antipodal balance ⇒ vanishing shell amplitudes -/
 130
 131private lemma antipodal_pair_term_eq_zero
 132    (m : Fin 8 → ℝ) (p : Fin 8)
 133    (hm : m p = m (p + 4)) :
 134    (m p : ℂ) * tickRoot p + (m (p + 4) : ℂ) * tickRoot (p + 4) = 0 := by
 135  rw [hm, tickRoot_add_four]
 136  ring
 137
 138private lemma sum_fin8_antipodal_cancel (f : Fin 8 → ℂ)
 139    (h : ∀ p : Fin 8, f p + f (p + 4) = 0) :
 140    ∑ p : Fin 8, f p = 0 := by
 141  have h0 := h 0
 142  have h1 := h 1
 143  have h2 := h 2
 144  have h3 := h 3
 145  have e0 : (0 : Fin 8) + 4 = 4 := rfl
 146  have e1 : (1 : Fin 8) + 4 = 5 := rfl
 147  have e2 : (2 : Fin 8) + 4 = 6 := rfl
 148  have e3 : (3 : Fin 8) + 4 = 7 := rfl
 149  simp only [Fin.sum_univ_eight, e0, e1, e2, e3] at h0 h1 h2 h3 ⊢
 150  linear_combination h0 + h1 + h2 + h3
 151
 152/-- **THEOREM.** Antipodal fiber-mass balance at shell `n` forces
 153`exactShellAmplitude (tickDerivedPhase tau) n = 0` by four opposite-root
 154cancellations. No Q-independence. -/
 155theorem exactShellAmplitude_eq_zero_of_antipodalBalanced_at
 156    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (n : ℕ)
 157    (hbal : ∀ p : Fin 8, tickFiberMass tau n p = tickFiberMass tau n (p + 4)) :
 158    exactShellAmplitude (tickDerivedPhase tau) n = 0 := by
 159  rw [exactShellAmplitude_tick_fiberwise]
 160  refine sum_fin8_antipodal_cancel
 161    (fun p => (tickFiberMass tau n p : ℂ) * tickRoot p) fun p => ?_
 162  simpa using antipodal_pair_term_eq_zero (tickFiberMass tau n) p (hbal p)
 163
 164private theorem sum_amp_eq_zero_of_amps_zero
 165    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
 166    {s : Finset ℕ}
 167    (h : ∀ k ∈ s, exactShellAmplitude phase k = 0) :
 168    ∑ k ∈ s, exactShellAmplitude phase k = 0 :=
 169  Finset.sum_eq_zero h
 170
 171/-- **THEOREM.** Eventual antipodal balance ⇒ `OscillatoryTail` on the
 172tick-derived phase (finite head irrelevant). -/
 173theorem eventuallyAntipodalBalanced_implies_oscillatoryTail
 174    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8)
 175    (hbal : EventuallyTickFiberAntipodalMassBalanced tau) :
 176    OscillatoryTail (tickDerivedPhase tau) := by
 177  obtain ⟨N, hN⟩ := hbal
 178  intro ε hε
 179  refine ⟨N, fun m n hm _hmn => ?_⟩
 180  have hamp :
 181      ∀ k ∈ Finset.Ico m n,
 182        exactShellAmplitude (tickDerivedPhase tau) k = 0 := by
 183    intro k hk
 184    have hkN : N ≤ k := le_trans hm (Finset.mem_Ico.mp hk).1
 185    exact exactShellAmplitude_eq_zero_of_antipodalBalanced_at tau k (hN k hkN)
 186  rw [sum_amp_eq_zero_of_amps_zero _ hamp, norm_zero]
 187  exact hε
 188
 189/-! ## §4. Conditional structure: `TailAntipodalShift` -/
 190
 191/-- **CONDITIONAL hyp.** From some shell `N` onward, a family of
 192exact-path-class automorphisms that rotate the tick by `+4` and preserve
 193`classMu`. Same shape as `TailFiberShift` with antipodal step. Not
 194inhabited in this module. -/
 195structure TailAntipodalShift (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) where
 196  N : ℕ
 197  shift : ∀ n : ℕ, N ≤ n → ExactPathClass n ≃ ExactPathClass n
 198  tick_shift :
 199    ∀ n : ℕ, ∀ hn : N ≤ n, ∀ c : ExactPathClass n,
 200      tau n (shift n hn c) = tau n c + 4
 201  mu_shift :
 202    ∀ n : ℕ, ∀ hn : N ≤ n, ∀ c : ExactPathClass n,
 203      classMu (shift n hn c) = classMu c
 204
 205/-- The antipodal shift restricts to a `classMu`-preserving bijection of
 206tick fibers `p → p+4`. -/
 207theorem tickFiberMass_add_four_of_tailAntipodalShift
 208    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailAntipodalShift tau)
 209    {n : ℕ} (hn : h.N ≤ n) (p : Fin 8) :
 210    tickFiberMass tau n p = tickFiberMass tau n (p + 4) := by
 211  classical
 212  let e := h.shift n hn
 213  have hmap :
 214      (tickFiber tau n p).map e.toEmbedding = tickFiber tau n (p + 4) := by
 215    ext d
 216    simp only [tickFiber, Finset.mem_map, Finset.mem_filter, Finset.mem_univ,
 217      true_and, Equiv.coe_toEmbedding]
 218    constructor
 219    · rintro ⟨c, hc, rfl⟩
 220      rw [h.tick_shift n hn c, hc]
 221    · intro hd
 222      refine ⟨e.symm d, ?_, e.apply_symm_apply d⟩
 223      have htick := h.tick_shift n hn (e.symm d)
 224      rw [e.apply_symm_apply] at htick
 225      have : tau n (e.symm d) + 4 = p + 4 := htick.symm.trans hd
 226      exact add_right_cancel this
 227  unfold tickFiberMass
 228  rw [← hmap, Finset.sum_map]
 229  refine Finset.sum_congr rfl fun c _ => (h.mu_shift n hn c).symm
 230
 231/-- **BRIDGE.** A `TailAntipodalShift` forces eventual antipodal
 232fiber-mass balance. -/
 233theorem eventuallyTickFiberAntipodalMassBalanced_of_tailAntipodalShift
 234    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailAntipodalShift tau) :
 235    EventuallyTickFiberAntipodalMassBalanced tau := by
 236  refine ⟨h.N, fun n hn p =>
 237    tickFiberMass_add_four_of_tailAntipodalShift tau h hn p⟩
 238
 239/-- Abstract composition: antipodal shift ⇒ `OscillatoryTail`. -/
 240theorem oscillatoryTail_of_tailAntipodalShift
 241    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailAntipodalShift tau) :
 242    OscillatoryTail (tickDerivedPhase tau) :=
 243  eventuallyAntipodalBalanced_implies_oscillatoryTail tau
 244    (eventuallyTickFiberAntipodalMassBalanced_of_tailAntipodalShift tau h)
 245
 246/-! ## §5. Old target is strictly stronger: compose `+1` four times -/
 247
 248private def equivIterate4 {α : Type*} (e : α ≃ α) : α ≃ α :=
 249  e.trans (e.trans (e.trans e))
 250
 251private lemma tick_shift_four
 252    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8)
 253    {n : ℕ} (e : ExactPathClass n ≃ ExactPathClass n)
 254    (htick : ∀ c : ExactPathClass n, tau n (e c) = tau n c + 1)
 255    (c : ExactPathClass n) :
 256    tau n (equivIterate4 e c) = tau n c + 4 := by
 257  have h1 : tau n (e c) = tau n c + 1 := htick c
 258  have h2 : tau n (e (e c)) = tau n (e c) + 1 := htick (e c)
 259  have h3 : tau n (e (e (e c))) = tau n (e (e c)) + 1 := htick (e (e c))
 260  have h4 : tau n (e (e (e (e c)))) = tau n (e (e (e c))) + 1 :=
 261    htick (e (e (e c)))
 262  change tau n (e (e (e (e c)))) = tau n c + 4
 263  calc tau n (e (e (e (e c))))
 264      = tau n (e (e (e c))) + 1 := h4
 265    _ = tau n (e (e c)) + 1 + 1 := by rw [h3]
 266    _ = tau n (e c) + 1 + 1 + 1 := by rw [h2]
 267    _ = tau n c + 1 + 1 + 1 + 1 := by rw [h1]
 268    _ = tau n c + 4 := by
 269        ext
 270        simp only [Fin.val_add]
 271        omega
 272
 273private lemma mu_shift_four
 274    {n : ℕ} (e : ExactPathClass n ≃ ExactPathClass n)
 275    (hmu : ∀ c : ExactPathClass n, classMu (e c) = classMu c)
 276    (c : ExactPathClass n) :
 277    classMu (equivIterate4 e c) = classMu c := by
 278  change classMu (e (e (e (e c)))) = classMu c
 279  simp only [hmu]
 280
 281/-- **THEOREM.** The old `+1` free-action target is strictly stronger:
 282four compositions yield an antipodal `+4` shift. -/
 283theorem nonempty_tailAntipodalShift_of_tailFiberShift
 284    (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailFiberShift tau) :
 285    Nonempty (TailAntipodalShift tau) := by
 286  refine ⟨{
 287    N := h.N
 288    shift := fun n hn => equivIterate4 (h.shift n hn)
 289    tick_shift := fun n hn c =>
 290      tick_shift_four tau (h.shift n hn) (h.tick_shift n hn) c
 291    mu_shift := fun n hn c =>
 292      mu_shift_four (h.shift n hn) (h.mu_shift n hn) c
 293  }⟩
 294
 295/-! ## §6. Status (R4 open; gap2 unflipped) -/
 296
 297structure Gap2AntipodalBalanceBridgeStatus where
 298  antipodalAmplitudeBridgeLanded : Bool
 299  antipodalOscillatoryTailBridgeLanded : Bool
 300  tailAntipodalShiftBridgeLanded : Bool
 301  fiberShiftImpliesAntipodalLanded : Bool
 302  fullBalanceImpliesAntipodalLanded : Bool
 303  tailAntipodalShiftInhabited : Bool
 304  r4ResidualOpen : Bool
 305  gap2ContinuumAndMeasure : Bool
 306
 307def gap2AntipodalBalanceBridgeStatus : Gap2AntipodalBalanceBridgeStatus where
 308  antipodalAmplitudeBridgeLanded := true
 309  antipodalOscillatoryTailBridgeLanded := true
 310  tailAntipodalShiftBridgeLanded := true
 311  fiberShiftImpliesAntipodalLanded := true
 312  fullBalanceImpliesAntipodalLanded := true
 313  tailAntipodalShiftInhabited := false
 314  r4ResidualOpen := true
 315  gap2ContinuumAndMeasure := false
 316
 317theorem gap2AntipodalBalanceBridgeStatus_flags :
 318    gap2AntipodalBalanceBridgeStatus.antipodalAmplitudeBridgeLanded = true ∧
 319      gap2AntipodalBalanceBridgeStatus.antipodalOscillatoryTailBridgeLanded =
 320        true ∧
 321      gap2AntipodalBalanceBridgeStatus.tailAntipodalShiftBridgeLanded = true ∧
 322      gap2AntipodalBalanceBridgeStatus.fiberShiftImpliesAntipodalLanded =
 323        true ∧
 324      gap2AntipodalBalanceBridgeStatus.fullBalanceImpliesAntipodalLanded =
 325        true ∧
 326      gap2AntipodalBalanceBridgeStatus.tailAntipodalShiftInhabited = false ∧
 327      gap2AntipodalBalanceBridgeStatus.r4ResidualOpen = true ∧
 328      gap2AntipodalBalanceBridgeStatus.gap2ContinuumAndMeasure = false := by
 329  decide
 330
 331end
 332
 333end Gap2AntipodalBalanceBridge
 334end SevenGaps
 335end Gravity
 336end IndisputableMonolith
 337