adm_interval
plain-language theorem explainer
Defines the ADM line element with lapse N, diagonal spatial metric h, and vanishing shift: ds² = −N² dt² + h(dx²+dy²+dz²). Gravity and continuum-limit arguments cite it as the discrete-to-continuum interval before specializing to Minkowski. The body is a direct algebraic abbreviation of that quadratic form.
Claim. The ADM interval with lapse $N$, diagonal spatial coefficient $h$, and zero shift is the real quadratic form $ds^2 = -N^2\,dt^2 + h\,(dx^2 + dy^2 + dz^2)$ on displacements $(dt,dx,dy,dz)$.
background
The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then Minkowski flat limit, then curved metric from defect. Architecture step 8 is the ADM decomposition (lapse plus spatial metric) that packages a Lorentzian interval on $\mathbb{R}^{1,3}$.
Sibling definitions already fix the flat Minkowski form $\eta(dt,dx,dy,dz) = -dt^2 + dx^2 + dy^2 + dz^2$, the signature signs (temporal negative, spatial positive), and the causal trichotomy (timelike / spacelike / lightlike). The ADM form generalizes that flat interval by a positive lapse $N$ and a positive diagonal spatial factor $h$, still with zero shift, matching the classical 3+1 split used before weak-field curvature is restored.
Upstream continuum and dimension-forcing material supplies $D=3$ spatial directions and the continuum limit of the discrete Laplacian; the present definition only names the interval polynomial those results will specialize.
proof idea
Definitional abbreviation only: the right-hand side is the expanded quadratic form $-(N,dt)^2 + h(dx^2+dy^2+dz^2)$. No lemmas are applied; downstream theorems unfold this def and simplify by ring or positivity of squares.
why it matters
This is the ADM packaging step in the continuum-manifold bridge. Immediate parents are adm_is_minkowski (lapse $=1$, $h=1$ recovers the Minkowski form), adm_temporal_timelike (pure time displacements have negative interval for $N>0$), and adm_spatial_spacelike (pure space displacements have positive interval for $h>0$). Those feed the master ContinuumLimitCert, which records forced Lorentzian signature and the flat-space limit.
In the Recognition chain this sits after T7/T8 (eight-tick octave and $D=3$) and after spatial metric forcing from $J''(1)=1$: the interval is how the discrete tick/voxel asymmetry becomes a continuum Lorentzian form before weak-field defects produce Einstein equations. It is scaffolding for geometry, not a dynamical field equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.