IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4DAudit
Audit layer over the exact second variation of the Einstein–Hilbert action in four dimensions. It checks that the continuum identity equating the second t-derivative of ∫√g R to −∫ hμν G⁽¹⁾μν (hypothesis A3 in step 7) carries no hidden numerical factor. Gravity analysts tracing the arc-2 coefficient chain to the face −(1/4)|k|²‖H‖²_F would cite it. Structure is import-and-audit of the exact-variation development, not a new derivation.
claimAudit of the exact second variation of the Einstein–Hilbert functional $S[g]=\int \sqrt{g}\,R$ in $4$D, focused on the continuum identity $\frac{d^2}{dt^2}\big|_{t=0}\int\sqrt{g_t}R[g_t]=-\int h_{\mu\nu}G^{(1)\mu\nu}$ (step-7 input A3) and on whether any free coefficient remains between that identity and the face $-\frac14|k|^2\|H\|_F^2$.
background
Step 7 of the continuum TT second-variation arc produces the Einstein–Hilbert face $-\frac14|k|^2|H|_F^2$ from four inputs. Three are already formalized: A1 (linearized Levi-Civita connection), A2 (linearized Ricci), and Regge’s normalization. The fourth, A3, asserts
$$\frac{d^2}{dt^2}\int\sqrt{g},R=-\int h_{\mu\nu}G^{(1)\mu\nu}$$
and was only stated, not derived, in ContinuumTTSecondVariation4D. Upstream work on the exact second variation of $\int\sqrt{g}R$ exists to close that gap; the present module is the audit face of that development.
In the Recognition gravity stack this sits inside the continuum coefficient chain that must match discrete curvature weights. Any residual scalar in A3 would rescale the face and break the match to the discrete side.
proof idea
This is an audit module, not a primary derivation. It imports the exact-second-variation development and organizes checks that A3 holds with coefficient exactly $1$ (no hidden factor) in four dimensions, and that the passage from that identity through the linearized Einstein tensor to the continuum face $-\frac14|k|^2|H|_F^2$ is coefficient-clean. Expect statement-level audits, normalization cross-checks against Regge’s convention, and pointers back to the formalized A1/A2 pieces rather than a fresh variational calculation.
why it matters in Recognition Science
A3 is called out upstream as “the one place in arc 2’s coefficient chain where a factor could still hide.” Closing or auditing that slot is required before the continuum EH face can be treated as forced rather than fitted. The module therefore guards the integrity of step 7’s output $-\frac14|k|^2|H|_F^2$, which later gravity results compare to discrete curvature and to the Recognition forcing chain’s geometric side (D = 3 spatial dimensions, eight-tick structure entering the continuum limit). No downstream Lean consumers are recorded yet; the scientific parent is the step-7 coefficient theorem and any uniqueness claim for the EH face.
scope and limits
- Does not re-derive the exact second variation; audits the existing development.
- Does not prove A1 or A2; those are assumed already formalized upstream.
- Does not address dimensions other than 4D continuum.
- Does not fix discrete-to-continuum matching beyond the A3 coefficient check.
- Does not claim a new numerical value for the EH face beyond −(1/4)|k|²‖H‖²_F.