lagrangian_route_same_face
plain-language theorem explainer
Phase average of the Lagrangian density on a real transverse-traceless cosine wave equals the continuum Einstein-Hilbert second-variation face. Gravity analysts cite it when equating the two classical routes that feed Regge normalization. The proof unfolds both sides, rewrites by phase-average and norm identities, then closes by ring.
Claim. For every $4\times 4$ real matrix $H$ and every wave vector $k\in\mathbb{R}^4$, the phase average of the phase-dependent Lagrangian density built from $(H,k)$ equals the continuum Einstein-Hilbert face $\mathrm{ehFace}(H,k)=-(1/4)\,|k|^2\,\|H\|_F^2$.
background
Arc 2, step 7 of the gravity analysis derives Regge's normalization constant without assuming it. The continuum side, from ContinuumTTSecondVariation4D, already shows that the phase average of the second variation of $\int R\sqrt{g}$ per unit volume on a real transverse-traceless cosine wave is the face $\mathrm{ehFace}(H,k)=-(1/4)\cdot|k|^2\cdot|H|_F^2$, obtained from the Levi-Civita connection alone.
A second classical density is the phase-dependent Lagrangian density along the same wave. The two densities are not pointwise equal: at zero phase one vanishes and the other need not. Agreement is expected only after averaging over the eight-tick phase circle. Wave4 is simply a map $\mathrm{Fin},4\to\mathbb{R}$ packaging the wave covector.
Sibling equalities identify the squared Frobenius norm of the TT amplitude and the squared spatial momentum with the scalars that appear after averaging $\sin^2$ factors. Those identities, together with linearity of phase average, set up an algebraic comparison of the two faces.
proof idea
Term-mode proof. Unfold the definitions of the phase-dependent Lagrangian density and of the EH face. Rewrite with four lemmas: phase average pulls out constant multipliers; the phase average of $\sin^2$ evaluates to the known constant; the Frobenius-square identity and the momentum-square identity replace the remaining quadratic forms by the shared scalars. The resulting polynomial identity is discharged by ring.
why it matters
This is the bridge that makes the two classical continuum faces interchangeable after averaging. Downstream, step7Cert packages it with the normalization gate, the identification of the discrete bookkeeping factor as $1/\rho$, the frozen-preflight EH-integral face, and the tetrahedron deficit sum. That certificate is the second half of Arc 2 step 7: showing that the historical factor-of-two mismatch between $-(1/8)$ and $-(1/4)$ is Regge's normalization $\rho=1/2$, not an error in either computation.
In the module's language, the two routes really are different densities and agree only after averaging, which is what makes the agreement informative. The result supports leaving $\rho$ free, forcing $\rho=1/2$ from the dictionary, and refuting the frozen preflight's implicit $\rho=1$. It sits entirely on the continuum side of the gravity analysis; the discrete Regge action $\sum_h A_h\delta_h$ enters only through the parent certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.