step7Cert
plain-language theorem explainer
Packages the full Arc-2 step-7 certificate for 4D Regge normalization: the normalization gate is discharged, the Lagrangian phase average equals the Einstein-Hilbert TT face, the discrete bookkeeping factor is the inverse of Regge's ρ = 1/2, the frozen preflight coefficient is exactly that EH face, and the tetrahedron/octahedron Gauss-Bonnet deficit sums hold. Gravity analysts reconciling continuum TT second variation with the Regge dictionary cite it. Proof is a term-mode 6-tuple of already-proved conjuncts.
Claim. The step-7 certificate holds: the normalization gate is discharged; for every $4\times 4$ metric perturbation $H$ and wave covector $k$, the phase average of the Lagrangian density equals the Einstein-Hilbert face $\mathrm{ehFace}(H,k)$; the discrete bookkeeping factor times Regge's normalization $\rho$ equals $1$; $\mathrm{ehFace}(H,k)$ equals the frozen preflight coefficient times $\|H\|_F^2\,|k|^2$; and the tetrahedron and octahedron deficit identities $4(2\pi-3\cdot\pi/3)=4\pi$ and $6(2\pi-4\cdot\pi/3)=4\pi$ hold.
background
Arc 2, step 7 (second half) sits the continuum Einstein-Hilbert TT second variation next to the banked Regge dictionary and asks what constant relates them. From the Levi-Civita connection alone, with no Regge input, the phase average of $d^2/dt^2\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$.
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 $\rho=1/2$. This module does not assume $\rho$: it leaves it free, shows the dictionary forces $\rho=1/2$, refutes $\rho=1$ (the frozen preflight's implicit choice), and checks $\rho=1/2$ independently via Gauss-Bonnet on two triangulated spheres.
Step7Cert is the single proposition collecting every claim of that arc: gate discharge, Lagrangian route equals EH face, bookkeeping factor times $\rho$ is 1, frozen preflight is the EH integral face, and the two deficit-sum identities.
proof idea
Term-mode constructor for the six-conjunct proposition. Each field is an already-proved sibling:
normalizationGateDischarged(dictionary match on TT waves, $\rho$ pinned at the witness, $\rho=1$ fails, witness value, Gauss-Bonnet constant).lagrangian_route_same_face: unfold densities, apply phase-average of $\sin^2$, Frobenius and momentum identities, then ring.discreteBookkeepingFactor_is_inverse_regge: unfold $\rho$, rewrite the bookkeeping factor as 2,norm_num.frozen_preflight_is_the_eh_integral_face: unfold EH face and the frozen coefficient to the same TT symbol. 5–6.tetrahedron_deficit_sumandoctahedron_deficit_sum: the two sphere Gauss-Bonnet checks that independently force $\rho=1/2$.
No new algebra; pure packaging.
why it matters
Closes Arc 2 step 7: the historical factor-of-two mismatch between continuum $-(1/8)$ and frozen $-(1/4)$ is Regge's normalization constant, not a failed computation. Both numbers are correct faces of different actions; discreteBookkeepingFactor := 2 is $1/\rho$ and is derived. The gate failed because the two sides varied different functionals.
Downstream use is presently empty in the graph; the certificate is the terminal status object for this module. It sits in the gravity analysis chain that reconciles continuum TT second variation (ContinuumTTSecondVariation4D) with the Regge exact midpoint identity, and it discharges the classical A4 input ($\rho=1/2$) without assuming it. Framework-wise it is classical GR bookkeeping inside the RS gravity stack, not a T0–T8 forcing step, but it removes a long-standing obstruction to reading the Regge dictionary as a derived face of the Einstein-Hilbert action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.