hasDerivAt_areaRate_zero
plain-language theorem explainer
Before equilibrium is imposed, the derivative at λ=0 of the area rate θA equals the product-rule mix of the Raychaudhuri slope times area plus expansion times the instantaneous area rate. Anyone assembling the second area variation from the two MODEL laws cites this step. The proof is a one-line product rule on the two HasDerivAt premises at zero.
Claim. Let $D$ be local area-congruence data: scalar Raychaudhuri fields plus a cross-sectional area $A$ obeying the MODEL law $A'=\theta A$. Then $\lambda\mapsto \theta(\lambda)A(\lambda)$ is differentiable at $\lambda=0$, with derivative equal to $\mathrm{raychaudhuriSlope}(\theta(0),\sigma^2(0),R_{kk}(0))\,A(0)+\theta(0)\,(\theta(0)A(0))$.
background
This module sits in the local null-congruence calculus layer. It extends the scalar Raychaudhuri MODEL (twist-free null-horizon germ) by an explicit area-rate MODEL $A'=\theta A$, then studies the second variation of area at a single equilibrium point. No integrated area formula, stress tensor, Unruh relation, EFE, or ledger bridge is assumed.
LocalAreaCongruenceData packages the inherited Raychaudhuri fields (expansion $\theta$, shear-squared, null Ricci) together with a real area function and the pointwise premise that $A$ has derivative $\theta(\lambda)A(\lambda)$ at every affine parameter. The companion law for $\theta'$ is the usual Raychaudhuri slope evaluated along the congruence.
The present statement is the pre-equilibrium product rule: differentiate $\theta A$ at $\lambda=0$ using only those two MODEL derivatives. Later siblings impose $\theta(0)=\sigma(0)=0$ and recover $A''(0)=-A(0)R_{kk}(0)$.
proof idea
One-line term proof. Apply the Mathlib product rule for HasDerivAt to the pair (D.law 0) and (D.areaLaw 0). The first supplies $\theta'(0)$ as the Raychaudhuri slope at the initial data; the second supplies $A'(0)=\theta(0)A(0)$. Their product expands exactly to the displayed target derivative. No rewriting or equilibrium hypotheses are used.
why it matters
This is the calculus hinge between the two MODEL laws and the equilibrium second-area-variation identities in the same module (hasDerivAt_areaRate_eq_neg_area_mul_ricciNull, deriv_deriv_area_zero_eq_neg_area_mul_ricciNull, and the iterated-derivative form). The module doc frames the whole development as a pure calculus theorem conditional on those two geometric MODEL interfaces; arithmetic decoys later show that zero expansion, zero shear, and the unit factor in $A'=\theta A$ are load-bearing.
In the broader Recognition relativity stack this keeps the local focusing/area-response step honest: second variation of horizon cross-section area is derived before any ledger-to-geometry or C-gap claim is introduced. No downstream consumers are wired yet (used_by is empty), so the lemma currently serves the in-module equilibrium chain rather than a sealed paper proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.