LocalAreaCongruenceData
plain-language theorem explainer
Packages local scalar Raychaudhuri data with a cross-sectional area curve whose rate is fixed by the model law A' = θ A. Relativists and RS geometry workers cite it as the input bundle for equilibrium second-area variation. It is a pure structure: inheritance plus one HasDerivAt premise, no proof body.
Claim. A local area-congruence datum is a local scalar Raychaudhuri datum (expansion $\theta$, squared shear $\sigma^2$, null Ricci $R_{kk}$, and the twist-free null-horizon Raychaudhuri ODE) together with a real function $A(\lambda)$ such that for every affine parameter $\lambda$, $A$ is differentiable at $\lambda$ with derivative $\theta(\lambda)\,A(\lambda)$. The area-rate law is an explicit model premise, not an integrated area formula.
background
The module studies local equilibrium area variation: it adjoins the explicit area-rate model $A'=\theta A$ to the scalar Raychaudhuri model and derives the second area variation at one equilibrium point. Honesty tags stress that both differential laws are model interfaces; zero initial expansion and shear are equilibrium hypotheses; no stress tensor, Unruh relation, EFE, or ledger-to-geometry bridge is introduced.
Upstream, LocalRaychaudhuriData supplies three real functions along an affine parameter—expansion, squared shear, and null Ricci—plus the model ODE for twist-free null-horizon expansion. The present structure extends that bundle by a cross-sectional area $A:\mathbb{R}\to\mathbb{R}$ and the pointwise law $\mathrm{d}A/\mathrm{d}\lambda=\theta(\lambda)A(\lambda)$, stated as HasDerivAt rather than as a global integrated formula.
In classical GR this is the standard infinitesimal area evolution for a null congruence; here it remains a named model premise so that later calculus theorems stay conditional on exactly those two geometric laws.
proof idea
No proof: this is a structure definition. It extends the upstream local Raychaudhuri data record and adds two fields—an area map and a universal HasDerivAt premise encoding $A'=\theta A$. Downstream lemmas read those fields directly (e.g. product rule on the two model laws, then specialization at $\theta(0)=\sigma^2(0)=0$).
why it matters
This is the carrier type for the module's equilibrium second-area calculus. Parent results include the global derivative form of the area-rate model, the product-rule derivative of the area rate before equilibrium, and the equilibrium identities $\mathrm{d}^2A/\mathrm{d}\lambda^2|{0}=-A(0),R{kk}(0)$ in both HasDerivAt and pointwise deriv form, plus the iterated-derivative packaging. A sibling matrix-form theorem in LocalAreaRaychaudhuri reuses the same area-law shape with definitional transport of null Ricci.
Within Recognition Science this sits in the relativity geometry layer that prepares local focusing statements without claiming EFE matching or ledger bridges. It does not touch T5–T8, RCL, or the alpha band; it is pure conditional calculus on two geometric model laws. Arithmetic decoys elsewhere in the module show that vanishing expansion, vanishing shear, and the unit factor in $A'=\theta A$ are load-bearing for the equilibrium conclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.