null_scalar_of_source
plain-language theorem explainer
Given an Einstein-shaped matrix source κT = Ric + f η, every Minkowski-null contraction kills the undetermined metric term and yields Ric(k,k) = κ T(k,k). Gravity workers cite it when reducing a matrix-level Einstein equation to a null scalar identity without fixing f. The proof unpacks the existential witness and applies the already-proved null reduction for a fixed scalar multiple.
Claim. Fix a real coupling $\kappa$ and $4\times 4$ real matrices $T$ and $\mathrm{Ric}$. Suppose there exists $f\in\mathbb{R}$ such that $\kappa\, T = \mathrm{Ric} + f\,\eta$, where $\eta$ is the Minkowski metric matrix. Then for every four-vector $k$ with $\eta(k,k)=0$, the quadratic contractions satisfy $\mathrm{Ric}(k,k) = \kappa\, T(k,k)$.
background
The module treats the purely algebraic step from an assumed Einstein-shaped matrix equation to its null-contracted scalar form. It does not derive the source from the RS action; the source is an external interface.
EinsteinShapedSource κ T Ric means there exists a real scalar $f$ with $κ • T = Ric + f • η_4$, where $η_4$ is the standard Minkowski metric matrix of signature $(-,+,+,+)$. The quadratic contraction quadContr A k is $A_{μν} k^μ k^ν$. A vector $k$ is MinkowskiNull when $-(k^0)^2+(k^1)^2+(k^2)^2+(k^3)^2=0$.
Upstream, the sibling lemma null_scalar_of_einstein_shaped already shows that once $f$ is fixed, the metric term vanishes on every null direction, leaving $Ric(k,k)=κ T(k,k)$. The present theorem only packages that fact under the existential interface.
proof idea
Term-mode unpacking of the interface. From h : EinsteinShapedSource coupling T Ric obtain a witness scalar $f$ and the matrix identity $coupling • T = Ric + f • η$. Introduce an arbitrary null vector $k$. Finish by applying null_scalar_of_einstein_shaped to that fixed $f$, the identity, and the nullness hypothesis. No further algebra is performed here.
why it matters
This is the bundled form of the null reduction used throughout the RS gravity bridge. Downstream, rs_null_scalar_of_source specializes the free coupling to the RS Einstein coupling kappa_einstein, giving the RS-normalized null scalar identity in one line.
In the Clausius–Einstein story, null contractions are the natural probes: the undetermined pure-trace metric term is invisible on lightlike directions, so the sourced curvature reduces to a scalar relation between $Ric$ and $T$. The module honesty tags stress that inhabiting EinsteinShapedSource from the RS action remains open; this theorem only closes the algebraic half of that bridge.
It sits in the Gravity domain as conditional matrix algebra, not as a derived field equation from the ledger or eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.