decoy_nonzero_shear_areaRate_ne
plain-language theorem explainer
At the concrete point θ=0, σ²=1, R=1, A=1, the arithmetic area-rate slope is not equal to −A R. Anyone checking load-bearing hypotheses in the local equilibrium area-variation model would cite this decoy. The proof is a one-step norm_num unfold of the two scalar slope definitions.
Claim. With expansion $\theta=0$, shear-squared $\sigma^2=1$, null Ricci contraction $R=1$, and area $A=1$, the arithmetic area-rate slope (Raychaudhuri slope times $A$, plus $\theta^2 A$) is not equal to $-1$.
background
The module sits the explicit area-rate model $A'=\theta A$ on top of the scalar twist-free null Raychaudhuri model and studies the second area variation at one equilibrium point. Both laws are MODEL interfaces: no stress tensor, EFE, Unruh relation, or ledger-to-geometry bridge is claimed.
The scalar Raychaudhuri slope is
$d\theta/d\lambda=-\tfrac12\theta^2-\sigma^2-R_{ab}k^ak^b$,
written as the real function raychaudhuriSlope. Differentiating the product $A'=\theta A$ under unit normalization yields the arithmetic area-rate slope
areaRateSlope$(\theta,\sigma^2,R,A)=$(Raychaudhuri slope)$\cdot A+\theta^2 A$.
Sibling lemmas already show that if shear is nonzero (or expansion is nonzero), this slope fails to equal $-A R$. The present declaration is the concrete numerical witness for nonzero shear.
proof idea
One-line norm_num after unfolding areaRateSlope and raychaudhuriSlope. Substituting $\theta=0$, $\sigma^2=1$, $R=1$, $A=1$ gives Raychaudhuri slope $-2$ and area-rate slope $-2$, which is definitionally unequal to $-1$. No calculus lemmas are needed; the inequality is pure arithmetic on the two closed-form scalars.
why it matters
Module honesty tags state that arithmetic decoys show zero expansion, zero shear, and the unit factor in $A'=\theta A$ are load-bearing. This decoy pins the shear side: with $\theta=0$ but $\sigma^2=1$, the second area variation is not simply $-A R$. Together with the companion expansion decoy it certifies that the equilibrium hypotheses used for the local second-variation identity cannot be dropped.
No downstream theorem currently depends on it (used_by is empty). Its role is local certification inside the Relativity geometry stack, not a step in the T0–T8 forcing chain or the mass ladder. It keeps the Raychaudhuri-plus-area-law calculus honest before any horizon or ledger claim is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.