Pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.LocalEquilibriumAreaVariation

show as:
view Lean formalization →

Packages local scalar Raychaudhuri data with cross-sectional area under an explicit area-rate model law, not an integrated area formula. At local equilibrium the second area germ equals minus area times the null Ricci scalar. Downstream matrix-Ricci adapters and decoy inequalities for nonzero expansion or shear cite this package. Arguments differentiate the model area-rate law against the equilibrium Raychaudhuri slope from the upstream reduction module.

claimLocal area-congruence data $(A,\theta,\sigma,R_{kk})$ obey the model law $A'=\theta A$. At equilibrium ($\theta=\sigma=0$) one has $A''(0)=-A(0)\,R_{kk}$, equivalently $(\mathrm{d}^2A/\mathrm{d}\lambda^2)|_0=-A(0)\,R_{kk}$. If expansion or shear is nonzero, the area-rate slope differs from $-A\,R_{kk}$.

background

Upstream, the local Raychaudhuri reduction module records the scalar 4D null-congruence slope and proves its local-equilibrium algebraic reduction under an explicit differential-law model. That slope is the usual combination of expansion, shear, and the null Ricci contraction $R_{kk}=\mathrm{Ric}(k,k)$ along a null generator $k$.

This module adds cross-sectional area $A$ to that scalar package. The area-rate law $A'=\theta A$ is declared as a model premise: it is not derived here by integrating the expansion of a congruence. Local area-congruence data therefore couple $(A,\theta,\sigma,R_{kk})$ with that differential law and the equilibrium reduction already proved upstream.

The theoretical setting is local null-congruence geometry in the Relativity layer: one works with scalar germs along an affine parameter, not with a global focusing theorem or a full Einstein-equation solution.

proof idea

The module is a short calculus layer on top of the upstream equilibrium reduction. First, the model premise $A'=\theta A$ is recorded and differentiated: the first derivative identity is immediate, and a second differentiation produces a formula for $A''$ in terms of $\theta'$, $\theta$, and $A$.

At equilibrium one substitutes the upstream algebraic reduction of the Raychaudhuri slope ($\theta'=\sigma=0$ forces the slope to $-R_{kk}$) to obtain $A''(0)=-A(0),R_{kk}$, also packaged as a HasDerivAt statement and as an iterated second derivative at zero. An auxiliary area-rate slope object isolates that second-order coefficient.

Separate inequalities show the slope cannot equal $-A,R_{kk}$ when expansion or shear is nonzero; named decoy lemmas restate those mismatches for downstream contrast.

why it matters in Recognition Science

Downstream, LocalAreaRaychaudhuri is only a definitional adapter: it maps a matrix-valued Ricci field and Lorentz-null probes onto the scalar $R_{kk}$ consumed here, and its module doc states that the equilibrium second-area germ is already proved in this file from the explicit area-rate and Raychaudhuri model laws.

In the Recognition relativity stack this is the bridge from scalar null-congruence equilibrium to an area-focusing germ usable by geometric adapters. It does not itself invoke the forcing chain (T0–T8), the Recognition Composition Law, or the $\phi$-ladder; those enter only if a later physics layer ties $R_{kk}$ or the area germ to RS constants.

The decoy lemmas matter for honesty tagging: they mark that the clean second-area identity is equilibrium-only, so nonzero expansion or shear cannot silently reuse the same germ.

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)