Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4D

show as:
view Lean formalization →

Exact phase-averaged second-variation densities for the Einstein-Hilbert action in 4D, for transverse-traceless, trace, and longitudinal modes. Gravity analysts comparing continuum EH faces to Regge midpoint dictionaries cite it. The argument reduces each density to an affine sin-squared form, averages over the phase, and matches the banked EH face coefficient.

claimIn 4D, the phase averages of the exact continuum second-variation densities of $\int R\sqrt{g}$ for TT, pure-trace, and longitudinal plane-wave modes equal the corresponding Einstein-Hilbert face values; in particular the TT average agrees with the banked coefficient $a_3$, while a pure-trace decoy misses that face.

background

Arc 2 of the gravity analysis derives continuum second variations of the Einstein-Hilbert action $\int R\sqrt{g}$ in four dimensions from the Levi-Civita connection alone, in the same convention as the banked Regge midpoint dictionary. The upstream module ContinuumTTSecondVariation4D supplies the continuum TT second variation of that action for a real transverse-traceless plane wave.

This module packages the exact mode densities (TT, trace, longitudinal) and their phase averages. Every exact density below has the affine shape $a\sin^2\theta+b$; the elementary averages of constants and of $\sin^2$ therefore control the face values. The setting is classical GR linearized about flat space, with plane-wave polarization projectors and a uniform phase average over one period.

proof idea

The module is a short calculation chain, not a definition dump. First, phase averages of constants and of $\sin^2\theta$ (and the affine combination $a\sin^2\theta+b$) are recorded as elementary real identities. Exact continuum densities for TT, trace, and longitudinal modes are written in that affine shape. Their phase averages are then evaluated by applying the sin-squared lemmas. The TT average is identified with the banked EH face; a named comparison shows the continuum $a_3$ coefficient agrees with that exact average, while a pure-trace decoy is shown to miss the face.

why it matters in Recognition Science

The module closes the continuum side of the EH second-variation comparison in 4D: exact phase-averaged densities, not schematic symbols, sit on the continuum face that the Regge midpoint dictionary must match. Downstream, EHSecondVariationExact4DAudit imports the module and runs a full axiom audit (#print axioms on every named result), expecting only the standard classical footprint. That audit treats the base-triple reading as a claim about postulates, not about extra geometric axioms. Within Recognition gravity analysis this is the exact continuum counterpart to the discrete second-variation bookkeeping that feeds curvature and Newtonian limits; it does not itself invoke the forcing chain (T0-T8) or the J-cost, but it supplies the GR face those discrete constructions are measured against.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)