EinsteinShapedSource
plain-language theorem explainer
Defines the matrix-level interface for an Einstein-shaped sourced equation: a coupling times a stress-energy matrix equals a Ricci matrix plus an undetermined multiple of Minkowski η. Gravity and RS-null-reduction proofs cite it as the external input hypothesis. The body is a pure existential Prop, not a derived theorem.
Claim. Given a real coupling $\kappa$ and $4\times 4$ real matrices $T$ and $\mathrm{Ric}$, the pair is Einstein-shaped when there exists $f\in\mathbb{R}$ such that $\kappa\, T = \mathrm{Ric} + f\,\eta$, where $\eta=\mathrm{diag}(-1,1,1,1)$ is the Minkowski metric in the standard basis.
background
The module treats the algebraic step from an independently supplied Einstein-shaped matrix equation to its null-contracted scalar form. Honesty tags mark the matrix and null-contraction algebra as proved, while inhabiting the source interface from the RS action remains an external input.
The Minkowski metric $\eta$ is the standard $(-!+,+,+)$ matrix on $\mathbb{R}^4$. Quadratic contraction $A(k,k)=A_{\mu\nu}k^\mu k^\nu$ is the bilinear form used downstream. The definition packages the classical Einstein shape $\kappa T=\mathrm{Ric}+f\eta$ as a Prop on two matrices and a coupling, without deriving it from a ledger or horizon patch.
Upstream, only the metric matrix is needed here; the two unrelated T symbols in the dependency graph (exp/log field and Freudenthal strip) are name collisions, not inputs to this interface.
proof idea
Definitional: the body is the existential proposition $\exists f:\mathbb{R},;\kappa\bullet T=\mathrm{Ric}+f\bullet\eta$. No tactics or lemmas. Downstream theorems unpack the witness $f$ and cancel the metric term on null vectors.
why it matters
This is the explicit input interface for the module's null reduction chain. null_scalar_of_source bundles the reduction: under the interface and Minkowski-null $k$, $\mathrm{Ric}(k,k)=\kappa,T(k,k)$. The RS specialization rs_null_scalar_of_source fixes $\kappa=\kappa_{\mathrm{einstein}}$. source_of_componentwise lifts entrywise equations into the interface; RSNullFieldReductionCert certifies metric-term vanishing and source reduction.
Module docs stress that inhabiting the interface from the RS action is open: the file does not construct horizons, identify cut channels with covectors, or derive a sourced field equation from the ledger. It is the conditional hinge between classical Einstein shape and the RS null scalar equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.