IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   3
   4/-!
   5# The continuum transverse-traceless second variation of `∫ R √g` (4D, derived)
   6
   7Arc 2, step 7.  This module derives, from the Levi-Civita connection and
   8nothing else, the number that the Einstein-Hilbert action puts on a real
   9transverse-traceless plane wave, in the *same convention* the banked Regge
  10midpoint dictionary uses.
  11
  12## Why this module exists
  13
  14`ReggeExactFlatHessianNormGate4D` bridges the computed `-(1/8)` and the frozen
  15preflight `-(1/4)` with `discreteBookkeepingFactor := 2`, a definition with no
  16derivation.  Step 6 refuted the cheap explanation (that the 2 is the Frobenius
  17square of `axisTTPlus`) by reading both sides at a normalized polarization.  So
  18the honest move is to derive the continuum side independently and see which
  19number appears.
  20
  21## Non-circularity is structural, not promised
  22
  23This module imports `Mathlib` and `EdgeTTDecomposition4D` (linear algebra only,
  24itself importing nothing but `Mathlib`).  It does **not** import the coupling
  25table, the Bloch symbol, the norm gate, the preflight, or any existing
  26coefficient in the tree.  Nothing here can have read the answer.  The
  27comparison against the dictionary lives in the separate module
  28`ReggeNormalizationDerived4D`.
  29
  30## Conventions, matched to the discrete side by reading it first
  31
  32The discrete symbol (`ReggeExactFlatHessianBlochSymbol4D`, generated by
  33`scripts/qg/regge_4d_exact_m2_table_20260721.py`) is the unit-cell average of
  34`d²/dt²` of the Regge action under the **real** perturbation
  35`h(x) = H cos(k·x)`; the explicit `1/2` in its `couplingWeight` is the lattice
  36average of `cos(k·m_e) cos(k·m_e')`, which the generator states as
  37"real-cos = (1/2) Re(complex)".  So the object derived here is the phase
  38average of `d²/dt² ∫ R √g` per unit volume under the same real cosine wave,
  39and *not* the quadratic Taylor coefficient, which would differ by a further 2.
  40
  41## Named classical inputs
  42
  43* **A1** linearized Christoffel symbol `Γ⁽¹⁾_{λμν} = ½(∂_μ h_{λν} + ∂_ν h_{λμ}
  44  - ∂_λ h_{μν})`, the Levi-Civita connection linearized.  `linChristoffel`.
  45* **A2** `R⁽¹⁾_{μν} = ∂_λ Γ⁽¹⁾^λ_{μν} - ∂_ν Γ⁽¹⁾^λ_{μλ}`; the `ΓΓ` terms of the
  46  Ricci contraction are second order in `h` and drop.  `linRicci`.
  47* **A3** `d²/dt² ∫√g R = -∫ h_{μν} G⁽¹⁾^{μν}`, from Euler's theorem for a
  48  quadratic form together with `δ(√g R)/δg_{μν} = -√g G^{μν}`, flat space being
  49  a solution so the linear term vanishes.  `ehSecondVariationDensity`.
  50
  51A1 and A2 are formalized here as definitions of the standard objects and every
  52derivative in them is *proved*, not asserted.  A3 fixes the normalization of the
  53density and is stated as such.  The fourth input, Regge's own normalization
  54`Σ_h A_h δ_h = ½ ∫ R √g`, belongs to the comparison and lives in
  55`ReggeNormalizationDerived4D`.
  56
  57Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  58-/
  59
  60namespace IndisputableMonolith
  61namespace Gravity
  62namespace Analysis
  63namespace ContinuumTTSecondVariation4D
  64
  65open BigOperators
  66open EdgeTTDecomposition4D
  67
  68noncomputable section
  69
  70abbrev Pt := Fin 4 → ℝ
  71
  72/-! ## §1. Coordinates, partial derivatives, and the plane wave -/
  73
  74/-- Plane-wave phase `k · x`. -/
  75def phase (k x : Pt) : ℝ := ∑ i : Fin 4, k i * x i
  76
  77/-- Partial derivative of a scalar field in coordinate direction `μ`. -/
  78def pd (μ : Fin 4) (f : Pt → ℝ) (x : Pt) : ℝ :=
  79  deriv (fun t : ℝ => f (Function.update x μ t)) (x μ)
  80
  81/-- Frobenius square, `∑_{ij} H_{ij}²`.  Definitionally the same expression as
  82`ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq`, restated here so this module
  83imports nothing from the Regge side. -/
  84def frobSq (H : Mat4) : ℝ := ∑ i : Fin 4, ∑ j : Fin 4, H i j * H i j
  85
  86theorem phase_update (k x : Pt) (μ : Fin 4) (t : ℝ) :
  87    phase k (Function.update x μ t) = phase k x + k μ * (t - x μ) := by
  88  unfold phase
  89  have hterm : ∀ i : Fin 4,
  90      k i * Function.update x μ t i
  91        = k i * x i + (if i = μ then k μ * (t - x μ) else 0) := by
  92    intro i
  93    rcases eq_or_ne i μ with h | h
  94    · rw [h]
  95      have hu : Function.update x μ t μ = t := by simp
  96      rw [hu, if_pos rfl]
  97      ring
  98    · have hu : Function.update x μ t i = x i := by simp [h]
  99      rw [hu, if_neg h]
 100      ring
 101  rw [Finset.sum_congr rfl (fun i _ => hterm i), Finset.sum_add_distrib]
 102  simp
 103
 104theorem hasDerivAt_phase_update (k x : Pt) (μ : Fin 4) :
 105    HasDerivAt (fun t : ℝ => phase k (Function.update x μ t)) (k μ) (x μ) := by
 106  have hrw : (fun t : ℝ => phase k (Function.update x μ t))
 107      = fun t : ℝ => phase k x + k μ * (t - x μ) :=
 108    funext fun t => phase_update k x μ t
 109  rw [hrw]
 110  have h1 : HasDerivAt (fun t : ℝ => t - x μ) 1 (x μ) :=
 111    (hasDerivAt_id (x μ)).sub_const (x μ)
 112  simpa using ((h1.const_mul (k μ)).const_add (phase k x))
 113
 114theorem phase_update_self (k x : Pt) (μ : Fin 4) :
 115    phase k (Function.update x μ (x μ)) = phase k x := by
 116  simp
 117
 118/-- Derivative of a cosine plane wave.  **Proved**, not asserted: this is the
 119step that carries the real-standing-wave convention into the answer. -/
 120theorem pd_cos (c : ℝ) (k : Pt) (μ : Fin 4) (x : Pt) :
 121    pd μ (fun y => c * Real.cos (phase k y)) x = -(c * k μ) * Real.sin (phase k x) := by
 122  have hp := hasDerivAt_phase_update k x μ
 123  have hcos : HasDerivAt (fun t : ℝ => Real.cos (phase k (Function.update x μ t)))
 124      (-Real.sin (phase k x) * k μ) (x μ) := by
 125    have hc := (Real.hasDerivAt_cos (phase k (Function.update x μ (x μ)))).comp (x μ) hp
 126    rw [phase_update_self] at hc
 127    exact hc
 128  have hmul := hcos.const_mul c
 129  rw [pd, hmul.deriv]
 130  ring
 131
 132/-- Derivative of a sine plane wave. -/
 133theorem pd_sin (c : ℝ) (k : Pt) (μ : Fin 4) (x : Pt) :
 134    pd μ (fun y => c * Real.sin (phase k y)) x = (c * k μ) * Real.cos (phase k x) := by
 135  have hp := hasDerivAt_phase_update k x μ
 136  have hsin : HasDerivAt (fun t : ℝ => Real.sin (phase k (Function.update x μ t)))
 137      (Real.cos (phase k x) * k μ) (x μ) := by
 138    have hc := (Real.hasDerivAt_sin (phase k (Function.update x μ (x μ)))).comp (x μ) hp
 139    rw [phase_update_self] at hc
 140    exact hc
 141  have hmul := hsin.const_mul c
 142  rw [pd, hmul.deriv]
 143  ring
 144
 145/-- The metric perturbation `h_{ab}(x) = H_{ab} cos(k·x)`: a **real** standing
 146wave, matching the discrete side's convention. -/
 147def hWave (H : Mat4) (k : Pt) (a b : Fin 4) (x : Pt) : ℝ :=
 148  H a b * Real.cos (phase k x)
 149
 150/-! ## §2. A1: the linearized Christoffel symbol -/
 151
 152/-- **A1.**  `Γ⁽¹⁾_{λμν} = ½(∂_μ h_{λν} + ∂_ν h_{λμ} - ∂_λ h_{μν})`, indices
 153raised with the flat Euclidean metric. -/
 154def linChristoffel (H : Mat4) (k : Pt) (l μ ν : Fin 4) (x : Pt) : ℝ :=
 155  (1 / 2 : ℝ) *
 156    (pd μ (hWave H k l ν) x + pd ν (hWave H k l μ) x - pd l (hWave H k μ ν) x)
 157
 158/-- Closed-form amplitude of the linearized Christoffel symbol on the plane wave. -/
 159def chrAmp (H : Mat4) (k : Pt) (l μ ν : Fin 4) : ℝ :=
 160  (1 / 2 : ℝ) * (k l * H μ ν - k μ * H l ν - k ν * H l μ)
 161
 162theorem linChristoffel_eq (H : Mat4) (k : Pt) (l μ ν : Fin 4) (x : Pt) :
 163    linChristoffel H k l μ ν x = chrAmp H k l μ ν * Real.sin (phase k x) := by
 164  unfold linChristoffel chrAmp hWave
 165  rw [pd_cos, pd_cos, pd_cos]
 166  ring
 167
 168/-! ## §3. A2: the linearized Ricci tensor -/
 169
 170/-- **A2.**  `R⁽¹⁾_{μν} = ∂_λ Γ⁽¹⁾^λ_{μν} - ∂_ν Γ⁽¹⁾^λ_{μλ}`.  The `ΓΓ` terms of
 171the full Ricci contraction are quadratic in `h` and absent at this order. -/
 172def linRicci (H : Mat4) (k : Pt) (μ ν : Fin 4) (x : Pt) : ℝ :=
 173  (∑ l : Fin 4, pd l (linChristoffel H k l μ ν) x)
 174    - pd ν (fun y => ∑ l : Fin 4, linChristoffel H k l μ l y) x
 175
 176/-- Closed-form amplitude of the linearized Ricci tensor on the plane wave. -/
 177def ricciAmp (H : Mat4) (k : Pt) (μ ν : Fin 4) : ℝ :=
 178  (∑ l : Fin 4, k l * chrAmp H k l μ ν) - k ν * (∑ l : Fin 4, chrAmp H k l μ l)
 179
 180theorem linRicci_eq (H : Mat4) (k : Pt) (μ ν : Fin 4) (x : Pt) :
 181    linRicci H k μ ν x = ricciAmp H k μ ν * Real.cos (phase k x) := by
 182  have hdiv : ∀ l : Fin 4,
 183      pd l (linChristoffel H k l μ ν) x
 184        = (chrAmp H k l μ ν * k l) * Real.cos (phase k x) := by
 185    intro l
 186    have hfun : linChristoffel H k l μ ν
 187        = fun y => chrAmp H k l μ ν * Real.sin (phase k y) :=
 188      funext fun y => linChristoffel_eq H k l μ ν y
 189    rw [hfun, pd_sin]
 190  have htracefun : (fun y => ∑ l : Fin 4, linChristoffel H k l μ l y)
 191      = fun y => (∑ l : Fin 4, chrAmp H k l μ l) * Real.sin (phase k y) := by
 192    funext y
 193    rw [Finset.sum_mul]
 194    exact Finset.sum_congr rfl fun l _ => linChristoffel_eq H k l μ l y
 195  unfold linRicci ricciAmp
 196  rw [htracefun, pd_sin, Finset.sum_congr rfl (fun l _ => hdiv l), ← Finset.sum_mul]
 197  rw [sub_mul]
 198  refine congrArg₂ (· - ·) ?_ ?_
 199  · exact congrArg (· * Real.cos (phase k x))
 200      (Finset.sum_congr rfl fun l _ => mul_comm _ _)
 201  · ring
 202
 203/-! ## §4. The transverse-traceless reduction -/
 204
 205theorem sum_k_mul_row (H : Mat4) (k : Pt) (hsym : IsSymmetric H)
 206    (htrans : IsTransverse k H) (ν : Fin 4) :
 207    ∑ l : Fin 4, k l * H l ν = 0 := by
 208  have h := htrans ν
 209  rw [← h]
 210  refine Finset.sum_congr rfl fun l _ => ?_
 211  rw [hsym l ν]
 212  ring
 213
 214theorem sum_k_chrAmp (H : Mat4) (k : Pt) (hsym : IsSymmetric H)
 215    (htrans : IsTransverse k H) (μ ν : Fin 4) :
 216    ∑ l : Fin 4, k l * chrAmp H k l μ ν = (1 / 2 : ℝ) * momentumSq k * H μ ν := by
 217  have hμ := sum_k_mul_row H k hsym htrans μ
 218  have hν := sum_k_mul_row H k hsym htrans ν
 219  have hexp : ∀ l : Fin 4, k l * chrAmp H k l μ ν
 220      = ((1 / 2 : ℝ) * H μ ν) * (k l * k l)
 221        - ((1 / 2 : ℝ) * k μ) * (k l * H l ν)
 222        - ((1 / 2 : ℝ) * k ν) * (k l * H l μ) := by
 223    intro l; unfold chrAmp; ring
 224  rw [Finset.sum_congr rfl (fun l _ => hexp l), Finset.sum_sub_distrib,
 225    Finset.sum_sub_distrib, ← Finset.mul_sum, ← Finset.mul_sum, ← Finset.mul_sum, hμ, hν]
 226  simp only [momentumSq, mul_zero, sub_zero]
 227  ring
 228
 229theorem sum_chrAmp_trace (H : Mat4) (k : Pt) (hsym : IsSymmetric H)
 230    (htr : IsTraceless H) (μ : Fin 4) :
 231    ∑ l : Fin 4, chrAmp H k l μ l = 0 := by
 232  have hexp : ∀ l : Fin 4, chrAmp H k l μ l = -(((1 / 2 : ℝ) * k μ) * H l l) := by
 233    intro l
 234    unfold chrAmp
 235    rw [hsym l μ]
 236    ring
 237  rw [Finset.sum_congr rfl (fun l _ => hexp l), Finset.sum_neg_distrib, ← Finset.mul_sum]
 238  have : ∑ l : Fin 4, H l l = 0 := htr
 239  rw [this]
 240  ring
 241
 242theorem ricciAmp_tt (H : Mat4) (k : Pt) (hTT : IsTT k H) (μ ν : Fin 4) :
 243    ricciAmp H k μ ν = (1 / 2 : ℝ) * momentumSq k * H μ ν := by
 244  obtain ⟨hsym, htr, htrans⟩ := hTT
 245  unfold ricciAmp
 246  rw [sum_k_chrAmp H k hsym htrans μ ν, sum_chrAmp_trace H k hsym htr μ]
 247  ring
 248
 249/-- On the transverse-traceless space the linearized Ricci tensor is exactly
 250`-(1/2) □ h`, the massless wave operator. -/
 251theorem linRicci_tt (H : Mat4) (k : Pt) (hTT : IsTT k H) (μ ν : Fin 4) (x : Pt) :
 252    linRicci H k μ ν x = (1 / 2 : ℝ) * momentumSq k * H μ ν * Real.cos (phase k x) := by
 253  rw [linRicci_eq, ricciAmp_tt H k hTT]
 254
 255/-! ## §5. A3: the second variation density -/
 256
 257/-- Ricci scalar at linear order, traced with the flat metric. -/
 258def linRicciScalar (H : Mat4) (k : Pt) (x : Pt) : ℝ :=
 259  ∑ μ : Fin 4, linRicci H k μ μ x
 260
 261/-- Linearized Einstein tensor `G⁽¹⁾_{μν} = R⁽¹⁾_{μν} - ½ δ_{μν} R⁽¹⁾`. -/
 262def linEinstein (H : Mat4) (k : Pt) (μ ν : Fin 4) (x : Pt) : ℝ :=
 263  linRicci H k μ ν x
 264    - (1 / 2 : ℝ) * (if μ = ν then (1 : ℝ) else 0) * linRicciScalar H k x
 265
 266theorem linRicciScalar_tt (H : Mat4) (k : Pt) (hTT : IsTT k H) (x : Pt) :
 267    linRicciScalar H k x = 0 := by
 268  have htr : euclideanTrace H = 0 := hTT.2.1
 269  unfold linRicciScalar
 270  rw [Finset.sum_congr rfl (fun μ _ => linRicci_tt H k hTT μ μ x)]
 271  have hfac : ∀ μ : Fin 4,
 272      (1 / 2 : ℝ) * momentumSq k * H μ μ * Real.cos (phase k x)
 273        = ((1 / 2 : ℝ) * momentumSq k * Real.cos (phase k x)) * H μ μ := by
 274    intro μ; ring
 275  rw [Finset.sum_congr rfl (fun μ _ => hfac μ), ← Finset.mul_sum]
 276  have : ∑ μ : Fin 4, H μ μ = 0 := htr
 277  rw [this, mul_zero]
 278
 279theorem linEinstein_tt (H : Mat4) (k : Pt) (hTT : IsTT k H) (μ ν : Fin 4) (x : Pt) :
 280    linEinstein H k μ ν x
 281      = (1 / 2 : ℝ) * momentumSq k * H μ ν * Real.cos (phase k x) := by
 282  unfold linEinstein
 283  rw [linRicci_tt H k hTT, linRicciScalar_tt H k hTT]
 284  ring
 285
 286/-- **A3.**  The second derivative of `∫ √g R` along `g = δ + t h`, as a
 287density: `d²/dt² ∫√g R = -∫ h_{μν} G⁽¹⁾^{μν}`.  This is Euler's theorem for a
 288quadratic form applied to `S⁽²⁾[h] = -½ ∫ h G⁽¹⁾`, itself
 289`δ(√g R)/δg_{μν} = -√g G^{μν}` expanded about flat space. -/
 290def ehSecondVariationDensity (H : Mat4) (k : Pt) (x : Pt) : ℝ :=
 291  - ∑ μ : Fin 4, ∑ ν : Fin 4, hWave H k μ ν x * linEinstein H k μ ν x
 292
 293theorem ehSecondVariationDensity_tt (H : Mat4) (k : Pt) (hTT : IsTT k H) (x : Pt) :
 294    ehSecondVariationDensity H k x
 295      = -((1 / 2 : ℝ) * momentumSq k * frobSq H) * Real.cos (phase k x) ^ 2 := by
 296  unfold ehSecondVariationDensity hWave frobSq
 297  have hin : ∀ μ ν : Fin 4,
 298      H μ ν * Real.cos (phase k x) * linEinstein H k μ ν x
 299        = ((1 / 2 : ℝ) * momentumSq k * Real.cos (phase k x) ^ 2) * (H μ ν * H μ ν) := by
 300    intro μ ν
 301    rw [linEinstein_tt H k hTT]
 302    ring
 303  rw [Finset.sum_congr rfl
 304    (fun μ _ => Finset.sum_congr rfl (fun ν _ => hin μ ν))]
 305  simp only [← Finset.mul_sum]
 306  ring
 307
 308/-! ## §6. The phase average, and the derived Einstein-Hilbert face -/
 309
 310/-- Mean of a phase function over one period.  The density of §5 depends on `x`
 311only through `phase k x`, so for a nonzero wave covector the spatial average over
 312a large box equals this. -/
 313def phaseAverage (f : ℝ → ℝ) : ℝ :=
 314  (1 / (2 * Real.pi)) * ∫ θ in (0 : ℝ)..(2 * Real.pi), f θ
 315
 316theorem phaseAverage_const_mul (c : ℝ) (f : ℝ → ℝ) :
 317    phaseAverage (fun θ => c * f θ) = c * phaseAverage f := by
 318  unfold phaseAverage
 319  rw [intervalIntegral.integral_const_mul]
 320  ring
 321
 322/-- The mean square of a real cosine wave is `1/2`.  This is the entire content
 323of the discrete side's explicit `1/2`, and one of the two factors of two that
 324arc 2 has been unable to account for. -/
 325theorem phaseAverage_cos_sq : phaseAverage (fun θ => Real.cos θ ^ 2) = 1 / 2 := by
 326  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 327  unfold phaseAverage
 328  rw [integral_cos_sq]
 329  simp only [Real.sin_two_pi, Real.cos_two_pi, Real.sin_zero, Real.cos_zero,
 330    mul_zero, sub_zero, sub_self]
 331  field_simp
 332  ring
 333
 334/-- The density of §5, written as a function of the phase alone. -/
 335def densityOfPhase (H : Mat4) (k : Pt) (θ : ℝ) : ℝ :=
 336  -((1 / 2 : ℝ) * momentumSq k * frobSq H) * Real.cos θ ^ 2
 337
 338theorem density_factors_through_phase (H : Mat4) (k : Pt) (hTT : IsTT k H) (x : Pt) :
 339    ehSecondVariationDensity H k x = densityOfPhase H k (phase k x) :=
 340  ehSecondVariationDensity_tt H k hTT x
 341
 342/-- **The derived continuum Einstein-Hilbert face.**  The phase average, per unit
 343volume, of `d²/dt² ∫ √g R` on a real transverse-traceless cosine wave. -/
 344def ehFace (H : Mat4) (k : Pt) : ℝ :=
 345  -(1 / 4 : ℝ) * momentumSq k * frobSq H
 346
 347/-- **P1.**  The derived face is the average of the derived density.  Every step
 348between the Levi-Civita connection and this number is proved above. -/
 349theorem ehFace_eq_phaseAverage (H : Mat4) (k : Pt) :
 350    ehFace H k = phaseAverage (densityOfPhase H k) := by
 351  unfold densityOfPhase ehFace
 352  rw [phaseAverage_const_mul, phaseAverage_cos_sq]
 353  ring
 354
 355theorem ehFace_eq_average_of_density (H : Mat4) (k : Pt) (hTT : IsTT k H) (x : Pt) :
 356    ehSecondVariationDensity H k x = densityOfPhase H k (phase k x)
 357      ∧ ehFace H k = phaseAverage (densityOfPhase H k) :=
 358  ⟨density_factors_through_phase H k hTT x, ehFace_eq_phaseAverage H k⟩
 359
 360/-! ## §7. Rigidity: the derivation has no free constant
 361
 362Decoy T3 says a derivation with named inputs can be steered anywhere.  It cannot.
 363With A1 to A3 fixed, `ehFace` is a single number for each `(H, k)`, and the
 364statements below show it is not merely one of a family: scaling the density by
 365any `c ≠ 1` changes the face. -/
 366
 367theorem ehFace_rigid (H : Mat4) (k : Pt) (c : ℝ)
 368    (hne : momentumSq k * frobSq H ≠ 0)
 369    (h : phaseAverage (fun θ => c * densityOfPhase H k θ) = ehFace H k) :
 370    c = 1 := by
 371  rw [phaseAverage_const_mul, ← ehFace_eq_phaseAverage] at h
 372  unfold ehFace at h
 373  have hx : c * (-(1 / 4 : ℝ) * momentumSq k * frobSq H)
 374      = 1 * (-(1 / 4 : ℝ) * momentumSq k * frobSq H) := by rw [h]; ring
 375  have hne' : (-(1 / 4 : ℝ) * momentumSq k * frobSq H) ≠ 0 := by
 376    intro hz
 377    apply hne
 378    have : (-(1 / 4 : ℝ)) * (momentumSq k * frobSq H) = 0 := by
 379      rw [← hz]; ring
 380    rcases mul_eq_zero.mp this with h1 | h2
 381    · norm_num at h1
 382    · exact h2
 383  exact mul_right_cancel₀ hne' hx
 384
 385/-! ## §8. Status -/
 386
 387/-- What is derived here and what is assumed, in one string, so a reader who
 388never saw the write-up cannot mistake the tag. -/
 389def provenance : String :=
 390  "DERIVED: linearized Christoffel (A1), linearized Ricci (A2), TT reduction, the \
 391plane-wave derivatives (proved from Mathlib's deriv, not asserted), the cos-squared \
 392mean 1/2, and the resulting face -(1/4)·|k|²·‖H‖²_F for d²/dt² of ∫R√g per unit \
 393volume on a real cosine wave. ASSUMED: A3, that d²/dt² ∫√gR = -∫ h·G⁽¹⁾, which is \
 394Euler's theorem for a quadratic form plus δ(√gR)/δg = -√g G. NOT USED ANYWHERE HERE: \
 395the coupling table, the Bloch symbol, the norm gate, the preflight, or any existing \
 396coefficient in the tree."
 397
 398end
 399
 400end ContinuumTTSecondVariation4D
 401end Analysis
 402end Gravity
 403end IndisputableMonolith
 404