causal_trichotomy
plain-language theorem explainer
Every real 4-displacement is timelike, spacelike, or lightlike under the Minkowski form s² = −t² + x² + y² + z². Gravity and continuum-limit arguments cite it to lock causal structure before the N→∞ bridge. The proof is a one-step case split on the real trichotomy of s² versus zero.
Claim. For all real coordinates $t,x,y,z$, writing $s^2 = -t^2 + x^2 + y^2 + z^2$, one has $s^2 < 0$ or $s^2 > 0$ or $s^2 = 0$ (timelike, spacelike, or lightlike separation).
background
The module ContinuumManifoldEmergence is the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice → quadratic cost → Laplacian → Lorentzian interval → Minkowski flat limit → curved metric from defect → Einstein equations. Architecture step 1 fixes the Minkowski form η on ℝ^{1,3} by s² = −t² + x² + y² + z²; step 3 is the causal trichotomy.
Sibling predicates package the three cones: timelike means s² < 0, spacelike means s² > 0, and lightlike (null) means s² = 0. Signature lemmas already show the temporal direction is negative and each spatial axis is positive, so the form is Lorentzian rather than Euclidean. RS-native units set c = ℓ₀/τ₀ = 1 voxel per tick, so the null cone is the discrete speed limit once the continuum limit is taken.
Upstream forcing (D = 3, eight-tick period) fixes the ambient dimension in which this 1+3 split lives; the present lemma only needs the ordered field structure of ℝ.
proof idea
Term-mode case analysis on lt_trichotomy applied to minkowski_form t x y z versus 0. The three exhaustive branches of the real order (strictly less, equal, strictly greater) are mapped, in order, to the left disjunct (timelike), the nested right-right disjunct (lightlike), and the nested right-left disjunct (spacelike). No further lemmas are required: the definitions of the three predicates are literally the three comparisons of s² to zero.
why it matters
Causal structure is architecture item 3 of the continuum bridge and is listed among the unconditional proved facts of the module (Lorentzian signature, light cone, causal structure, flat Minkowski limit). Downstream, continuum_limit_certificate packages it as the causal_classification field of ContinuumLimitCert, so every consumer of the master certificate inherits a complete timelike/spacelike/null partition.
In the RS chain this sits after T8 (D = 3 forced) and after the tick/voxel asymmetry that forces Lorentzian signature; it precedes the light-cone speed-limit theorem (c = 1 voxel/tick) and the weak-field path to the Einstein equations. Without trichotomy the continuum limit would not yet be a causal Lorentzian manifold in the sense the certificate claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.