provenance
plain-language theorem explainer
A single provenance string for the continuum TT second-variation module: it lists what is derived (linearized Christoffel and Ricci, TT reduction, Mathlib plane-wave derivatives, cos² mean 1/2, and the face −(1/4)|k|²‖H‖²_F) versus what is assumed (A3: second time derivative of ∫√g R equals −∫ h·G⁽¹⁾). Anyone auditing Arc 2 step 7 cites it to separate proved continuum calculus from the classical Euler identity. The body is a literal documentation string, not a proof.
Claim. The module records a fixed provenance tag: derived are the linearized Christoffel symbols, linearized Ricci, transverse-traceless reduction, plane-wave derivatives from the standard derivative calculus, the mean $\langle\cos^2\rangle=1/2$, and the continuum face value $-\frac14 |k|^2 \|H\|_F^2$ for $\frac{d^2}{dt^2}\int R\sqrt{g}$ per unit volume on a real cosine wave $h=H\cos(k\cdot x)$; assumed is only A3, namely $\frac{d^2}{dt^2}\int\sqrt{g}R=-\int h\cdot G^{(1)}$; the coupling table, Bloch symbol, norm gate, and preflight coefficients are unused.
background
Arc 2, step 7 of the gravity analysis derives the continuum transverse-traceless second variation of the Einstein–Hilbert integrand $\int R\sqrt{g}$ in four dimensions, in the same real-cosine convention used by the banked Regge midpoint dictionary. The discrete side averages $d^2/dt^2$ of the Regge action under $h(x)=H\cos(k\cdot x)$; the continuum object here is the matching phase average per unit volume, not the bare quadratic Taylor coefficient (which would differ by another factor of 2).
Named classical inputs begin with A1, the linearized Levi-Civita Christoffel symbol $\Gamma^{(1)}{\lambda\mu\nu}=\frac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$, and continue through linearized Ricci and TT reduction. The module imports only Mathlib and a pure linear-algebra edge decomposition; it deliberately does not import the coupling table, Bloch symbol, norm gate, or preflight, so the continuum number cannot have been read from the discrete answer.
The provenance string exists so a reader who never saw the write-up cannot mistake the tag: which faces are derived calculus, and which single classical identity remains an assumption.
proof idea
There is no proof. The declaration is a string definition whose body is a fixed English inventory: DERIVED lists A1, A2, TT reduction, plane-wave derivatives obtained from Mathlib's deriv (not asserted), the cos-squared mean $1/2$, and the resulting continuum face $-\frac14|k|^2|H|_F^2$; ASSUMED names only A3 (Euler's theorem for a quadratic form together with $\delta(\sqrt{g}R)/\delta g=-\sqrt{g}G$); NOT USED ANYWHERE HERE excludes the coupling table, Bloch symbol, norm gate, preflight, and every existing coefficient in the tree.
why it matters
The module exists because ReggeExactFlatHessianNormGate4D bridged a computed discrete $-1/8$ to a frozen preflight $-1/4$ by a bare discreteBookkeepingFactor := 2 with no derivation. Step 6 refuted the cheap Frobenius-square explanation at a normalized polarization, so the honest move is an independent continuum derivation. This provenance tag is the audit handle for that independence: it freezes, in one place, what the continuum calculus actually delivers versus the single classical assumption A3.
Downstream comparison against the Regge dictionary lives in the separate module ReggeNormalizationDerived4D. Within Recognition gravity, the face value $-\frac14|k|^2|H|_F^2$ is the continuum number that must be reconciled with the discrete Hessian before any claim about the Einstein–Hilbert second variation on TT waves is banked. The string does not itself close that comparison; it prevents silent circularity while the comparison is written.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.