source_of_componentwise
plain-language theorem explainer
Entrywise Einstein-shaped source equations lift to the matrix-level interface. Anyone holding κ T_ij = Ric_ij + f η_ij for all indices can cite this to obtain EinsteinShapedSource. The proof packages the given scalar f as the existential witness and finishes by matrix extensionality.
Claim. Let $\kappa, f \in \mathbb{R}$ and let $T, \mathrm{Ric}$ be $4\times 4$ real matrices. If $\kappa\, T_{ij} = \mathrm{Ric}_{ij} + f\, \eta_{ij}$ for every pair of indices $i,j$, where $\eta = \mathrm{diag}(-1,1,1,1)$ is the Minkowski metric, then the Einstein-shaped source interface holds: there exists a real scalar (namely this $f$) such that $\kappa\, T = \mathrm{Ric} + f\, \eta$ as matrices.
background
The module treats the algebraic step from an assumed Einstein-shaped matrix source to its null-contracted scalar equation. Honesty tags mark all matrix and null-contraction algebra as THEOREM, while inhabiting the source interface from the RS action remains OPEN external input.
EinsteinShapedSource κ T Ric is the Prop interface $\exists f,; \kappa\bullet T = \mathrm{Ric} + f\bullet\eta$, explicitly not derived in-tree from the RS action. Here $\eta$ is minkowskiEta4, the standard $(-,+,+,+)$ Minkowski metric in the coordinate basis. Scalar multiplication on matrices is entrywise.
Downstream in the same file, null reduction of one such equation shows the undetermined metric term vanishes on every Minkowski-null direction, yielding $\mathrm{Ric}(k,k) = \kappa, T(k,k)$. The present lemma only bridges the entrywise presentation into that matrix interface.
proof idea
Term/tactic hybrid, three steps. Supply the given scalar $f$ as the existential witness for EinsteinShapedSource via refine ⟨f, ?_⟩. Discharge the remaining matrix equality by ext i j, reducing to entrywise comparison. Rewrite scalar multiplications with Matrix.smul_apply and smul_eq_mul, then apply the componentwise hypothesis h i j. No external lemmas beyond matrix API.
why it matters
Closes the presentation gap between componentwise source equations (natural when reading off curvature and stress-energy entries) and the matrix Prop that the rest of the null-reduction pipeline consumes. The module goal is: from $\kappa T = \mathrm{Ric} + f\eta$ and Minkowski-null $k$, conclude $\mathrm{Ric}(k,k) = \kappa T(k,k)$, with RS specialization $\kappa = \kappa_{\mathrm{einstein}}$.
No used_by edges are recorded yet; siblings such as null_scalar_of_einstein_shaped and rs_null_scalar_of_source are the intended consumers. The declaration does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure linear-algebra scaffolding inside the gravity bridge. It leaves open the external input flagged in the module doc: deriving an inhabited EinsteinShapedSource from the RS action or ledger, rather than assuming it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.