normalizationGateDischarged
plain-language theorem explainer
The Regge normalization gate is fully discharged: the discrete face at ρ = 1/2 matches the banked midpoint Bloch M2 dictionary on every TT mode, ρ is uniquely pinned to 1/2 at the witness, ρ = 1 is refuted, the witness value is −1/4, and Gauss–Bonnet independently forces the same ρ. Gravity analysts comparing continuum EH second variation to Regge area–deficit bookkeeping cite this. Proof is a six-field term packing prior lemmas.
Claim. The normalization gate holds: for every transverse-traceless pair $(H,k)$, the Regge face at the derived constant $\rho=1/2$ equals the exact midpoint Bloch $M_2$ dictionary value; any $\rho$ matching the dictionary at the axis witness equals $1/2$; the face at $\rho=1$ fails that match; the witness dictionary value is $-1/4$; and Gauss–Bonnet on the sphere gives $4\pi=\rho\,I_{\mathrm{EH}}$ at $\rho=1/2$ while refuting $\rho=1$.
background
Arc 2, step 7 (second half) places the continuum TT second variation beside the banked discrete dictionary and asks which constant relates them. From the Levi-Civita connection alone, the phase average of $d^2/dt^2\int R\sqrt{g}$ per unit volume on a real TT cosine wave is $\mathrm{ehFace}(H,k)=-(1/4),|k|^2,|H|_F^2$. The discrete object is the Regge action $\sum_h A_h\delta_h$ (area times deficit), related to the Einstein–Hilbert integral by $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$. Classically $\rho=1/2$; this module leaves $\rho$ free.
The proposition NormalizationGateDischarged packages six claims: universal agreement of the Regge face at the derived $\rho$ with the midpoint Bloch $M_2$ dictionary on TT modes; uniqueness of $\rho=1/2$ at the axis witness; failure of $\rho=1$; the nonzero witness value $-1/4$; and the Gauss–Bonnet identity $4\pi=\rho,I_{\mathrm{EH}}$ together with its $\rho=1$ refutation. Upstream, dictionary_witness_value evaluates the dictionary on the axis TT-plus mode to $-1/4$, and gauss_bonnet_refutes_rho_one shows both triangulated spheres give deficit sum $4\pi$, not $8\pi$.
proof idea
Term-mode constructor for the six-conjunct proposition. The first field is the lambda fun H k hTT => reggeFace_eq_dictionary H k hTT, the universal TT agreement at the derived Regge constant. The remaining five fields are direct citations: rho_pinned_at_witness (uniqueness of $\rho=1/2$ at the axis), rho_one_fails (disequality at $\rho=1$), dictionary_witness_value (witness equals $-1/4$), regge_constant_from_gauss_bonnet ($4\pi=\rho,I_{\mathrm{EH}}$ at the derived $\rho$), and gauss_bonnet_refutes_rho_one ($4\pi\neq 1\cdot I_{\mathrm{EH}}$). No further rewriting; the gate is the conjunction of already-proved faces.
why it matters
Closes the second half of Arc 2 step 7: the historical factor-of-two mismatch between the continuum face $-1/4$ and the banked discrete face $-1/8$ is Regge's normalization, not an error on either side. Both constants are correct faces of different functionals; discreteBookkeepingFactor := 2 is $1/\rho$ and is now derived. Downstream, step7Cert consumes this theorem as its first conjunct, bundling the discharged gate with the Lagrangian-route same-face claim, the inverse-Regge bookkeeping identity, the frozen-preflight EH-face identification, and the tetrahedron deficit sum. Within the gravity analysis stack this is the point where continuum EH second variation and discrete Regge area–deficit calculus are reconciled without assuming $\rho$ a priori, and where $\rho=1$ (the frozen preflight's implicit choice) is ruled out both by the dictionary witness and by Gauss–Bonnet on two spheres.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.