Pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.LocalAreaRaychaudhuri

show as:
view Lean formalization →

Defines Raychaudhuri data in which the Ricci-null scalar is the quadratic contraction of a symmetric matrix Ricci field with a Lorentz-null probe. The package keeps the differential Raychaudhuri law and second-area identities, without a stress tensor or Ricci-stress equality. Relativity workers linking local area variation to the Clausius-Einstein algebraic hinge would cite it. Content is mostly structure and definitional bridges from the imported area-variation and Clausius modules.

claimA data package for local Raychaudhuri geometry: a symmetric matrix-valued Ricci field $R_{\mu\nu}$, a Lorentz-null probe $\ell^\mu$ ($g(\ell,\ell)=0$), and the Ricci-null scalar fixed as the quadratic contraction $R_{\mu\nu}\ell^\mu\ell^\nu$. The package records the Raychaudhuri differential law and the second area variation at equilibrium ($A'=\theta A$), but carries neither a stress tensor nor a Ricci-stress identification.

background

Jacobson's thermodynamic route to Einstein gravity equates local Clausius balance $\delta Q = T,dS$ on null horizons with area variation of the horizon cross-section. The imported Clausius-Einstein bridge isolates the finite-dimensional algebra: equality of two symmetric quadratic forms on every Minkowski-null direction fixes their difference only up to a multiple of the metric, so an all-null Clausius balance has the algebraic shape of Einstein's equation with the metric term free.

The companion module on local equilibrium area variation supplies the explicit model $A' = \theta A$ on top of a scalar Raychaudhuri model and derives the second area variation at a single equilibrium point. The present module sits between those layers: it packages matrix Ricci data so that the Ricci-null scalar is definitionally the quadratic contraction against the null probe, ready for area-second-derivative identities without yet committing to $T_{\mu\nu}$ or $R_{\mu\nu}\propto T_{\mu\nu}$.

proof idea

Definition and packaging module rather than a deep proof development. It introduces a structure (matrix Ricci Raychaudhuri data) whose Ricci-null field is the quadratic contraction of the symmetric matrix Ricci against the null probe, with conversion lemmas into the scalar local Raychaudhuri data used upstream. A named identity equates the second area derivative at equilibrium to minus area times that quadratic contraction, wiring the imported $A'=\theta A$ equilibrium variation into the matrix Ricci setting. No stress tensor or Einstein equation is proved here.

why it matters in Recognition Science

In the Recognition relativity stack this is the geometric hinge that makes Ricci enter Raychaudhuri as a null quadratic form, the same algebraic object the Clausius-Einstein bridge later constrains. Downstream consumers (none linked yet in the graph) would use it to pass from equilibrium area variation to a local Einstein-shaped balance without smuggling in matter content early. It keeps the honesty split explicit: Raychaudhuri differential law and area identities only; Ricci-stress equality and the full thermodynamic derivation remain outside. Framework-wise it supports the geometric side of the gravity bridge, not the T0-T8 forcing chain or the phi-ladder mass formula.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)