not_three_temporal
plain-language theorem explainer
The theorem shows that the number of temporal dimensions cannot equal three. Workers deriving Lorentzian geometry from the J-cost functional and T0-T8 chain would cite it to exclude three-dimensional time. The proof is a one-line simplification that invokes the definition fixing temporal dimensions at one.
Claim. $N_t$ denotes the number of temporal dimensions. Then $N_t$ is not equal to 3.
background
The module derives the full 4D Lorentzian structure (signature (−,+,+,+), light cone, arrow of time) from the J-cost functional and the forcing chain T0–T8. Temporal dimension is defined as exactly one, corresponding to the octave advance of the eight-tick recognition operator. The upstream definition states: “The number of temporal dimensions: exactly 1 (the octave advance).” This pairs with the spatial count D = 3 forced by T8 to produce total dimension four.
proof idea
One-line wrapper that applies simp to the definition of temporal_dim, which evaluates to 1, immediately yielding the negation of equality with 3.
why it matters
The result closes off an alternative dimension count inside the spacetime-emergence registry (SE-001 through SE-010). It directly supports the central claim that spacetime metric signature and causal structure are theorems of cost minimization rather than background postulates. It aligns with T7 (eight-tick temporal direction) and T8 (D = 3 spatial) while feeding the downstream construction of spacetime_dim_eq_four.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.