toLocalRaychaudhuriData_ricciNull
plain-language theorem explainer
When matrix Ricci data is packaged as local Raychaudhuri data, the scalar Ricci-null field at affine parameter λ equals the quadratic contraction of the stored Ricci matrix against the null probe. Relativity and Clausius–Einstein bridge work cites this as the definitional bridge between matrix and scalar forms. The proof is pure reflexivity: the adapter sets ricciNull by that contraction.
Claim. For any matrix Ricci–Raychaudhuri package $D$ and affine parameter $\lambda\in\mathbb{R}$, the Ricci-null scalar of the induced local Raychaudhuri data satisfies $$D.(\mathrm{to\ local}).\mathrm{ricciNull}(\lambda)=A_{\mu\nu}k^{\mu}k^{\nu},$$ where $A=D.\mathrm{ricciTensor}(\lambda)$ is the symmetric $4\times 4$ Ricci matrix and $k=D.\mathrm{nullProbe}(\lambda)$ is the Lorentz-null probe at $\lambda$.
background
The module is a thin definitional adapter. LocalEquilibriumAreaVariation already derives the equilibrium second-area germ from explicit area-rate and Raychaudhuri model laws that consume a scalar field ricciNull. Here one starts instead from a symmetric matrix-valued Ricci field $A(\lambda)$ on $\mathbb{R}^{1,3}$ and a Lorentz-null probe $k(\lambda)$, and packages them so the scalar is the quadratic contraction.
That contraction is quadContr: $A_{\mu\nu}k^{\mu}k^{\nu}=\sum_{i,j}A_{ij}k_i k_j$. The structure MatrixRicciRaychaudhuriData stores expansion and shear-squared rates, the Ricci matrix, the null probe, symmetry of $A$, nullness of $k$, and a MODEL twist-free null Raychaudhuri ODE written with the explicit matrix contraction. It stores no stress tensor and no Ricci–stress equality.
Honesty tags in the module doc are explicit: nothing here equates Ricci with stress, derives the probe from a finite cut, or states an Einstein equation. Spatial dimension $D=3$ appears only as ambient RS context (T8), not as a hypothesis of this lemma.
proof idea
One-line rfl. The conversion toLocalRaychaudhuriData defines the scalar ricciNull field to be exactly quadContr of the stored Ricci matrix against the null probe, so the stated equality is definitional. Marked @[simp] so downstream rewrites unfold the adapter automatically.
why it matters
Closes the matrix-to-scalar seam needed by the local equilibrium area-variation story: second-area identities can be stated with quadContr on matrix Ricci data without a separate matching lemma. The sibling doc notes the matrix form of the equilibrium second-area variation is obtained by definitional transport of ricciNull rather than by storing a separate equality; this simp lemma is that transport.
In the broader RS relativity stack it sits under the Clausius–Einstein bridge vocabulary (quadContr, null probes) while remaining strictly kinematic: MODEL Raychaudhuri with explicit Ricci contraction, not a derivation of Einstein equations. No used_by edges are recorded yet; the natural consumers are second-area and focusing identities that prefer matrix Ricci input. Framework landmarks touched only indirectly: null congruence geometry in $D=3$ spacetime, not the T5–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.