module module high

`IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D`

Continuum second variation of the Einstein-Hilbert integrand on real transverse-traceless cosine waves in Euclidean 4D. Delivers the phase-averaged face ehFace(H,k) = -(1/4)|k|²‖H‖²_F from the linearized Levi-Civita connection alone. Gravity arc-2 step-7 authors cite it to pin Regge's normalization against the continuum side. Argument builds plane-wave kinematics, linearized Christoffel amplitudes, then averages the second t-derivative of √g R.

claimOn a real transverse-traceless symmetric amplitude $H$ and nonzero Euclidean wave covector $k\in\mathbb{R}^4$, the phase average (per unit volume) of the second variation $d^2/dt^2\int R\sqrt{g}$ of the Einstein-Hilbert density along the cosine wave $h(t,x)=t\,H\cos(k\cdot x)$ equals $-\frac14 |k|^2 \|H\|_F^2$. The derivation uses the linearized Levi-Civita connection and states the identity $d^2/dt^2\int R\sqrt{g}=-\int h_{\mu\nu}G^{(1)\mu\nu}$ as an input.

background

This module sits in the QG full-theory campaign (arc 2, step 7): continuum Einstein-Hilbert second variation on transverse-traceless (TT) plane waves in 4D. Upstream, EdgeTTDecomposition4D supplies the linear-algebra TT projector for symmetric $4\times 4$ real matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$.

Local objects include the plane-wave phase $\phi(x)=k\cdot x$, its first derivatives, the Frobenius square $|H|_F^2$, the cosine wave metric perturbation $h(t,x)=t,H\cos(k\cdot x)$, and the linearized Christoffel symbols with their momentum-space amplitudes. The continuum face is computed without any Regge-calculus input: only the Levi-Civita connection and the stated second-variation identity A3.

Notation is Euclidean signature on $\mathbb{R}^4$; averages are over the phase torus. The TT condition on $H$ (transverse to $k$ and traceless) kills longitudinal and trace channels so the quadratic form collapses to a pure multiple of $|k|^2|H|_F^2$.

proof idea

Definition-heavy analytic module, not a single theorem. It introduces point and phase infrastructure, proves elementary derivative facts for phase updates (including hasDerivAt lemmas for cos/sin compositions), builds the TT cosine wave $h$, and computes linearized Christoffel amplitudes in momentum space.

The second $t$-derivative of the EH density is reduced, via the stated identity A3 linking $d^2/dt^2\int R\sqrt{g}$ to the linearized Einstein tensor contracted with $h$, to a quadratic form in $H$ and $k$. Phase averaging then kills cross terms and yields the exact face $-\frac14|k|^2|H|_F^2$. Upstream TT decomposition guarantees only physical modes enter the average.

why it matters in Recognition Science

Closes the continuum half of arc 2 step 7. Downstream, ReggeNormalizationDerived4D quotes the face directly: the phase average of $d^2/dt^2\int R\sqrt{g}$ per unit volume is ehFace H k = -(1/4)·|k|²·‖H‖²_F, derived from the Levi-Civita connection alone with no Regge-side access. Comparing that continuum coefficient to the banked Regge dictionary pins Regge's normalization constant.

EHSecondVariationExact4D isolates the remaining gap: A3 ($d^2/dt^2\int\sqrt{g}R=-\int h_{\mu\nu}G^{(1)\mu\nu}$) is stated and used here but not derived, the one place a hidden factor could still sit in the coefficient chain. ReggeNormalizationDerived4DAudit axiom-audits every named theorem of this module together with the Regge comparison, requiring exactly [propext, Classical.choice, Quot.sound].

In the broader Recognition gravity stack this supplies the continuum TT quadratic form that later matches discrete curvature weights, independent of the forcing chain (T0-T8) but required for the continuum-discrete dictionary.

scope and limits

Does not derive A3; states $d^2/dt^2\int R\sqrt{g}=-\int h_{\mu\nu}G^{(1)\mu\nu}$ as an input hypothesis.
Does not treat non-TT, massive, or gauge-longitudinal modes; TT projection is assumed.
Does not address Lorentzian signature or curved backgrounds; Euclidean $\mathbb{R}^4$ plane waves only.
Does not compute discrete Regge weights; continuum face only, compared downstream.
Does not fix overall EH normalization beyond the relative face coefficient $-1/4$.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4DAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D module_import

declarations in this module (37)

abbrev Pt L70
def phase L75
def pd L78
def frobSq L84
theorem phase_update L86
theorem hasDerivAt_phase_update L104
theorem phase_update_self L114
theorem pd_cos L120
theorem pd_sin L133
def hWave L147
def linChristoffel L154
def chrAmp L159
theorem linChristoffel_eq L162
def linRicci L172
def ricciAmp L177
theorem linRicci_eq L180
theorem sum_k_mul_row L205
theorem sum_k_chrAmp L214
theorem sum_chrAmp_trace L229
theorem ricciAmp_tt L242
theorem linRicci_tt L251
def linRicciScalar L258
def linEinstein L262
theorem linRicciScalar_tt L266
theorem linEinstein_tt L279
def ehSecondVariationDensity L290
theorem ehSecondVariationDensity_tt L293
def phaseAverage L313
theorem phaseAverage_const_mul L316
theorem phaseAverage_cos_sq L325
def densityOfPhase L335
theorem density_factors_through_phase L338
def ehFace L344
theorem ehFace_eq_phaseAverage L349
theorem ehFace_eq_average_of_density L355
theorem ehFace_rigid L367
def provenance L389