rho_one_fails
plain-language theorem explainer
At the plus-polarization TT witness against the axis wave, the discrete Regge face with free constant ρ equal to 1 disagrees with the banked exact-midpoint Bloch second-variation value. Gravity analysts deriving Regge's continuum normalization cite this as Discrimination 2: the frozen preflight's implicit ρ=1 is refuted, not merely left open. The proof rewrites both sides to explicit rationals via the face and dictionary lemmas, then closes by norm_num.
Claim. Let $H_+$ be the unnormalized plus TT polarization $\mathrm{diag}(0,0,1,-1)$ and let $k$ be the axis wave covector $(1,0,0,0)$. Then the Regge face at free constant $\rho=1$ on $(H_+,k)$ is not equal to the exact midpoint Bloch $M_2$ dictionary value on the same pair: $\mathrm{reggeFace}(1; H_+,k) \neq M_2^{\mathrm{Bloch}}(H_+,k)$.
background
Arc 2, step 7 of the gravity analysis derives Regge's continuum normalization rather than assuming it. ContinuumTTSecondVariation4D shows that the phase-averaged second variation of $\int R\sqrt{g}$ per unit volume on a real transverse-traceless cosine wave is $\mathrm{ehFace}(H,k)=-(1/4),|k|^2,|H|_F^2$, obtained from the Levi-Civita connection alone with no Regge input.
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\cdot\int R\sqrt{g}$ with $\rho=1/2$. This module leaves $\rho$ free: reggeFace is the discrete second-variation face scaled by $\rho$, while exactMidpointBlochM2 is the banked dictionary value of the continuum/Bloch side at the exact midpoint.
The witness pair is fixed: axisTTPlus is the plus polarization $\mathrm{diag}(0,0,1,-1)$, and axisWave is the covector $(1,0,0,0)$. Sibling lemmas pin Frobenius and wave norms of that pair, and dictionary_witness_value records the numerical dictionary entry used for comparison.
proof idea
Term-mode proof by rewriting both sides to concrete rationals, then a numerical check. Rewrite reggeFace 1 via reggeFace_eq (expands the free-$\rho$ face into $\rho$ times the discrete bookkeeping combination of Frobenius and wave norms). Substitute dictionary_witness_value for the Bloch $M_2$ side. Unfold frobeniusNormSq_axisTTPlus and waveNormSq_axisWave to their explicit values on the witness. The resulting rational inequality is discharged by norm_num.
why it matters
Discrimination 2 in the module's pinning arc: $\rho=1$ is what a naive comparison of the discrete Regge action against $\int R\sqrt{g}$ assumes, and what the frozen preflight implicitly used. Refuting it at the witness shows the historical gate failure was a functional mismatch (two different actions), not an error in the Regge computation.
Downstream, normalizationGateDischarged packages this with the positive pinning $\rho=1/2$, the dictionary witness value, the face-equals-dictionary identity, and the independent Gauss-Bonnet check on triangulated spheres. Together they discharge the normalization gate: the factor of two between continuum $-(1/4)$ and discrete $-(1/8)$ is exactly $1/\rho$ with $\rho=1/2$, so discreteBookkeepingFactor := 2 is derived rather than postulated.
In the broader Recognition gravity stack this closes the classical A4 input (Regge normalization) without smuggling continuum conventions into the discrete side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.