areaRateSlope
plain-language theorem explainer
Defines the scalar second-area rate from differentiating the product law A' = θ A under the null Raychaudhuri slope. Local-equilibrium area-variation lemmas cite it as the left-hand side that equals −A R_kk only at equilibrium. The body is one-line arithmetic: Raychaudhuri slope times area, plus θ·(θ A).
Claim. For real scalars $\theta$, $\sigma^2$, $R_{ab}k^a k^b$, and $A$, set the area-rate slope equal to $\bigl(-\tfrac12\theta^2-\sigma^2-R_{ab}k^a k^b\bigr)A+\theta\cdot(\theta A)$.
background
The module studies second area variation at one affine parameter value along a twist-free null congruence. Two explicit MODEL premises are fixed: the scalar Raychaudhuri law for expansion $\theta$, and the unit area-rate law $A'=\theta A$. No integrated area evolution, stress tensor, Unruh relation, EFE, or ledger-to-geometry bridge is introduced.
Upstream, the scalar Raychaudhuri slope is the real right-hand side $d\theta/d\lambda=-\tfrac12\theta^2-\sigma^2-R_{ab}k^a k^b$, with no spacetime geometry imported. Differentiating the product $A'=\theta A$ gives $A''=\theta'A+\theta A'=\theta'A+\theta^2 A$. Substituting the Raychaudhuri slope for $\theta'$ is exactly this definition.
Equilibrium hypotheses (vanishing initial expansion and shear) are reserved for later theorems; the definition itself is pure arithmetic on four real scalars.
proof idea
Definitional, not a proof. Apply the product rule to $d(\theta A)/d\lambda$, replace $\theta'$ by the upstream Raychaudhuri slope $-\tfrac12\theta^2-\sigma^2-R$, and replace $A'$ by $\theta A$. The body is the closed form
raychaudhuriSlope θ σ² R * A + θ * (θ * A).
No tactics or lemmas beyond that upstream slope abbreviation.
why it matters
This is the calculus hinge between the local Raychaudhuri germ and equilibrium second-area variation. Four sibling results consume it: two obstruction theorems show that nonzero initial expansion (even with $\sigma^2=0$) or nonzero shear-squared (even with $\theta=0$), together with $A\neq 0$, force the slope away from $-A R$; two numerical decoys ($\theta=2$ and $\sigma^2=1$) discharge the same inequalities by norm_num.
In the Recognition relativity stack it keeps the reduced formula $A''=-A R_{kk}$ strictly conditional on zero expansion, zero shear, and the unit normalization $A'=\theta A$. It does not touch the T0–T8 forcing chain, eight-tick octave, or mass ladder; those live elsewhere. Its role is honesty bookkeeping: load-bearing hypotheses are named before any equilibrium claim is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.