deriv_area_eq_expansion_mul_area
plain-language theorem explainer
The explicit area-rate model A'=θA is restated as equality of derivative functions: deriv(area)=expansion·area pointwise. Anyone deriving the second variation of cross-sectional area under a local null Raychaudhuri germ cites this. The proof is a one-line application of deriv_eq to the HasDerivAt area-law premise.
Claim. Let $D$ be local area-congruence data (scalar Raychaudhuri fields plus a cross-sectional area $A$). Then as functions of the affine parameter $\lambda$, $\frac{dA}{d\lambda}=\theta\,A$, i.e. $\mathrm{deriv}(A)=\lambda\mapsto\theta(\lambda)\,A(\lambda)$.
background
The module works in a local null-congruence setting with two explicit MODEL laws: a twist-free scalar Raychaudhuri germ for the expansion $\theta$, and an area-rate law $A'=\theta A$. No integrated area formula, stress tensor, Unruh relation, or Einstein equation is assumed.
LocalAreaCongruenceData extends the local Raychaudhuri data by a real function area and the premise areaLaw: at every $\lambda$, $A$ has derivative $\theta(\lambda)A(\lambda)$. That premise is a pointwise HasDerivAt statement, not yet a global equality of functions.
Mathlib's deriv_eq converts a universal HasDerivAt hypothesis into equality of the deriv function with the given rate. The present theorem is exactly that conversion for the area-rate MODEL.
proof idea
One-line term proof: apply Mathlib deriv_eq to the structure field D.areaLaw. The field already asserts HasDerivAt area (expansion λ · area λ) λ for every λ, so deriv_eq yields the function equality deriv area = fun λ => expansion λ * area λ.
why it matters
This is the bridge from the MODEL interface (HasDerivAt area law) to ordinary calculus on deriv area. The sole downstream consumer is hasDerivAt_deriv_area_eq_neg_area_mul_ricciNull, which rewrites deriv area via this equality and then differentiates the product under equilibrium hypotheses (vanishing initial expansion and shear) to obtain the second area variation $(A')'(0)=-A(0),R_{kk}(0)$.
In the Recognition relativity stack this is pure local calculus on MODEL germs: it does not touch the T0–T8 forcing chain, the ledger-to-geometry bridge, or C-gap claims. It does make the load-bearing role of the unit-normalized law $A'=\theta A$ explicit for the equilibrium second-variation theorems and the arithmetic decoys that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.