adm_is_minkowski
plain-language theorem explainer
For unit lapse and identity spatial metric, the ADM interval equals the Minkowski quadratic form on every real displacement. Continuum-limit and zero-parameter gravity arguments cite this to identify the flat RS limit with special-relativistic geometry. The proof is a pure algebraic identity: unfold both definitions and close by ring.
Claim. For all real $dt,dx,dy,dz$, the ADM interval with lapse $N=1$ and diagonal spatial factor $h=1$ equals the Minkowski form: $-(1\cdot dt)^2 + 1\cdot(dx^2+dy^2+dz^2) = -dt^2 + dx^2 + dy^2 + dz^2$.
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, then curved metric from defect and Einstein equations. Lorentzian signature, $c=\ell_0/\tau_0$, spatial metric from $J''(1)=1$, and $D=3$ are forced rather than fit.
The ADM interval is the standard 3+1 decomposition with zero shift: $ds^2=-N^2,dt^2+h(dx^2+dy^2+dz^2)$, with lapse $N$ and diagonal spatial factor $h$. The Minkowski form on $\mathbb{R}^{1,3}$ is $s^2=-t^2+x^2+y^2+z^2$. An upstream spacetime-emergence interval packages the same quadratic form via the diagonal $\eta=\mathrm{diag}(-1,1,1,1)$.
The claim is the flat specialization: unit lapse and identity spatial metric recover Minkowski exactly, which the module lists among the unconditional flat-space results.
proof idea
Term-style tactic proof with no lemmas beyond the two local definitions. Unfold adm_interval and minkowski_form, substitute $N=1$ and $h=1$, and finish by ring: $-(1\cdot dt)^2+1\cdot(dx^2+dy^2+dz^2)$ rewrites to $-dt^2+dx^2+dy^2+dz^2$. Pure polynomial identity; no analytic or continuum hypotheses.
why it matters
Pins architecture step 8 (ADM decomposition) to step 1 (Minkowski form $\eta$): the flat ADM slice is literally Minkowski, so the continuum limit is special-relativistic before defects curve the metric. Downstream, continuum_limit_certificate packages the proved continuum fields (temporal negativity, spatial positivity, causal trichotomy); this identity is the algebraic backbone that those signature and causal lemmas sit on when the metric is flat.
In the broader RS chain it closes the "flat-space limit = Minkowski" bullet of the module's proved list, after DimensionForcing ($D=3$) and the J-cost spatial metric from $J''(1)=1$. Curvature and Einstein equations enter only later via defect perturbations; this declaration stays in the zero-parameter flat sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.