ehFace_rigid
plain-language theorem explainer
If the phase average of a constant multiple c of the continuum TT second-variation density equals the Einstein-Hilbert face value, and the wave is nondegenerate, then c must be 1. Anyone auditing that the continuum EH derivation has no free normalization cites this. The proof rewrites both sides to a common nonzero scalar and cancels.
Claim. Let $H$ be a $4\times 4$ real matrix and $k\in\mathbb{R}^4$. Write $k^2$ for the squared momentum and $\|H\|_F^2$ for the Frobenius square. If $k^2\|H\|_F^2\neq 0$ and the phase average of $\theta\mapsto c\cdot\rho(H,k,\theta)$ equals the continuum Einstein-Hilbert face value of $(H,k)$, then $c=1$.
background
This module (Arc 2, step 7) derives, from the linearized Levi-Civita connection alone, the number that the Einstein-Hilbert action $\int R\sqrt{g}$ assigns to a real transverse-traceless plane wave in 4D. The discrete Regge side averages $d^2/dt^2$ of the action under $h(x)=H\cos(k\cdot x)$; the continuum object matched here is the same phase average of the second variation density, not the quadratic Taylor coefficient.
The face value ehFace H k is the closed-form scalar $-\frac14,k^2|H|_F^2$. The density densityOfPhase H k θ is the pointwise second-variation density as a function of the plane-wave phase $θ=k\cdot x$. An upstream identity already proves that the face equals the phase average of that density: ehFace H k = phaseAverage (densityOfPhase H k).
Section 7 frames rigidity against Decoy T3 (the claim that a derivation with named classical inputs can be steered by an overall constant). With the classical inputs A1–A3 fixed, the face is a single number per $(H,k)$; this theorem says scaling the density by any $c\neq 1$ moves that number.
proof idea
Rewrite the hypothesis with phaseAverage_const_mul and the identity ehFace_eq_phaseAverage, so both sides become multiples of the same face expression. Unfold ehFace to expose the scalar $-\frac14,k^2|H|_F^2$. The hypothesis then reads $c\cdot s = 1\cdot s$ for $s=-\frac14,k^2|H|_F^2$. Nondegeneracy $k^2|H|_F^2\neq 0$ implies $s\neq 0$ (via mul_eq_zero and a norm_num check that $-1/4\neq 0$). Cancel $s$ on the right with mul_right_cancel₀ to conclude $c=1$.
why it matters
Closes the rigidity half of §7 in the continuum TT second-variation derivation: the continuum face is not one member of a one-parameter family. Together with ehFace_eq_phaseAverage and the density factorization through phase, it shows that every step from linearized Christoffel symbols to the numerical face is fixed once A1–A3 are fixed.
The module exists to settle the continuum side of the Regge midpoint dictionary independently of the banked preflight coefficient $-1/4$ and the ad-hoc discreteBookkeepingFactor := 2. Rigidity here means no free constant can be smuggled in when that comparison is later made in ReggeNormalizationDerived4D. No downstream consumers are wired yet (used_by is empty); the theorem is a local audit gate for the continuum derivation itself, answering Decoy T3 in the negative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.