exact_average_eq_ehFace
plain-language theorem explainer
On a transverse-traceless cosine wave with Frobenius norm squared equal to 2, the wavelength average of the exact second-variation density equals the derived Einstein-Hilbert face −(1/4)|k|²‖H‖²_F. Gravity analysts checking step 7's continuum coefficient cite this equality. The proof rewrites the average closed form, unfolds the face definition, substitutes the norm hypothesis, and finishes by ring.
Claim. Let $H$ be a $4\times 4$ real matrix and $k$ a wave covector. If $\|H\|_F^2 = 2$, then the wavelength average of the exact transverse-traceless second-variation density of $\int\sqrt{g}\,R$ at momentum squared $|k|^2$ equals the derived Einstein-Hilbert face $-\frac14 |k|^2 \|H\|_F^2$.
background
This module sits in the continuum gravity analysis that audits step 7 of the Recognition Science coefficient chain for the Einstein-Hilbert action. Step 7 produced the continuum face $-\frac14 |k|^2 |H|F^2$ from linearized connection (A1), linearized Ricci (A2), Regge normalization, and an undischarged identity A3 equating $d^2/dt^2\int\sqrt{g} R$ to $-\int h{\mu\nu} G^{(1)\mu\nu}$. A3 fixes overall density normalization, so a hidden factor could still sit there.
The exact density (closed form from full inverse metric, Christoffel, Ricci, and scalar curvature, no $t$-expansion) was obtained off-kernel by symbolic algebra and is treated as given input here. For the plus TT polarization it is $\kappa^2(7\sin^2(\kappa z)-4)$; its wavelength average is $-\kappa^2/2$. The derived face is defined as ehFace H k = -(1/4)·momentumSq k · frobSq H. With $|H|_F^2=2$ that is exactly $-\frac14 |k|^2·2$.
Upstream, ehFace is the phase-average target proved from the linearized continuum pipeline in ContinuumTTSecondVariation4D. Sibling lemmas supply wavelength averages of the exact TT, pure-trace, and longitudinal densities.
proof idea
Four-step algebraic identification, not a curvature computation.
- Rewrite the left-hand side by
exactDensityTT_average, which already evaluates the wavelength average of the exact TT density as a closed rational expression in the momentum square. - Unfold the definition of the continuum Einstein-Hilbert face: $-\frac14·|k|^2·|H|_F^2$.
- Substitute the hypothesis $|H|_F^2=2$.
ringequates the two polynomial expressions in $|k|^2$.
No connection, Ricci, or variation lemmas are invoked; the work is pure identification of two already-reduced scalars under the Frobenius-norm witness.
why it matters
This is the bridge that lets the exact (non-linearized) second variation speak to step 7's derived face. Downstream, a3_agrees_with_exact rewrites through this theorem and ehFace_eq_phaseAverage to conclude that step 7's assumed A3 right-hand side and the exact left-hand side share the same wavelength average at the TT witness, so "the assumption did not move the coefficient."
In the module's audit language: A1 and A2 built the face; the exact density was never linearized; their averages match when $|H|_F^2=2$. That pins the overall normalization of the continuum EH density on the TT sector and removes the last free factor in arc 2's coefficient chain for this witness class. Sibling discrimination (trace_decoy_misses_the_face) shows the same face formula fails on pure-trace data with the same Frobenius square, so the match is TT-specific rather than vacuous curve-fitting.
The exact curvature itself remains DERIVED-UNFORMALIZED (Python symbolic receipt); this theorem only equates averages downstream of that closed form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.