adm_temporal_timelike
plain-language theorem explainer
Purely temporal ADM displacements (nonzero time step, vanishing spatial steps) yield a strictly negative interval when the lapse is positive. Relativists and continuum-limit workers cite this to lock the temporal leg of the Lorentzian signature in the RS ADM chart. The proof unfolds the ADM interval and finishes by positivity of squares.
Claim. Let $N>0$ be the ADM lapse and $dt\neq 0$. With unit spatial diagonal metric and vanishing spatial increments, the ADM interval satisfies $-N^{2}\,dt^{2}<0$.
background
This 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 and weak-field curvature. Signature is forced by tick/voxel asymmetry; the spatial metric by $J''(1)=1$; $c=\ell_0/\tau_0$ by one voxel per tick; $D=3$ by DimensionForcing.
The ADM interval (zero shift, diagonal spatial metric $h$) is $ds^{2}=-N^{2}dt^{2}+h(dx^{2}+dy^{2}+dz^{2})$. Siblings define the Minkowski form $\eta$ on $\mathbb{R}^{1,3}$, the predicates timelike/spacelike/lightlike, and causal trichotomy. The related spacetime interval on a four-displacement is $\sum_i\eta_{ii}v_i^{2}$.
proof idea
Unfold the ADM interval definition, simplify the pure-temporal specialization ($h=1$, $dx=dy=dz=0$) to $-N^{2}dt^{2}$, then apply nonlinear arithmetic. The only inputs are $dt\neq 0$ and $N>0$, which give $dt^{2}>0$ and $N^{2}>0$ via square-positivity, so the product is positive and the whole expression is strictly negative.
why it matters
Locks the temporal half of the Lorentzian signature in the ADM chart that the module uses to pass from discrete ledger geometry to continuum gravity. Together with the companion spatial-spacelike statement and the Minkowski-form siblings, it underwrites causal trichotomy and the light-cone speed limit ($c=1$ voxel/tick) listed as unconditional in the module architecture.
In the broader RS chain this is the continuum face of the forcing that already fixes $D=3$ (T8) and the eight-tick octave (T7): time is the distinguished negative direction once the tick structure is continuum-extended. No downstream dependents are recorded yet; the natural consumers are the causal-structure and weak-field Einstein-equation certificates in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.