MatrixRicciRaychaudhuriData
plain-language theorem explainer
Packages expansion, shear-squared, a symmetric 4×4 Ricci matrix field, and a Minkowski-null probe so that the Ricci-null scalar is definitionally the quadratic contraction R_μν k^μ k^ν. Anyone wiring matrix Ricci into the scalar local-area Raychaudhuri pipeline cites this adapter. It is pure structure data plus a MODEL ODE field; no proof content.
Claim. A data package consisting of real functions $\theta(\lambda)$ (expansion), $\sigma^2(\lambda)$ (shear-squared), a field of symmetric $4\times 4$ matrices $R_{\mu\nu}(\lambda)$, and a Lorentz-null probe $k^\mu(\lambda)$ (Minkowski signature $(-,+,+,+)$), such that at every affine parameter $\lambda$ the derivative $\theta'(\lambda)$ equals the twist-free null Raychaudhuri slope built from $\theta(\lambda)$, $\sigma^2(\lambda)$, and the quadratic contraction $R_{\mu\nu}(\lambda)\,k^\mu(\lambda)\,k^\nu(\lambda)$. No stress tensor and no Ricci-stress equality are stored.
background
The classical null Raychaudhuri equation governs the evolution of the expansion $\theta$ of a twist-free null congruence: $\frac{d\theta}{d\lambda}=-\frac12\theta^2-\sigma^2-R_{\mu\nu}k^\mu k^\nu$. In this codebase the scalar package LocalRaychaudhuriData already consumes a single real function ricciNull in place of that contraction, and LocalEquilibriumAreaVariation derives the equilibrium second-area germ from the area-rate law plus that scalar MODEL ODE.
This module only inserts a definitional adapter. MinkowskiNull is the standard nullness condition $-(k^0)^2+(k^1)^2+(k^2)^2+(k^3)^2=0$. quadContr is the quadratic contraction of a $4\times 4$ matrix against a four-vector. The structure stores a matrix-valued Ricci field and a null probe, forces symmetry of the matrix and nullness of the probe, and writes the Raychaudhuri slope with the contraction expanded in place.
Honesty tags from the module: the law field is MODEL (twist-free null Raychaudhuri with explicit matrix contraction). Nothing here equates Ricci with stress, derives the probe from a finite cut, or states an Einstein equation.
proof idea
No proof: this is a structure declaration. The four data fields and two Prop fields (ricci_symmetric, probe_null) are stored as hypotheses on the package. The law field is the MODEL ODE, requiring HasDerivAt of expansion at every $\lambda$ with slope raychaudhuriSlope(θ, σ², quadContr(R,k)).
The companion forgetful map toLocalRaychaudhuriData is a one-line record construction: copy expansion and shear-squared, set ricciNull := fun λ => quadContr (ricciTensor λ) (nullProbe λ), and reuse law unchanged. The simp lemma toLocalRaychaudhuriData_ricciNull is then rfl.
why it matters
This is the matrix Ricci adapter that lets the local-area pipeline speak in components rather than a pre-contracted scalar. Downstream, second_area_deriv_eq_neg_area_mul_quadContr obtains the matrix form of the equilibrium second-area variation by definitional transport of ricciNull (no separate matching equality). The simp fact toLocalRaychaudhuriData_ricciNull pins that transport to rfl.
In the broader Recognition stack this sits under the Clausius–Einstein bridge imports: it prepares matrix Ricci for the local-equilibrium area germ without claiming Einstein dynamics. Framework landmarks nearby are the forced spatial dimension $D=3$ (T8) and the four-dimensional Lorentz index set Fin 4, but this declaration itself does not re-derive $D$ or the eight-tick octave. Open honesty gap, stated in the module: no Ricci-stress equality and no derivation of the null probe from the finite cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.