timelike_iff
plain-language theorem explainer
Timelike separation on ℝ^{1,3} is equivalent to the open light-cone inequality x²+y²+z² < t². Anyone working the causal trichotomy or continuum limit from ledger sites to Minkowski space cites this. The proof unfolds the Minkowski form and closes both directions by linear arithmetic.
Claim. For all real $t,x,y,z$, the event $(t,x,y,z)$ is timelike (Minkowski quadratic form $s^2=-t^2+x^2+y^2+z^2$ strictly negative) if and only if $x^2+y^2+z^2<t^2$.
background
The module ContinuumManifoldEmergence is the zero-parameter bridge from discrete RS ledger sites to Lorentzian spacetime: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then Minkowski flat limit and curved metric from defect. Architecture step 1 fixes the Minkowski form $\eta$ on $\mathbb{R}^{1,3}$ by $s^2=-t^2+x^2+y^2+z^2$; step 3 builds the causal trichotomy (timelike / spacelike / lightlike).
minkowski_form is that quadratic form. is_timelike is the predicate $s^2<0$ (inside the light cone). Signature and light-cone structure are listed as unconditionally proved in this module; $c=1$ voxel per tick and $D=3$ enter from DimensionForcing and the tick/voxel asymmetry elsewhere in the chain.
proof idea
Term-mode proof by unfolding. Expand is_timelike to minkowski_form t x y z < 0, then expand the form to $-t^2+x^2+y^2+z^2<0$. Split the biconditional; each direction is closed by linarith (rearrangement of the quadratic inequality). No external lemmas beyond the two local definitions.
why it matters
Fills the doc-commented claim "Timelike ↔ Inside Cone" in the causal-structure block of ContinuumManifoldEmergence. That block is the foundation for light-cone speed limit $c=1$ voxel/tick and for the later ADM / weak-field path to Einstein equations. Lorentzian signature itself is forced by tick/voxel asymmetry (not fit), matching the module's zero-parameter stance versus phenomenological ILG kernels. No downstream uses are recorded yet; siblings causal_trichotomy and light_cone_speed_limit are the natural consumers. Ties to framework landmarks T7 (eight-tick octave) and T8 ($D=3$) only indirectly via the ambient continuum-limit story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.