scaledAreaRateSlope
plain-language theorem explainer
Packages the second time-derivative of cross-sectional area under a scaled area law A' = c θ A, inserting the Raychaudhuri slope for θ'. Horizon and local-equilibrium auditors cite it when testing that the unit coefficient c = 1 is load-bearing. The body is pure arithmetic (product rule), not a proved identity.
Claim. For real parameters $c$, $\theta$, $\sigma^2$, $R_{\mathrm{null}}$, and $A$, define the scaled area-rate slope by $c\bigl(S(\theta,\sigma^2,R_{\mathrm{null}})\,A + \theta\cdot(c\,\theta\,A)\bigr)$, where $S$ is the Raychaudhuri slope of the expansion. This is the formal second derivative of the model law $A' = c\,\theta\,A$.
background
The module works in a local null-congruence setting with two explicit MODEL interfaces: a twist-free scalar Raychaudhuri law for the expansion $\theta$, and an area-rate law $A' = \theta A$ (unit coefficient). Equilibrium means vanishing initial expansion and shear; the second area variation is then a pure calculus consequence of those two laws.
The unscaled sibling packages $A''$ at a point via the product rule $A'' = \theta' A + \theta A'$, with $\theta'$ replaced by the Raychaudhuri slope (shear-squared and null Ricci terms). The present definition inserts a free coefficient $c$ into the area law, so $A' = c,\theta,A$ and the second derivative becomes $c(\theta' A + c,\theta^2 A)$.
Module honesty tags stress that no area law is integrated, and no stress tensor, Unruh relation, EFE, or ledger-to-geometry bridge is assumed. The construction exists to support arithmetic decoys that isolate which normalizations are load-bearing.
proof idea
Definitional, not a proof. Expand the product rule under the scaled model $A' = c,\theta,A$: differentiate once more to get $A'' = c(\theta' A + \theta A')$, substitute $A' = c,\theta,A$ again, and replace $\theta'$ by the already-defined Raychaudhuri slope in $(\theta,\sigma^2,R_{\mathrm{null}})$. The resulting closed-form expression in five real scalars is the body.
why it matters
Feeds the normalization decoy decoy_areaLaw_coefficient_two_changes_equilibrium, which evaluates this expression at the equilibrium witness $\theta=0$, $\sigma^2=0$, $R=1$, $A=1$ with $c=2$ and obtains second-area rate $-2$, not the unit-law value $-1$. That decoy is the module's explicit check that the coefficient in $A' = \theta A$ is load-bearing for the equilibrium second variation.
In the broader Recognition geometry stack this sits downstream of the local Raychaudhuri reduction and upstream of any claim that the equilibrium area curvature matches a unit-normalized null-focusing law. It does not itself touch T0–T8, the RCL, or the phi ladder; it is a calculus packaging step that keeps the area-law coefficient visible so decoys can kill silent rescalings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.