not_split_signature
plain-language theorem explainer
The theorem shows that the temporal dimension count cannot equal two. Researchers deriving Lorentzian spacetime from J-cost minimization would cite it to confirm the single temporal direction required by the eight-tick octave. The proof reduces directly to the definition of temporal dimension via simplification.
Claim. The number of temporal dimensions is not two: $d_t = 1$ implies $¬(d_t = 2)$, where $d_t$ is the temporal dimension count fixed by the octave advance.
background
The module derives the full 4D Lorentzian structure (signature (−,+,+,+), light cone, arrow of time) from the J-cost functional and the T0–T8 forcing chain. Key local definitions include the temporal dimension count as the unique cost-reducing direction under the 8-tick recognition operator. The upstream result temporal_dim supplies the concrete value: temporal_dim : ℕ := 1, described as the number of temporal dimensions exactly equal to one (the octave advance).
proof idea
One-line wrapper that applies simp to the definition of temporal_dim.
why it matters
This declaration supports the central theorem that 4D Lorentzian spacetime emerges from J-cost (SE-001 through SE-010). It locks the temporal half of the derivation RCL → J-uniqueness (T5) → 8-tick octave (T7) + D = 3 (T8) → η = diag(−1,+1,+1,+1). The result closes a possible split in the dimension count before the full spacetime_dim_eq_four theorem is reached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.