regge_normalization_pinned
plain-language theorem explainer
Whenever the free-normalization Regge face equals the continuum exact-midpoint Bloch second-variation face on a transverse-traceless 4D wave with nonzero Frobenius and wave norms, the normalization constant is forced to ρ = 1/2. Gravity analysts matching discrete Regge action to continuum Einstein-Hilbert cite this pinning. The proof rewrites both faces to scalar multiples of the same norm product and cancels the nonzero factor.
Claim. Let $H$ be a $4\times 4$ real matrix and $k\in\mathbb{R}^4$ a wavevector such that $H$ is symmetric, Euclidean-traceless, and transverse to $k$. Write $N_F=\|H\|_F^2$ and $N_k=|k|^2$. If $N_F N_k\neq 0$ and the Regge face at free normalization $\rho$ equals the exact-midpoint Bloch $M_2$ face of $(H,k)$, then $\rho=1/2$.
background
Arc 2, step 7 (second half) places two independently computed second-variation faces side by side. From the Levi-Civita connection alone, with no Regge input, the continuum module shows that the phase average of $d^2/dt^2\int R\sqrt{g}$ per unit volume on a real transverse-traceless cosine wave is $-(1/4),|k|^2|H|_F^2$.
The discrete object is the Regge action $\sum_h A_h\delta_h$ (area times deficit). Classically one writes $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$ with historical value $\rho=1/2$. This module leaves $\rho$ free: the Regge face is the dictionary expression linear in $\rho$, while the continuum face is the banked exact-midpoint Bloch $M_2$ value.
Algebraic TT means $H$ is symmetric, traceless, and transverse to the wavevector $k$ (a map $\mathrm{Fin},4\to\mathbb{R}$). The nonzero product of Frobenius and wave norm squares excludes the degenerate zero mode where both faces vanish identically.
proof idea
Rewrite the equality hypothesis with two identities: the continuum face equals $-\tfrac18$ times the Frobenius-wave product under the TT hypothesis, and the Regge face expands to $(\rho/4)$ times that same product. Rearrange by linear combination to $(\rho/4-1/8)\cdot(|H|_F^2|k|^2)=0$. Split on the zero-product rule: either the coefficient vanishes, which is $\rho=1/2$ by linarith, or the norm product vanishes, contradicting the nonzero hypothesis.
why it matters
This is paper checkpoint P3 and classical input A4: the 1,208-row discrete dictionary (exact Heron areas and Gram dihedral derivatives, no continuum input) forces $\rho=1/2$, a check that could have failed. Downstream, rho_pinned_at_witness specializes to a concrete nonzero TT witness and thereby refutes every $\rho\neq 1/2$.
The module narrative is that the factor of two between continuum $-1/8$ and the frozen preflight $-1/4$ is exactly Regge's normalization: both numbers are correct faces of different actions. The discrete bookkeeping factor $2=1/\rho$ is therefore derived, not assumed, so the historical gate mismatch was a functional mismatch, not a Regge error. Independent Gauss-Bonnet checks on triangulated spheres (§6) corroborate the same constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.