NormalizationGateDischarged
plain-language theorem explainer
Six-conjunct gate proposition asserting that Regge's free normalization constant is forced to 1/2: full TT dictionary match, uniqueness at a witness polarization, refutation of ρ=1, banked midpoint value −1/4, and Gauss–Bonnet on spheres. Cited by anyone discharging the historical normalization gate or packaging Arc-2 step 7. Pure Prop definition; the discharge theorem builds the six proofs separately.
Claim. The following hold simultaneously: (i) for every transverse-traceless $4\times 4$ metric perturbation $H$ and Euclidean wave covector $k$, the Regge face at the derived normalization equals the exact midpoint Bloch $m^2$ coefficient of $H,k$; (ii) any real $\rho$ for which that face equality holds on the plus-polarization witness forces $\rho=1/2$; (iii) $\rho=1$ fails on that witness; (iv) the midpoint coefficient there equals $-1/4$; (v) $4\pi$ equals the derived normalization times the triangulated-sphere Einstein–Hilbert integral; (vi) $4\pi$ is not equal to $1$ times that integral.
background
Arc 2, step 7 of the gravity analysis compares two second-variation faces of curvature actions in 4D. From the Levi-Civita connection alone, the continuum side yields a phase-averaged Einstein–Hilbert face
$$ehFace(H,k)=-(1/4),|k|^2,|H|_F^2$$
on real transverse-traceless cosine waves. The discrete side is the Regge action $\sum_h A_h\delta_h$ (area times deficit), related to $\int R\sqrt{g}$ by a free classical constant $\rho$ via $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$. Historically $\rho=1/2$ is assumed; this module leaves $\rho$ free.
A wave is a map $k:\mathrm{Fin},4\to\mathbb{R}$. Algebraic TT means symmetric, Euclidean-traceless, and transverse to $k$. The plus witness is the unnormalized polarization $\mathrm{diag}(0,0,1,-1)$ against the axis wave $(1,0,0,0)$. The exact midpoint Bloch $m^2$ is the cosine two-jet coefficient of the centered Regge symbol. The Regge face is that discrete second variation scaled by a free $\rho$; the derived normalization is the value this module pins.
The older Boolean gate always reported success. This proposition replaces it by equations and refutations over the actual constants, so changing any coefficient in the tree breaks a conjunct.
proof idea
Definition only: the body is the six-fold conjunction written out as a Prop, with no tactics and no proof term. Each conjunct names an equality or inequality already established (or to be established) by sibling lemmas: universal TT match of the Regge face at the derived normalization against the midpoint Bloch symbol; uniqueness of $\rho$ at the plus/axis witness; failure of $\rho=1$ there; the numerical witness value $-1/4$; and the two Gauss–Bonnet comparisons $4\pi=\rho_{\mathrm{der}}\cdot I_{S^2}$ versus $4\pi\neq 1\cdot I_{S^2}$. Discharge is deferred to the theorem that inhabits this Prop.
why it matters
This is the discriminating replacement for the non-discriminating historical normalization gate. The module result is that the factor-of-two gap between the banked discrete face $-(1/8)$ and the continuum face $-(1/4)$ is exactly Regge's $\rho=1/2$ (equivalently discrete bookkeeping factor $1/\rho=2$): both numbers are correct faces of different functionals, so the old gate failed from comparing unequal actions, not from a wrong Regge computation.
Downstream, the theorem normalizationGateDischarged inhabits this Prop by packaging the six sibling proofs. Step7Cert conjoins it with the continuum phase-average identity, the bookkeeping reciprocity, and the frozen-preflight coefficient check, so the whole of step 7 is one proposition. The typed naming-defect residual records that a legacy continuum-face name still returns the EH face rather than the Regge face; readers are pointed here instead.
In the broader RS gravity stack this closes A4 (the fourth classical input) without assuming $\rho$, and keeps the discrete/continuum dictionary honest before later curvature or mass-ladder work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.