Step7Cert
plain-language theorem explainer
Packages every claim of Arc 2 step 7 as a single proposition: normalization gate discharged, continuum phase-average identity for the Einstein-Hilbert face, bookkeeping factor times Regge normalization equals one, dictionary match of that face to the frozen preflight coefficient, and two Gauss-Bonnet deficit checks on triangulated spheres. Downstream theorem step7Cert is the witness. Pure definitional conjunction with no proof content.
Claim. The conjunction of six statements: the normalization gate is discharged; for every $4\times 4$ matrix $H$ and wave covector $k$, the phase average of the second-variation Lagrangian density equals the continuum Einstein-Hilbert face $\mathrm{eh}(H,k)=-(1/4)|k|^2\|H\|_F^2$; the discrete bookkeeping factor times the Regge normalization constant equals $1$; that continuum face equals the frozen preflight EH coefficient times $\|H\|_F^2|k|^2$; and the spherical deficit identities $4(2\pi-3\cdot\pi/3)=4\pi$ and $6(2\pi-4\cdot\pi/3)=4\pi$.
background
Arc 2, step 7 of the Regge-to-continuum bridge. From the Levi-Civita connection alone, the continuum module derives that the phase average (per unit volume) of $d^2/dt^2\int R\sqrt{g}$ on a real transverse-traceless cosine wave is the Einstein-Hilbert face $\mathrm{eh}(H,k)=-(1/4),|k|^2,|H|F^2$. Here the phase average is the mean of a phase function over one period $[0,2\pi]$, the Frobenius squared norm is $\sum{i,j}H_{ij}^2$, and the wave norm is the squared Euclidean length of the covector $k$.
The discrete side is the Regge action $\sum_h A_h\delta_h$ (area times deficit), related to the continuum integral by a free normalization $\rho$ via $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$. Classical literature takes $\rho=1/2$; the frozen preflight effectively used $\rho=1$. This module leaves $\rho$ free and asks what constant the dictionary forces.
The shifted cost $H(x)=J(x)+1$ appears only as ambient algebra infrastructure and is not used in the geometric content of the certificate.
proof idea
Definitional packaging only: a six-fold conjunction of named atomic propositions and closed real identities. No tactics, no lemmas applied at this declaration. The witness theorem later discharges each conjunct by name (normalization gate, Lagrangian-route face identity, bookkeeping-factor inverse, frozen-preflight coefficient match, and the two tetrahedron/octahedron-style deficit sums).
why it matters
This is the single Prop that step 7 must establish. The parent theorem step7Cert proves it, closing the second half of Arc 2 step 7: continuum EH second variation beside the banked Regge dictionary, with Regge's normalization $\rho=1/2$ forced rather than assumed. The factor of two between the continuum face $-(1/4)$ and the historical frozen $-(1/8)$ is exactly $1/\rho$; both numbers are correct faces of different actions. The two spherical identities independently check $\rho=1/2$ against Gauss-Bonnet on triangulated $S^2$ (4 triangular faces; 6 square-equivalent deficits). Downstream, discharging this certificate shows the historical gate failed because the two sides varied different functionals, not because the Regge Hessian was wrong.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.