lagrangianDensityOfPhase
plain-language theorem explainer
Defines the phase-dependent density of the quadratic-Lagrangian route on a real TT cosine wave: −(1/2)|k|²‖H‖_F² sin²θ. Gravity analysts comparing continuum second-variation faces to the Regge dictionary cite it. It is a pure algebraic definition, not a theorem.
Claim. For a $4\times 4$ polarization matrix $H$ and a real wave covector $k\in\mathbb{R}^4$, the quadratic-Lagrangian density at phase $\theta$ is $-\tfrac12\,|k|^2\,\|H\|_F^2\sin^2\theta$.
background
This module sits in Arc 2, step 7 of the 4D Regge continuum analysis. From the Levi-Civita connection alone, the continuum second variation of $\int R\sqrt{g}$ on a real transverse-traceless cosine wave has phase-averaged face $ehFace(H,k)=-(1/4),|k|^2,|H|_F^2$. The discrete side is the Regge action $\sum_h A_h\delta_h$, related to the continuum Einstein–Hilbert integral by an unknown normalization $\rho$, historically $\rho=1/2$.
Two scalar ingredients appear on both routes: the squared Euclidean wave norm $|k|^2=\sum_i k_i^2$ and the Frobenius squared norm $|H|F^2=\sum{i,j}H_{ij}^2$. The present definition packages the quadratic-Lagrangian density before phase averaging, with the $\sin^2\theta$ modulation of a cosine wave. A parallel density (the curvature/Regge route) is compared later; the two agree only after averaging.
proof idea
No proof: this is a one-line definition. It multiplies the constant prefactor $-(1/2),\mathrm{waveNormSq}(k),\mathrm{frobeniusNormSq}(H)$ by $\sin^2\theta$. Downstream, phaseAverage and the identity $\langle\sin^2\rangle=1/2$ recover $ehFace$.
why it matters
It is the phase-resolved face of the continuum quadratic-Lagrangian route. The theorem lagrangian_route_same_face shows its phase average equals ehFace, so the continuum second-variation coefficient $-(1/4)$ is recovered without assuming Regge’s $\rho$. two_routes_differ_pointwise uses the $\theta=0$ vanishing of this density to prove the two routes are genuinely different pointwise densities that only meet after averaging. Both facts feed Step7Cert, which packages discharge of the normalization gate, the average identity, and the relation $\mathrm{discreteBookkeepingFactor}\cdot\mathrm{reggeNormalization}=1$. In the module narrative, the factor-of-two mismatch with the frozen preflight is Regge’s normalization $1/\rho$, not an error in either computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.