Pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.LocalRaychaudhuriReduction

show as:
view Lean formalization →

Scalar packaging of the 4D null Raychaudhuri law: the expansion slope equals minus half theta-squared minus shear-squared minus the Ricci null contraction, with all three inputs treated as real numbers. Relativity workers cite it when they need the local focusing ODE without a full spacetime manifold. The module supplies the slope definition, derivative identities at equilibrium, and decoy inequalities that separate the zero-expansion, zero-shear case from nonzero contaminants.

claimDefine the scalar null Raychaudhuri slope by $\mathrm{slope}(\theta,\sigma^2,R_{kk})=-\tfrac12\theta^2-\sigma^2-R_{kk}$. At vanishing expansion and shear one has $d\theta/d\lambda=-R_{ab}k^ak^b$. Nonzero $\theta$ or $\sigma^2$ forces the slope away from $-R_{kk}$.

background

Classical null Raychaudhuri governs the rate of change of the expansion $\theta$ of a null congruence along its affine parameter $\lambda$:

$$d\theta/d\lambda=-\tfrac12\theta^2-\sigma^2-R_{ab}k^ak^b.$$

Here $\sigma^2$ is the shear-squared scalar and $R_{ab}k^ak^b$ is the Ricci tensor contracted on the null generator. The present module strips that identity down to three real scalars and a pure real-valued right-hand side; no Lorentzian metric, connection, or curvature tensor is imported.

Sibling objects introduce the slope function, a data bundle holding the three scalars, derivative statements at the equilibrium point $(\theta,\sigma^2)=(0,0)$, and decoy lemmas showing that a nonzero expansion or shear term cannot reproduce the pure $-R_{kk}$ slope. Downstream work builds an area-rate model $A'=\theta A$ on top of this scalar skeleton.

proof idea

Definitional core plus elementary real analysis. The slope is introduced as an ordinary real function of three variables. Derivative claims at vanishing expansion are discharged by direct differentiation and ring or norm-num simplification. Decoy inequalities compare the full slope against $-R_{kk}$ and use the nonnegativity of $\theta^2$ and $\sigma^2$ (via linarith-style arithmetic) to obtain strict inequality whenever either contaminant is nonzero. No geometric lemmas appear; the argument never leaves $\mathbb{R}$.

why it matters in Recognition Science

Feeds the local-equilibrium area-variation layer (LocalEquilibriumAreaVariation), which adds the model $A'=\theta A$ and derives the second area variation at one equilibrium point. That step is the bridge from the pure focusing ODE to concrete statements about area decrease under positive Ricci null contraction. Inside the Recognition relativity stack the module therefore supplies the minimal analytic engine for null focusing without committing to a full spacetime formalization, keeping the geometric hypotheses explicit and local.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (9)