signature_unique
plain-language theorem explainer
The theorem establishes that the only RS-compatible spacetime signature is one temporal dimension paired with three spatial dimensions. Researchers deriving Lorentzian geometry from the J-cost functional and the T0-T8 chain would cite this uniqueness result. The proof is a short term-mode construction that applies reflexivity to the dimension equalities and reduces the forall clause by substitution into the total-dimension equality followed by arithmetic resolution.
Claim. The temporal dimension equals one and the spatial dimension equals three, and for any natural numbers $d_t$ and $d_s$ satisfying $d_t + d_s$ equal to the total spacetime dimension, the assumption $d_t = 1$ forces $d_s = 3$.
background
The Spacetime Emergence module shows that the full 4D Lorentzian structure, including metric signature diag(-1,+1,+1,+1), arises from the J-cost functional via the forcing chain T0-T8. The eight-tick octave (T7) selects the temporal direction as the unique cost-reducing axis, while T8 fixes three spatial dimensions. Upstream results fix the total spacetime dimension at four and supply the gap as the product of closure and Fibonacci factors; the sibling equality spacetime_dim_eq_four supplies the concrete value used in the uniqueness argument.
proof idea
The term proof refines a triple whose first two components are reflexivity proofs for the temporal and spatial dimension equalities. The third component is a lambda that receives the sum hypothesis and the temporal-equals-one hypothesis, rewrites the sum using the total-dimension-equals-four lemma, and invokes the omega tactic to obtain the required spatial-dimension conclusion.
why it matters
As SE-010 this result completes the spacetime-emergence registry and confirms that the (1,3) signature is the sole RS-compatible choice. It supports the central module claim that spacetime itself is a theorem of cost minimization, incorporating the eight-tick octave (T7) and D=3 (T8) without free parameters. The proof is closed; no scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.