decoy_areaLaw_coefficient_two_changes_equilibrium
plain-language theorem explainer
At equilibrium (vanishing expansion and shear) with unit Ricci-null contraction and unit area, the scaled area law with coefficient 2 yields second-area rate -2, not the unit-law value -1. Anyone checking that unit normalization A'=θA is load-bearing for local equilibrium area variation would cite this arithmetic decoy. The proof is a one-line numerical evaluation of the scaled slope against the Raychaudhuri slope.
Claim. At the equilibrium witness $\theta=0$, $\sigma^2=0$, Ricci-null contraction $R=1$, and area $A=1$, the second area-rate from the scaled law $A'=c\,\theta A$ with coefficient $c=2$ is not equal to $-1$.
background
The module adjoins the explicit area-rate MODEL $A'=\theta A$ to the scalar Raychaudhuri MODEL and studies the second area variation at one equilibrium point. Honesty tags mark both laws as MODEL interfaces: the inherited Raychaudhuri law is the twist-free null-horizon germ, and zero initial expansion and shear are equilibrium hypotheses. No area law is integrated; no stress tensor, Unruh relation, EFE, or ledger-to-geometry bridge is introduced.
Upstream, the Raychaudhuri slope is the scalar RHS $d\theta/d\lambda=-\tfrac12\theta^2-\sigma^2-R_{ab}k^ak^b$, treated as real arithmetic with no spacetime geometry imported. The scaled area-rate slope is the arithmetic second derivative under the deformed law $A'=c,\theta A$, formed by the product rule against that Raychaudhuri slope.
proof idea
One-line term proof: unfold the scaled area-rate slope and the Raychaudhuri slope, then discharge the numerical inequality by norm_num. At $c=2$, $\theta=0$, $\sigma^2=0$, $R=1$, $A=1$ the Raychaudhuri slope is $-1$ and the scaled second-area rate is $2\cdot(-1)=-2$, hence unequal to $-1$.
why it matters
Arithmetic decoy isolating the unit coefficient in $A'=\theta A$. The module doc states that such decoys show zero expansion, zero shear, and unit normalization are load-bearing for the equilibrium second variation. Sibling decoys handle nonzero expansion and nonzero shear; this one shows that $c=2$ at the equilibrium witness yields $-2$ rather than the unit-law target $-1$ (matching $-A R$ only when $c=1$). No downstream consumers are wired yet. It lives in the relativity geometry layer and does not touch the T0–T8 forcing chain, RCL, phi, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.