LocalRaychaudhuriData
plain-language theorem explainer
Packages three scalar fields along an affine parameter—expansion, shear-squared, and Ricci-null contraction—with an explicit MODEL premise that expansion obeys the twist-free null Raychaudhuri ODE. Equilibrium-reduction lemmas and area-congruence extensions cite it as the carrier of that law. Definitional only: the ODE is assumed, not derived from a metric or null congruence.
Claim. A local Raychaudhuri data package consists of three real functions of an affine parameter $\lambda$: the expansion $\theta(\lambda)$, the shear-squared $\sigma^2(\lambda)$, and the Ricci-null contraction $R_{ab}k^a k^b(\lambda)$, together with the model law that for every $\lambda$ one has $\frac{d\theta}{d\lambda}\big|_{\lambda} = -\tfrac12\theta(\lambda)^2 - \sigma^2(\lambda) - R_{ab}k^a k^b(\lambda)$.
background
The module records the scalar 4D null-congruence slope and proves its local-equilibrium algebraic reduction under an explicit differential-law MODEL. Honesty tags state that the law field is a MODEL interface (the twist-free null-horizon Raychaudhuri ODE for scalar expansion), that zero initial expansion and shear are equilibrium hypotheses rather than derived geometry, and that the module introduces neither metric, null vector, Ricci tensor, area element, ledger, stress, Unruh, EFE, nor C-gap1.
The right-hand side is the pure scalar map raychaudhuriSlope: for real arguments $\theta$, $\sigma^2$, and $R_{ab}k^a k^b$,
$$\mathrm{slope}(\theta,\sigma^2,R) = -\tfrac12\theta^2 - \sigma^2 - R.$$
No spacetime geometry is imported; the three arguments are treated as real scalars. Downstream, the same package is extended by an area field with its own MODEL area-rate law $dA/d\lambda = \theta A$, and by a matrix Ricci field contracted against a Lorentz-null probe.
proof idea
No proof body: this is a structure definition. Four fields are declared—three real-valued functions of the affine parameter, plus a Prop field asserting that at every real $\lambda$ the expansion admits a derivative equal to raychaudhuriSlope evaluated on the three fields at $\lambda$. Instantiating the structure means supplying those functions and a proof of the ODE premise; the structure itself performs no reduction.
why it matters
This is the carrier type for every local Raychaudhuri argument in the module. The general initial-slope lemma specializes the MODEL law at $\lambda=0$; under the equilibrium hypotheses $\theta(0)=0$ and $\sigma^2(0)=0$ one obtains $\mathrm{HasDerivAt},\theta,(-R(0)),0$ and the pointwise form $\theta'(0)=-R(0)$. Arithmetic decoys in the same module show each equilibrium premise is load-bearing.
Downstream, LocalAreaCongruenceData extends this structure by a cross-sectional area and an area-rate MODEL, and MatrixRicciRaychaudhuriData replaces the bare Ricci-null scalar by a quadratic contraction of a symmetric matrix Ricci field against a null probe—still without stress tensor or Ricci-stress equality. In the broader RS relativity stack the package isolates the classical null Raychaudhuri slope so later ledger or C-gap claims can cite a clean conditional reduction rather than smuggling geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.