two_routes_differ_pointwise
plain-language theorem explainer
At phase zero the Lagrangian-route density vanishes while the continuum TT second-variation density equals minus half the product of wave and Frobenius norms, hence is nonzero whenever that product is. Anyone separating the two Regge-versus-continuum faces cites this pointwise mismatch. The proof evaluates both closed forms at θ=0 via sin/cos and obtains a contradiction from the nonzero-product hypothesis.
Claim. Let $H$ be a $4\times 4$ real matrix and $k$ a four-component wave. If the product of the wave norm squared and the Frobenius norm squared of $H$ is nonzero, then the Lagrangian density of phase of $(H,k)$ at phase $0$ is not equal to the continuum density of phase of $(H,k)$ at phase $0$.
background
This module sits in Arc 2, step 7: it places the continuum second variation of $\int R\sqrt{g}$ on a real transverse-traceless cosine wave beside the banked Regge dictionary and isolates the constant that relates them. Continuum analysis (no Regge input) yields the phase-averaged face $ehFace,H,k=-(1/4),|k|^2,|H|_F^2$. Regge's classical normalization is $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$ with historically $\rho=1/2$; the module leaves $\rho$ free and forces it from the dictionary.
Two scalar densities of phase are compared. Upstream, densityOfPhase is the continuum §5 density written as a function of phase alone: $-\tfrac12,(\mathrm{momentumSq},k),(\mathrm{frobSq},H),\cos^2\theta$. The sibling Lagrangian-route density (unfolded in the proof) carries a $\sin$ factor and therefore vanishes at $\theta=0$. The wave type is simply $\mathrm{Fin},4\to\mathbb{R}$. The nonzero-product hypothesis excludes the trivial zero-wave or zero-perturbation case.
proof idea
Two short evaluations, then a contradiction. Unfold the Lagrangian density and rewrite with $\sin 0=0$; a ring simplification gives value $0$ at phase zero. Unfold the continuum density, rewrite via the in-module identities equating Frobenius and momentum squares to the wave/Frobenius norms, and use $\cos 0=1$; ring yields $-\tfrac12,(\mathrm{waveNormSq},k\cdot\mathrm{frobeniusNormSq},H)$. Substitute both evaluations into the claimed inequality. Assuming equality forces $0$ equal to that negative half-product, which linarith contradicts against the hypothesis that the product is nonzero.
why it matters
The module's thesis is that the factor-of-two gap between the computed continuum face $-(1/8)$ and the frozen dictionary face $-(1/4)$ is exactly Regge's normalization $\rho=1/2$ (so discreteBookkeepingFactor:=2 is $1/\rho$), not a bookkeeping error. For that diagnosis to be informative, the two densities must be genuinely different functionals that only agree after phase averaging. This theorem records the pointwise mismatch at $\theta=0$: one route is zero, the other is not. No downstream users are wired yet (used_by empty); it is a local witness inside the Regge-normalization derivation, supporting the narrative that both numbers are correct faces of different actions and that the historical gate failed by comparing unequal functionals. It does not itself pin $\rho$; that is done in the dictionary and Gauss-Bonnet checks elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.