RSNullFieldReductionCert
plain-language theorem explainer
Certificate packaging three matrix-level facts for the RS null reduction: the pure metric term vanishes on every Minkowski-null vector, an Einstein-shaped source with coupling κ_Einstein reduces to Ric(k,k)=κ T(k,k) on null directions, and that metric term is invisible to null data (a nonzero kernel exists). Gravity workers citing the algebraic step from κT=Ric+fη to the null scalar equation use this Prop. It is a definitional bundle; the inhabiting theorem wires three sibling lemmas into the fields.
Claim. A proposition-valued certificate with three clauses: (1) for every scalar $f$ and every Minkowski-null $k\in\mathbb{R}^4$, the quadratic contraction $(f\,\eta)(k,k)=0$; (2) if $\kappa T=\mathrm{Ric}+f\eta$ holds for the Einstein coupling $\kappa$, then $\mathrm{Ric}(k,k)=\kappa\,T(k,k)$ for every null $k$; (3) there exists a nonzero matrix $D$ such that $D(k,k)=0$ for all Minkowski-null $k$ (the metric term is not recoverable from null contractions alone).
background
The module treats a purely algebraic reduction: given an independently supplied Einstein-shaped matrix equation, contract both sides against a Minkowski-null vector and drop the undetermined metric term. Honesty tags in the module doc mark the matrix algebra as theorem content and the inhabitation of the source interface from the RS action as open/external.
An Einstein-shaped source at coupling $\kappa$ means there exists a scalar $f$ with $\kappa,T=\mathrm{Ric}+f,\eta$, where $\eta$ is the standard $(-,+,+,+)$ Minkowski metric on $\mathbb{R}^4$. The quadratic contraction is $A(k,k)=A_{\mu\nu}k^\mu k^\nu$. The RS specialization fixes $\kappa=\kappa_{\mathrm{Einstein}}=8\pi G/c^4$, which in RS-native units ($c=1$, $G=\phi^5/\pi$, $\hbar=\phi^{-5}$) equals $8\phi^5$.
Null directions are those $k$ with $\eta(k,k)=0$. On such $k$ the pure metric contribution $f,\eta(k,k)$ is identically zero, so the sourced equation collapses to a scalar relation between $\mathrm{Ric}$ and $T$.
proof idea
Definitional Prop structure, not a proved theorem. The three fields are named hypotheses whose mathematical content is exactly the three clauses above. No tactics or term proof live here; the body is empty.
The downstream inhabiting theorem fills the fields by direct assignment: metric-term vanishing from the sibling lemma that $(f,\eta)(k,k)=0$ on null $k$; source reduction from the RS-specialized null-scalar-of-source lemma (coupling fixed to $\kappa_{\mathrm{Einstein}}$); non-recovery from the existence lemma that exhibits a nonzero null-invisible matrix. Each field is therefore a one-line wrapper onto an already-proved sibling.
why it matters
This certificate is the public interface for the matrix-level RS null reduction. The sole downstream consumer is the inhabiting theorem that assembles the three sibling lemmas into a single Prop value, giving later gravity developments a single named handle rather than three separate facts.
In the Recognition framework it sits under the gravity bridge that connects an assumed Einstein-shaped source to a null-contracted scalar equation with the RS coupling $\kappa=8\phi^5$. It does not itself touch the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder; those enter only indirectly via the constants module that supplies $\kappa_{\mathrm{Einstein}}$.
The module doc is explicit about the open gap: inhabiting the Einstein-shaped source from the RS action remains external. The certificate therefore records what the algebra delivers once that source is granted, and records that the metric term is information-theoretically lost under null contraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.