not_three_temporal
plain-language theorem explainer
The declaration shows the temporal dimension count cannot equal three. Researchers deriving Lorentzian spacetime from J-cost minimization and the T0-T8 chain would cite it to exclude non-octave temporal structures. The proof reduces directly to the definition of temporal_dim as one via a single simplification step.
Claim. Let $N_t$ be the number of temporal dimensions. Then $N_t = 1$, so in particular $N_t ≠ 3$.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure (signature (−,+,+,+), light cones, arrow of time) from the J-cost functional and the forcing chain T0–T8. Temporal direction is singled out because the 8-tick recognition operator reduces cost, while spatial directions raise it quadratically via J''(1) = 1. The upstream definition states that the number of temporal dimensions equals exactly one, the octave advance.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of temporal_dim.
why it matters
The result supports the central claim of the module that spacetime is a theorem of cost minimization, not a background. It excludes three temporal dimensions so that one temporal octave (T7) plus three spatial dimensions (T8) yields the observed 4D Lorentzian geometry. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.