provenance
plain-language theorem explainer
A fixed provenance string for the exact Einstein-Hilbert second-variation module. It records, for a referee, which wavelength-average and face-identification facts are proved in Lean, which exact curvature identities live only in an external symbolic script, and which RS machinery is deliberately unused. Anyone citing the A3 normalization check or the TT face match should quote this ledger. The body is a string literal, not a proof.
Claim. A constant string that states: (i) Lean derives the wavelength averages, the match of the exact transverse-traceless density average to step 7's Einstein-Hilbert face $-\frac14 |k|^2 \|H\|_F^2$, agreement of that average with A3's right-hand side, failure of pure-trace and longitudinal decoys of the same Frobenius mass to hit the face, and coefficient rigidity under rescaling; (ii) symbolic algebra (not Lean) derives $d^2/dt^2(\sqrt{\det g}\, R)|_{t=0}=\kappa^2(7\sin^2-4)$ on the plus polarization and A3 agreement at five witnesses; (iii) the Regge tree, coupling table, Bloch symbol, norm gate, and banked coefficients are unused here.
background
The module sits in the gravity analysis arc that closes the continuum Einstein-Hilbert face used at step 7. Step 7 obtained $-\frac14 |k|^2 |H|F^2$ from four inputs: linearized Levi-Civita (A1), linearized Ricci (A2), Regge normalization, and A3, the identity $d^2/dt^2 \int \sqrt{g}, R = -\int h{\mu\nu} G^{(1)\mu\nu}$. A1–A2 and the normalization are formalized elsewhere; A3 was only stated and used in the continuum TT second-variation development, so it was the remaining place a hidden overall factor could sit.
Off Lean, a symbolic script builds the full inverse metric, Christoffels, Ricci, and scalar curvature for $g_{\mu\nu}(t)=\delta_{\mu\nu}+t H_{\mu\nu}\cos(\kappa z)$ with no expansion in $t$, then compares $d^2/dt^2(\sqrt{\det g}, R)$ at $t=0$ to $-\int h\cdot G^{(1)}$. On plus and cross polarizations the wavelength average is exactly the derived face; A3 holds at TT and non-TT witnesses; a transverse pure trace of the same Frobenius mass averages to the opposite sign. Exact curvature is therefore tagged derived-unformalized.
This declaration does not restate those theorems. It is the human-readable ledger of what the module claims versus what it refuses to claim.
proof idea
No mathematical proof. The declaration is a String definition whose body is a multi-line literal enumerating three buckets: facts derived in Lean (wavelength averages, exact-density average equals the step-7 face, agreement with A3's RHS, decoy failures, rescaling rigidity), facts derived only in the external symbolic script (closed-form second derivative on the plus polarization; A3 checks at five witnesses), and machinery explicitly not used (Regge tree, coupling table, Bloch symbol, norm gate, banked coefficients). Downstream code can quote the string; nothing is proved by inhabiting it.
why it matters
In Recognition Science the continuum EH face normalizes the density that feeds the coefficient chain after the forcing landmarks (J-uniqueness, $\phi$, eight-tick structure, $D=3$). Without a clear split between Lean theorems and external algebra, a referee could misread A3 as kernel-proved or as smuggling a banked factor. This provenance string is the audit trail for that split inside the exact-second-variation module.
It is widely referenced as a documentation hook across constants and cosmology (alpha-derivation provenance patterns, baryogenesis reprocessing factors, entropy-per-photon formula provenance, EW scale positivity, fermion weight ratios). Those uses treat "provenance" as the pattern of refusing typed-in magic numbers; here the same discipline is applied to the gravity face. The open gap it advertises is the still-unformalized exact curvature computation: Lean owns averages and face identification downstream of the closed form, not the full $t$-exact Ricci algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.