hasDerivAt_expansion_zero
plain-language theorem explainer
At affine parameter zero, the scalar expansion of a null congruence is differentiable with derivative equal to the twist-free Raychaudhuri slope on the initial expansion, shear-squared, and null Ricci. Anyone specializing the local MODEL ODE before imposing equilibrium cites this. The proof is a one-line instantiation of the packaged differential law at λ = 0.
Claim. Let $D$ be local scalar Raychaudhuri data: maps $\theta,\sigma^2,R_{kk}:\mathbb{R}\to\mathbb{R}$ together with the MODEL premise that $\theta$ obeys the twist-free null-horizon Raychaudhuri ODE at every affine parameter. Then $\theta$ has derivative at $0$ equal to the Raychaudhuri slope evaluated on $(\theta(0),\sigma^2(0),R_{kk}(0))$.
background
The module records a scalar 4D null-congruence slope and its algebraic reduction under an explicit differential-law MODEL. Honesty tags are strict: the law is a MODEL interface (the twist-free null-horizon Raychaudhuri ODE for the scalar expansion); zero initial expansion and shear are equilibrium hypotheses, not derived geometry; no metric, null vector, Ricci tensor, area element, ledger, stress, Unruh, EFE, or C-gap1 claim is introduced.
LocalRaychaudhuriData packages three real functions of an affine parameter—expansion $\theta$, shear-squared $\sigma^2$, and a null Ricci scalar $R_{kk}$—plus a field law asserting that for every $\lambda$, $\theta$ has derivative equal to the Raychaudhuri slope built from those three values at $\lambda$. The slope itself is the standard twist-free right-hand side (quadratic in $\theta$, linear in $\sigma^2$ and $R_{kk}$).
This declaration is the unrestricted specialization of that MODEL law at the initial point $\lambda=0$, before any equilibrium hypothesis is imposed.
proof idea
One-line term proof: apply the universal MODEL field law of the data package at the concrete affine parameter $0$. No algebraic rewriting, no calculus lemmas, and no equilibrium hypotheses are used. The resulting HasDerivAt statement is exactly the law's conclusion with $\lambda$ fixed to zero.
why it matters
Immediate parent is hasDerivAt_expansion_eq_neg_ricciNull, which under the local-equilibrium hypotheses $\theta(0)=0$ and $\sigma^2(0)=0$ rewrites the initial slope as $-R_{kk}(0)$. That reduction is the module's main algebraic claim: conditional on the MODEL law, equilibrium initial data force the initial expansion derivative to equal minus the null Ricci scalar.
The present lemma isolates the unrestricted initial-slope step so the equilibrium reduction is a pure arithmetic specialization of the slope formula, not a re-derivation of differentiability. Sibling decoy theorems then show each equilibrium premise is load-bearing: nonzero initial expansion or shear makes the slope differ from $-R_{kk}(0)$.
In the broader Recognition stack this sits in the relativity geometry layer as a conditional MODEL interface, not a forcing-chain (T0–T8) result. It does not touch $\phi$, the eight-tick octave, or the $\alpha$ band; it only prepares a clean local null-congruence slope for later gravity or horizon arguments that choose to adopt the MODEL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.