rsNullFieldReductionCert
plain-language theorem explainer
Packages three algebraic facts into one certificate for the RS null-field reduction: every scalar multiple of the Minkowski metric vanishes under null quadratic contraction, an Einstein-shaped source at the RS coupling reduces to Ric(k,k)=κ T(k,k) on null probes, and the metric term is invisible to those probes. Gravity workers on the Clausius–Einstein bridge cite it as the matrix-level reduction package. Term-mode assembly of three already-proved lemmas.
Claim. The following three statements hold simultaneously: (i) for every real $f$ and every Minkowski-null $k\in\mathbb{R}^4$, the quadratic contraction of $f\,\eta$ against $k$ is zero; (ii) if $(T,\mathrm{Ric})$ is an Einstein-shaped source at the RS coupling $\kappa_{\mathrm{E}}$, then for every null $k$ one has $\mathrm{Ric}(k,k)=\kappa_{\mathrm{E}}\,T(k,k)$; (iii) there exists a nonzero $4\times 4$ matrix $D$ with $\mathrm{quadContr}(D,k)=0$ for all null $k$ (the scalar metric term is not recovered from null data).
background
The module treats the purely algebraic passage from an independently supplied Einstein-shaped matrix equation to its null-contracted scalar form. One assumes a matrix identity of the shape $\kappa T=\mathrm{Ric}+f,\eta$ on $\mathrm{Mat}_4(\mathbb{R})$, with $\eta$ the Minkowski metric. A probe vector $k$ is Minkowski-null when its quadratic form against $\eta$ vanishes. Quadratic contraction $\mathrm{quadContr}(A,k)$ is the scalar $k^\top A k$.
Under those hypotheses the metric term drops out on null probes, leaving $\mathrm{Ric}(k,k)=\kappa T(k,k)$. The RS specialization fixes the coupling to the constant $\kappa_{\mathrm{E}}$ imported from the constants module. The certificate structure simply names the three algebraic claims that make this reduction honest: vanishing of metric terms, reduction of the source, and non-recoverability of the metric term from null data alone.
Upstream, quadContr_metric_term_eq_zero proves every scalar multiple of $\eta$ contracts to zero on null $k$; rs_null_scalar_of_source specializes the general null-scalar lemma to $\kappa_{\mathrm{E}}$; scalar_metric_term_is_null_invisible exhibits a nonzero matrix (namely $\eta$ itself) invisible to all null contractions.
proof idea
Term-mode inhabitant of the certificate structure. The three fields are filled by direct reference to the three upstream theorems: metric-term vanishing is quadContr_metric_term_eq_zero, source reduction is rs_null_scalar_of_source (itself a one-line specialization of the general null-scalar lemma at $\kappa_{\mathrm{E}}$), and non-recoverability is scalar_metric_term_is_null_invisible. No extra algebra is performed at this site.
why it matters
Closes the matrix-level RS null reduction package inside the Gravity domain. The module doc is explicit that this is a conditional algebraic step, not a derived field equation: inhabiting the Einstein-shaped source from the RS action remains an external open input, and the file deliberately names every public declaration as a reduction rather than a sourced field equation. No downstream consumers are wired yet; the certificate is the stable interface those consumers will import once the Clausius–Einstein bridge or a horizon-patch construction needs a single named Prop for the null reduction. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or the phi-ladder mass formula; its role is strictly the gravity-side null contraction algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.