decoy_nonzero_expansion_areaRate_ne
plain-language theorem explainer
Concrete numerical decoy: with expansion θ=2, vanishing shear, unit null Ricci, and unit area, the differentiated area-rate product is not −A·R. Cited to show that the zero-expansion equilibrium hypothesis is load-bearing for the second area-variation identity. Proof is a one-line norm_num after unfolding the two scalar slope definitions.
Claim. For expansion $\theta=2$, shear-squared $\sigma^2=0$, null Ricci contraction $R_{ab}k^a k^b=1$, and cross-sectional area $A=1$, the arithmetic area-rate slope is unequal to $-1$.
background
The module adjoins the explicit area-rate model $A'=\theta A$ to the scalar twist-free null Raychaudhuri model and computes the second area variation at a single equilibrium point. Both differential laws are MODEL interfaces: no stress tensor, EFE, Unruh relation, or ledger-to-geometry bridge is claimed.
The scalar Raychaudhuri right-hand side is raychaudhuriSlope: $d\theta/d\lambda=-\tfrac12\theta^2-\sigma^2-R_{ab}k^a k^b$, treated as a pure real expression. Differentiating the product $A'=\theta A$ and substituting that slope yields areaRateSlope $(\theta,\sigma^2,R,A)=\mathrm{raychaudhuriSlope}(\theta,\sigma^2,R)\cdot A+\theta(\theta A)$.
At true equilibrium ($\theta=\sigma=0$) this collapses to $-A,R$. The decoys check that the collapse fails when the equilibrium hypotheses are dropped.
proof idea
Unfold areaRateSlope and raychaudhuriSlope at the concrete point $(\theta,\sigma^2,R,A)=(2,0,1,1)$, then discharge the resulting rational inequality by norm_num. Explicitly: raychaudhuri slope equals $-\tfrac12\cdot 4-0-1=-3$, so area-rate slope equals $(-3)\cdot 1+2\cdot(2\cdot 1)=1$, and $1\neq -1$.
why it matters
Module honesty tags state that zero initial expansion and shear are equilibrium hypotheses and that arithmetic decoys show they are load-bearing for the second-variation identity. This declaration is the concrete expansion witness: nonzero $\theta$ alone already breaks equality of the area-rate slope with $-A R$, even with vanishing shear and unit normalizations.
It sits beside the general comparison lemma areaRateSlope_ne_neg_area_mul_ricciNull_of_nonzero_expansion and the parallel shear decoy. No downstream consumer is wired yet; the result is local scaffolding for the calculus-only claim that the equilibrium second area variation equals $-A R$ only when $\theta=\sigma=0$. No T0–T8 forcing step, RCL identity, or mass-ladder claim is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.