raychaudhuriSlope
plain-language theorem explainer
Packages the scalar right-hand side of the 4D null Raychaudhuri law as a pure real function of expansion, shear-squared, and Ricci-null contraction. Anyone working the local-equilibrium or area-variation reductions cites it as the expansion slope. The body is a one-line arithmetic definition with no geometric hypotheses.
Claim. For real scalars $\theta$ (expansion), $\sigma^2$ (shear-squared), and $R_{ab}k^a k^b$ (Ricci null contraction), the Raychaudhuri slope is $-\tfrac12\theta^2 - \sigma^2 - R_{ab}k^a k^b$.
background
The classical null Raychaudhuri equation governs the evolution of the expansion scalar $\theta$ of a twist-free null congruence along an affine parameter $\lambda$:
$$\frac{d\theta}{d\lambda} = -\tfrac12\theta^2 - \sigma^2 - R_{ab}k^a k^b.$$
This module isolates that right-hand side as a pure real arithmetic expression. The three arguments are treated as independent reals; no metric, null vector, Ricci tensor, or area element is imported. The differential law itself is an explicit MODEL premise (recorded later on LocalRaychaudhuriData), not a derived geometric fact. Zero initial expansion and shear are equilibrium hypotheses used downstream, not theorems of this definition.
proof idea
Definitional. The body is the single arithmetic term $-\tfrac12,\theta^2 - \sigma^2 - R_{\mathrm{null}}$, with no tactics, lemmas, or side conditions.
why it matters
This is the shared scalar slope that every local Raychaudhuri reduction in the geometry layer plugs into. Downstream, areaRateSlope multiplies it by area and adds the product rule term under the unit normalization $A'=\theta A$, yielding the second-area rate. The equilibrium lemmas then show that under $\theta(0)=0$ and $\sigma^2(0)=0$ the initial expansion derivative collapses to $-R_{\mathrm{null}}(0)$, while the decoy theorems (decoy_nonzero_expansion_*, decoy_nonzero_shear_*, coefficient-two decoy) prove each equilibrium premise is load-bearing. MatrixRicciRaychaudhuriData stores the same law with Ricci-null realized as a quadratic matrix contraction. The module deliberately stops short of EFE, stress, Unruh, or C-gap claims; it only supplies the arithmetic core those later steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.