IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4D

   1import IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D
   2
   3/-!
   4# The exact second variation of `∫ √g R`, and what it says about step 7's A3
   5
   6Step 7 derived the continuum Einstein-Hilbert face `-(1/4)·|k|²·‖H‖²_F` from four
   7inputs.  Three of them (A1 the linearized Levi-Civita connection, A2 the linearized
   8Ricci tensor, and Regge's own normalization) are formalized.  The fourth, **A3**,
   9that `d²/dt² ∫√g R = -∫ h_{μν} G⁽¹⁾^{μν}`, is *stated and used* in
  10`ContinuumTTSecondVariation4D` and never derived there.  It is the one place in
  11arc 2's coefficient chain where a factor could still hide, because it is the step
  12that fixes the overall normalization of the density.
  13
  14## What is now known, and how
  15
  16A3 has been tested exactly, off Lean, by
  17`scripts/qg/eh_second_variation_exact_20260727.py`: for the metric family
  18`g_{μν}(t) = δ_{μν} + t H_{μν} cos(κ z)` in four Euclidean dimensions with the wave
  19along `z`, that script builds the **full** inverse metric, the **full** Christoffel
  20symbols, the **full** Ricci tensor and the **full** scalar curvature with no
  21expansion in `t` anywhere, then takes `d²/dt²` of `√(det g)·R` at `t = 0` and
  22averages over one wavelength.  It compares the result against `-∫h·G⁽¹⁾` built the
  23way `ContinuumTTSecondVariation4D` builds it.  Findings:
  24
  25* On the plus polarization the exact density is `κ²·(7 sin²(κz) - 4)`, whose
  26  wavelength average is `-κ²/2`, which is exactly `-(1/4)·κ²·2` and so exactly the
  27  derived face.  Same on the cross polarization.  Same, scaled by four, on twice the
  28  plus polarization.
  29* A3's own right-hand side agrees with the exact left-hand side at **every** witness
  30  tried, including two that are not transverse-traceless (a transverse pure trace
  31  and a longitudinal perturbation).  So A3 is not an artefact of the TT reduction.
  32* The face formula is specific to TT, as it must be: the transverse pure trace has
  33  the same Frobenius square 2 and the same wave, and its exact average is `+κ²/2`,
  34  the opposite sign from the face.  A formula that fit that too would be fitting
  35  nothing.
  36
  37That is a symbolic-algebra receipt, not a kernel one, so the exact curvature is
  38tagged **DERIVED-UNFORMALIZED** and this module does not assert it.
  39
  40## What this module proves
  41
  42Everything downstream of the closed form, in Lean, at the base triple: that the
  43exact density's wavelength average **is** the derived Einstein-Hilbert face, that it
  44therefore agrees with A3's right-hand side at the witness, that the two non-TT
  45decoys do **not** land on the face, and that no rescaling of the density survives.
  46
  47## What remains open
  48
  49One named goal: derive `d²/dt²(√(det g)·R)|_{t=0} = κ²(7 sin²(κz) - 4)` inside Lean
  50from `pd`, the Christoffel formula and the Ricci contraction, rather than from the
  51symbolic receipt.  `ContinuumTTSecondVariation4D.pd` is already the right
  52primitive (a one-dimensional `deriv` through `Function.update`, so no `fderiv`
  53machinery is needed), and for the plus polarization the perturbed metric is
  54diagonal, `diag(1, 1 + t cos κz, 1 - t cos κz, 1)`, so its inverse can be written
  55down explicitly and *proved* to be the inverse rather than obtained from
  56`Matrix.inv`.  The exact intermediate the script prints, for whoever formalizes it:
  57
  58  `det g = 1 - t² cos²(κz)`
  59  `R = κ²t²(3t² sin⁴ - 7t² sin² + 4t² + 7 sin² - 4) / (2(1 - t² cos²)²)`
  60
  61Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  62-/
  63
  64namespace IndisputableMonolith
  65namespace Gravity
  66namespace Analysis
  67namespace EHSecondVariationExact4D
  68
  69open BigOperators
  70open EdgeTTDecomposition4D (Mat4 momentumSq)
  71open ContinuumTTSecondVariation4D (Pt phaseAverage densityOfPhase ehFace frobSq
  72  phaseAverage_const_mul ehFace_eq_phaseAverage)
  73
  74noncomputable section
  75
  76/-! ## §1. Two phase averages
  77
  78`ContinuumTTSecondVariation4D` proves the cosine-squared mean.  The exact density
  79is a sine-squared plus a constant, so those are the two averages needed here.
  80-/
  81
  82theorem phaseAverage_const (c : ℝ) : phaseAverage (fun _ => c) = c := by
  83  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
  84  unfold phaseAverage
  85  rw [intervalIntegral.integral_const]
  86  simp only [smul_eq_mul, sub_zero]
  87  field_simp
  88
  89theorem phaseAverage_sin_sq : phaseAverage (fun θ => Real.sin θ ^ 2) = 1 / 2 := by
  90  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
  91  unfold phaseAverage
  92  rw [integral_sin_sq]
  93  simp only [Real.sin_two_pi, Real.cos_two_pi, Real.sin_zero, Real.cos_zero,
  94    zero_mul, sub_zero, sub_self]
  95  field_simp
  96  ring
  97
  98/-- Average of `a·sin²θ + b`, which is the shape of every exact density below. -/
  99theorem phaseAverage_sin_sq_affine (a b : ℝ) :
 100    phaseAverage (fun θ => a * Real.sin θ ^ 2 + b) = a / 2 + b := by
 101  have hsin : IntervalIntegrable (fun θ : ℝ => a * Real.sin θ ^ 2)
 102      MeasureTheory.volume 0 (2 * Real.pi) :=
 103    (continuous_const.mul (Real.continuous_sin.pow 2)).intervalIntegrable _ _
 104  have hconst : IntervalIntegrable (fun _ : ℝ => b)
 105      MeasureTheory.volume 0 (2 * Real.pi) :=
 106    continuous_const.intervalIntegrable _ _
 107  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 108  unfold phaseAverage
 109  rw [intervalIntegral.integral_add hsin hconst,
 110    intervalIntegral.integral_const_mul, integral_sin_sq,
 111    intervalIntegral.integral_const]
 112  simp only [Real.sin_two_pi, Real.cos_two_pi, Real.sin_zero, Real.cos_zero,
 113    zero_mul, sub_zero, sub_self, smul_eq_mul]
 114  field_simp
 115  ring
 116
 117/-! ## §2. The exact densities
 118
 119Each is `d²/dt²(√(det g)·R)` at `t = 0` on the named perturbation, written as a
 120function of the phase, as computed from the Christoffel definition by
 121`scripts/qg/eh_second_variation_exact_20260727.py`.  `m` is `|k|²`.
 122-/
 123
 124/-- Exact second variation density on a transverse-traceless wave of Frobenius
 125square 2 (the plus and cross polarizations both give this). -/
 126def exactDensityTT (m : ℝ) (θ : ℝ) : ℝ := m * (7 * Real.sin θ ^ 2 - 4)
 127
 128/-- Exact second variation density on a transverse **pure trace** of Frobenius
 129square 2.  Same mass, same wave, different physics. -/
 130def exactDensityTrace (m : ℝ) (θ : ℝ) : ℝ := m * Real.sin θ ^ 2
 131
 132/-- Exact second variation density on a longitudinal perturbation, Frobenius
 133square 1.  It vanishes identically. -/
 134def exactDensityLongitudinal (_m : ℝ) (_θ : ℝ) : ℝ := 0
 135
 136theorem exactDensityTT_average (m : ℝ) :
 137    phaseAverage (exactDensityTT m) = -(m / 2) := by
 138  have hrw : exactDensityTT m
 139      = fun θ => (7 * m) * Real.sin θ ^ 2 + (-(4 * m)) := by
 140    funext θ; unfold exactDensityTT; ring
 141  rw [hrw, phaseAverage_sin_sq_affine]
 142  ring
 143
 144theorem exactDensityTrace_average (m : ℝ) :
 145    phaseAverage (exactDensityTrace m) = m / 2 := by
 146  have hrw : exactDensityTrace m = fun θ => m * Real.sin θ ^ 2 + 0 := by
 147    funext θ; unfold exactDensityTrace; ring
 148  rw [hrw, phaseAverage_sin_sq_affine]
 149  ring
 150
 151theorem exactDensityLongitudinal_average (m : ℝ) :
 152    phaseAverage (exactDensityLongitudinal m) = 0 := by
 153  unfold exactDensityLongitudinal
 154  simpa using phaseAverage_const (0 : ℝ)
 155
 156/-! ## §3. The exact computation lands on the derived face
 157
 158Stated for any polarization of Frobenius square 2 and any wave covector, because
 159`ehFace` depends on `H` only through `frobSq H`.  The script's witness is a
 160relabeling of the banked plus and cross polarizations, both of which have
 161Frobenius square 2.
 162-/
 163
 164/-- **The result.**  The wavelength average of the exact second variation equals
 165step 7's derived Einstein-Hilbert face.  No linearization was used to obtain the
 166left-hand side; A1 and A2 were used to obtain the right-hand side. -/
 167theorem exact_average_eq_ehFace (H : Mat4) (k : Pt) (hF : frobSq H = 2) :
 168    phaseAverage (exactDensityTT (momentumSq k)) = ehFace H k := by
 169  rw [exactDensityTT_average]
 170  unfold ContinuumTTSecondVariation4D.ehFace
 171  rw [hF]
 172  ring
 173
 174/-- **A3 at the witness.**  Step 7's assumed right-hand side and the exact
 175left-hand side have the same wavelength average, so the assumption did not move
 176the coefficient. -/
 177theorem a3_agrees_with_exact (H : Mat4) (k : Pt) (hF : frobSq H = 2) :
 178    phaseAverage (exactDensityTT (momentumSq k)) = phaseAverage (densityOfPhase H k) := by
 179  rw [exact_average_eq_ehFace H k hF, ehFace_eq_phaseAverage]
 180
 181/-! ## §4. Discrimination: the face formula is not fitting everything
 182
 183A gate that never fires has not been tested.  These two perturbations are exactly
 184what a fit-anything face formula would also capture, and it does not capture them.
 185-/
 186
 187/-- The transverse pure trace carries the same Frobenius square 2 and the same
 188wave, and its exact average has the **opposite sign** from the face.  So
 189`exact_average_eq_ehFace` is a statement about transverse-traceless data and not
 190about perturbations of mass 2. -/
 191theorem trace_decoy_misses_the_face (H : Mat4) (k : Pt) (hF : frobSq H = 2)
 192    (hm : momentumSq k ≠ 0) :
 193    phaseAverage (exactDensityTrace (momentumSq k)) ≠ ehFace H k := by
 194  rw [exactDensityTrace_average]
 195  unfold ContinuumTTSecondVariation4D.ehFace
 196  rw [hF]
 197  intro h
 198  apply hm
 199  have : momentumSq k / 2 + (1 / 4 : ℝ) * momentumSq k * 2 = 0 := by
 200    rw [h]; ring
 201  linarith [this]
 202
 203/-- The longitudinal perturbation has vanishing exact second variation, which the
 204face formula does not report for a nonzero polarization. -/
 205theorem longitudinal_decoy_misses_the_face (H : Mat4) (k : Pt) (hF : frobSq H = 1)
 206    (hm : momentumSq k ≠ 0) :
 207    phaseAverage (exactDensityLongitudinal (momentumSq k)) ≠ ehFace H k := by
 208  rw [exactDensityLongitudinal_average]
 209  unfold ContinuumTTSecondVariation4D.ehFace
 210  rw [hF]
 211  intro h
 212  apply hm
 213  linarith [h]
 214
 215/-- **Rigidity.**  Rescaling the exact density by any `c ≠ 1` breaks the agreement,
 216so the match is not a normalization that was free to be chosen. -/
 217theorem exact_density_rigid (m c : ℝ) (hm : m ≠ 0)
 218    (h : phaseAverage (fun θ => c * exactDensityTT m θ) = -(m / 2)) : c = 1 := by
 219  rw [phaseAverage_const_mul, exactDensityTT_average] at h
 220  have hm2 : -(m / 2) ≠ 0 := by
 221    intro hz; exact hm (by linarith)
 222  have hone : c * -(m / 2) = 1 * -(m / 2) := by rw [one_mul]; exact h
 223  exact mul_right_cancel₀ hm2 hone
 224
 225/-! ## §5. Provenance, in one string -/
 226
 227/-- What is derived here and what is not, in the words a referee needs. -/
 228def provenance : String :=
 229  "DERIVED IN LEAN: the wavelength averages, the identification of the exact TT \
 230density's average with step 7's derived face -(1/4)|k|^2||H||_F^2, the agreement \
 231of that average with A3's own right-hand side, the failure of a transverse pure \
 232trace of the same Frobenius mass and of a longitudinal perturbation to land on \
 233the face, and the rigidity of the coefficient under rescaling. \
 234DERIVED BUT NOT IN LEAN (symbolic algebra, scripts/qg/eh_second_variation_exact_20260727.py): \
 235that d^2/dt^2 of sqrt(det g) R at t=0 on the plus polarization is kappa^2(7 sin^2 - 4), \
 236computed from the full inverse metric, full Christoffels and full Ricci with no \
 237expansion in t, and the agreement of A3's two sides at five witnesses including two \
 238that are not transverse-traceless. NOT USED ANYWHERE HERE: the Regge tree, the \
 239coupling table, the Bloch symbol, the norm gate, or any banked coefficient."
 240
 241end
 242
 243end EHSecondVariationExact4D
 244end Analysis
 245end Gravity
 246end IndisputableMonolith
 247