Pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.LocalRaychaudhuriReduction

show as:
view Lean formalization →

Scalar reduction of the 4D null Raychaudhuri identity: the expansion slope equals −½θ² − σ² − R_ab k^a k^b, with θ, shear-squared, and the Ricci null contraction treated as ordinary reals. Relativity and focusing arguments that stay off the full spacetime bundle cite this layer. The module packages the slope definition, derivative-at-a-point lemmas, and decoy inequalities that force nonzero expansion or shear away from pure Ricci focusing.

claimDefine the scalar Raychaudhuri slope $S(\theta,\sigma^2,R_{kk}) = -\tfrac12\theta^2 - \sigma^2 - R_{kk}$. At an equilibrium point with $\theta=0$ and $\sigma^2=0$, one has $d\theta/d\lambda = -R_{kk}$. If either $\theta\neq 0$ or $\sigma^2\neq 0$, then $S(\theta,\sigma^2,R_{kk})\neq -R_{kk}$.

background

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

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

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

The central object is the slope function of those three scalars, together with a small data bundle that packages an expansion function and the Ricci null value at a point. Derivative lemmas then relate the actual derivative of expansion at equilibrium to the pure Ricci term, while decoy lemmas record that a nonzero expansion or shear term shifts the slope away from $-R_{kk}$.

proof idea

Definition-first module. The slope is introduced as an ordinary real function of three arguments. A data structure holds the local expansion and Ricci null value. HasDerivAt and deriv lemmas specialize the slope at vanishing expansion (and vanishing shear) to $-R_{kk}$ by direct substitution and calculus facts from Mathlib. Separate decoy lemmas and inequality corollaries show that a nonzero $\theta$ or $\sigma^2$ forces the slope strictly off $-R_{kk}$, proved by elementary algebra (ring, norm_num, linarith).

why it matters in Recognition Science

Feeds the downstream module LocalEquilibriumAreaVariation, which "adds the explicit area-rate MODEL $A'=\theta A$ to the scalar Raychaudhuri MODEL and derives the second area variation at one equilibrium point." That second-variation step is the local geometric input for equilibrium and focusing arguments in the RS relativity layer. By isolating the scalar RHS and the equilibrium reduction $d\theta/d\lambda=-R_{kk}$, this module keeps the area-variation work free of full spacetime geometry while still matching the classical null Raychaudhuri law.

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)