a3_agrees_with_exact
plain-language theorem explainer
At Frobenius-normalized TT metric data with square 2, the wavelength average of the exact continuum TT second-variation density equals the average of the phase density that step 7 treats as A3's right-hand side. Coefficient auditors in the continuum gravity chain cite this to confirm A3 does not shift the Einstein-Hilbert face factor. The proof is a two-step rewrite through the exact-average-equals-face lemma and the face-equals-phase-average identity.
Claim. For any $4\times 4$ matrix $H$ with Frobenius square $\|H\|_F^2=2$ and any momentum $k$, the wavelength average of the exact transverse-traceless second-variation density at $|k|^2$ equals the wavelength average of the A3 phase density built from $(H,k)$.
background
Step 7 of the continuum gravity arc derives the Einstein-Hilbert face $-(1/4)\cdot|k|^2\cdot|H|F^2$ from four inputs. Three (linearized Levi-Civita, linearized Ricci, Regge normalization) are formalized. The fourth, A3, asserts that the second $t$-derivative of $\int\sqrt{g},R$ equals $-\int h{\mu\nu}G^{(1)\mu\nu}$. That identity was stated and used in the continuum TT second-variation module without a Lean derivation; it is the remaining place a hidden overall factor could sit.
This module works at the base witness family $g_{\mu\nu}(t)=\delta_{\mu\nu}+t H_{\mu\nu}\cos(\kappa z)$ in Euclidean 4D. The exact density is the closed-form $d^2/dt^2(\sqrt{\det g},R)|_{t=0}$ obtained off-kernel by full (unexpanded) curvature; its TT specialization and wavelength average are the objects compared here. The phase density is the continuum expression ContinuumTTSecondVariation4D feeds as A3's right-hand side.
Upstream, the sibling exact-average-equals-face result already identifies the exact TT average with the derived EH face under $|H|_F^2=2$. The face-equals-phase-average identity identifies that same face with the average of the A3 phase density.
proof idea
Term-style two-rewrite proof. First apply the sibling lemma that, under Frobenius square 2, the wavelength average of the exact TT density equals the Einstein-Hilbert face value. Then rewrite by the identity that equates that face to the wavelength average of the A3 phase density of $(H,k)$. No further algebra or case splits.
why it matters
Closes the A3 coefficient gap in arc 2: step 7's assumed right-hand side and the exact left-hand side share the same wavelength average at the witness, so the assumption does not move the overall normalization of the density. The module doc records that the exact curvature itself remains DERIVED-UNFORMALIZED (symbolic receipt, not a kernel theorem); this declaration only transports the closed form into Lean averages.
Sibling discrimination results (trace decoy of opposite sign at the same Frobenius square) show the face formula is TT-specific and not a fit-anything identity. No downstream consumers are wired yet; the natural parents are any theorem that quotes the continuum EH face coefficient as fully normalized. Framework landmark: continuum limit of the gravity sector after the forcing chain has already fixed $D=3$ spatial dimensions and the eight-tick structure upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.