not_euclidean
The theorem asserts that the temporal dimension count cannot be zero under the Recognition Science forcing chain. Researchers deriving Lorentzian spacetime from J-cost minimization would cite it when excluding Euclidean signatures that lack an arrow of time. The proof reduces directly to the definition of temporal_dim via a single simplification step.
claimThe number of temporal dimensions is not zero: $d_t ≠ 0$, where $d_t$ is the count of the unique cost-reducing direction forced by the eight-tick octave.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure (metric signature (−,+,+,+), light cone, arrow of time) from the J-cost functional and the T0–T8 chain rather than postulating background spacetime. Key upstream definition: temporal_dim := 1, described as the number of temporal dimensions exactly equal to one (the octave advance). This places the result inside the exclusion of alternative signatures section, which follows the central theorem that spacetime itself is a cost-minimization theorem.
proof idea
One-line wrapper that applies the simp tactic to the definition of temporal_dim, which evaluates to 1 and therefore cannot equal zero.
why it matters in Recognition Science
It fills the exclusion step in §10 of the module, reinforcing the derivation of η = diag(−1, +1, +1, +1) from RCL, J-uniqueness (T5), eight-tick octave (T7), and D = 3 (T8). The result supports the arrow-of-time claim (SE-009) that recognition advances monotonically and aligns with sibling results on Lorentzian signature and spacetime dimension four. No open questions are directly closed here.
scope and limits
- Does not prove the numerical value of temporal_dim.
- Does not derive the spatial dimension count or full metric tensor.
- Does not address J-cost positivity or eigenvalue counts.
- Does not connect to mass ladder or coupling constants.
formal statement (Lean)
321theorem not_euclidean : ¬(temporal_dim = 0) := by simp [temporal_dim]