Pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.LocalEquilibriumAreaVariation

show as:
view Lean formalization →

Packages local scalar Raychaudhuri data with a cross-sectional area function and an explicit area-rate MODEL law. At local equilibrium (vanishing expansion and shear) it identifies the second area germ with minus area times the null Ricci scalar. Relativists tracing the RS local focusing argument cite it. Proofs are calculus identities from the MODEL ODEs plus the upstream equilibrium slope reduction.

claimGiven local null-congruence data $(A,\theta,\sigma,R_{kk})$ with MODEL laws $\dot A=\theta A$ and the scalar Raychaudhuri slope for $\dot\theta$, at an equilibrium point where $\theta=\sigma=0$ one has $\frac{d^2A}{d\lambda^2}\big|_0=-A\,R_{kk}$. Off equilibrium, the area-rate slope differs from $-A R_{kk}$ whenever $\theta\neq 0$ or $\sigma\neq 0$.

background

The parent setting is the local Raychaudhuri equilibrium reduction: a scalar 4D null-congruence slope together with an algebraic reduction of that slope under an explicit differential-law MODEL. This module adjoins a cross-sectional area $A(\lambda)$ along the same affine parameter.

The area-rate law $\dot A=\theta A$ is declared as a MODEL premise, not derived from an integrated area formula or from a full congruence embedding. The null Ricci scalar $R_{kk}$ and the expansion/shear scalars are inherited from the upstream local data bundle.

Local equilibrium means vanishing expansion and shear at the evaluation point. Under that hypothesis the second $\lambda$-derivative of $A$ is forced by the two MODEL ODEs alone.

proof idea

Define a data bundle pairing area with the upstream scalar Raychaudhuri fields. Record $\dot A=\theta A$ as a HasDerivAt fact. At equilibrium, $\theta=0$ collapses the first area derivative to zero; substituting the upstream equilibrium slope for $\dot\theta$ into the product rule yields $\ddot A=-A,R_{kk}$ (also as an iterated second derivative).

Separate lemmas compute the off-equilibrium area-rate slope and show it differs from $-A R_{kk}$ when expansion or shear is nonzero (decoy inequalities). Imports supply product-rule and iterated-derivative infrastructure from Mathlib.

why it matters in Recognition Science

Feeds LocalAreaRaychaudhuri, whose doc-comment states that this module "already proves the equilibrium second-area germ from the explicit area-rate and Raychaudhuri MODEL laws"; the downstream file only adapters matrix Ricci and Lorentz-null probes into the scalar $R_{kk}$ consumed here.

In the RS relativity stack this is the local focusing seed: equilibrium area variation is locked to null Ricci, so geodesic deviation and the focusing criterion sit on explicit MODEL ODEs rather than on a global curvature integral. It does not itself invoke the T0–T8 forcing chain; it is geometry infrastructure those later bridges can quote.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)