lightlike_iff_speed_c
plain-language theorem explainer
The equivalence states that a 4-vector displacement is lightlike precisely when its spatial quadratic form equals its temporal quadratic form. Researchers deriving Lorentzian geometry from J-cost minimization would cite this when establishing the causal light cone. The proof is a one-line term wrapper that rewrites the interval via its spatial-minus-temporal identity and closes the biconditional with linear arithmetic.
Claim. For a spacetime displacement $v = (v_0, v_1, v_2, v_3) $, the interval satisfies $ds^2(v) = 0$ if and only if $|v_1|^2 + |v_2|^2 + |v_3|^2 = v_0^2$, where the metric signature is $(-1, +1, +1, +1)$.
background
The Spacetime Emergence module derives 4D Lorentzian geometry from the J-cost functional and the T0-T8 forcing chain. Displacement is the 4-vector $(Δt, Δx_1, Δx_2, Δx_3)$. The interval is defined as $∑ η_{ii} v_i^2$ with $η = diag(-1,1,1,1)$. Spatial norm squared sums the three spatial components while temporal squared isolates the time component. The upstream lemma interval_eq_spatial_minus_temporal states that the interval equals spatial norm squared minus temporal squared.
proof idea
The term proof first rewrites the interval using the lemma interval_eq_spatial_minus_temporal, converting the goal into spatial_norm_sq v - temporal_sq v = 0. It then applies constructor to split the biconditional and linarith on each direction to obtain the required equality of quadratic forms.
why it matters
This equivalence supplies the light-cone condition inside the spacetime emergence certificate and the master forcing theorem reality_from_one_distinction. It realizes the causal structure forced by J-uniqueness (T5), the eight-tick octave (T7), D = 3 (T8), and the resulting Lorentzian signature with c = 1. The result closes one link in the chain from RCL to E² = p² + m².
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Lattice Weyl fermion gets an exact chiral symmetry, no doubling
"a single Weyl fermion ... protected by an emanant U(1) chiral symmetry which is also ultralocally generated but not quantized in the UV"