rs_null_scalar_of_source
plain-language theorem explainer
Given an Einstein-shaped matrix source at the RS coupling κ, every Minkowski-null contraction collapses to Ric(k,k) = κ T(k,k). Gravity and Clausius-bridge workers cite it when reducing a matrix field equation to its null-scalar form. The proof is a one-line specialization of the generic null-scalar reduction at κ = kappa_einstein.
Claim. Let $T$ and $\mathrm{Ric}$ be $4\times 4$ real matrices. Suppose there exists a scalar $f$ such that $\kappa T = \mathrm{Ric} + f\,\eta$, where $\kappa$ is the Einstein coupling and $\eta$ is the Minkowski metric. Then for every four-vector $k$ with $\eta(k,k)=0$, one has $\mathrm{Ric}(k,k) = \kappa\, T(k,k)$.
background
The module isolates one algebraic step: from an independently supplied Einstein-shaped matrix equation to its null-contracted scalar equation. An Einstein-shaped source at coupling $\kappa$ means $\exists f\in\mathbb{R}$ with $\kappa,T = \mathrm{Ric} + f,\eta_4$, where $\eta_4$ is the standard $(-,+,+,+)$ Minkowski matrix. This interface is an external input, not a derivation from the RS action.
Nullness is the usual Minkowski condition $\eta(k,k)=0$. The quadratic contraction $\mathrm{quadContr}(A,k)=A_{\mu\nu}k^\mu k^\nu$ is the bilinear form used throughout the Clausius-Einstein bridge. The RS coupling is $\kappa=\texttt{kappa_einstein}=8\pi G/c^4$, which in RS-native units ($c=1$, $G=\phi^5/\pi$) equals $8\phi^5$.
On any null $k$ the pure-metric term $f,\eta(k,k)$ vanishes, so the matrix identity collapses to a scalar equality between $\mathrm{Ric}$ and $T$.
proof idea
One-line wrapper that applies the generic lemma null_scalar_of_source at the fixed coupling kappa_einstein. That upstream lemma unpacks the existential witness $f$ in EinsteinShapedSource, uses bilinearity of the quadratic contraction, and cancels the metric term via quadContr_metric_term_eq_zero on every Minkowski-null direction.
why it matters
Feeds the certificate rsNullFieldReductionCert, which packages three facts: the metric term vanishes on nulls, the RS-coupled source reduces to the null scalar equation, and the undetermined scalar metric term is null-invisible. The module doc frames this as the algebraic half of an RS null-field reduction, not a derived Einstein equation from the ledger.
In the broader Recognition gravity stack this is the place where the RS-native Einstein coupling $\kappa=8\phi^5$ is wired into the Clausius-style null-probe algebra. Honesty tags remain explicit: inhabiting EinsteinShapedSource from the RS action is still OPEN external input; the module does not build horizons, identify cut channels with covectors, or derive a sourced field equation from the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.