Registry · Remark V.R17 tau-effective formalized

V.R17 — Spacelike separation on T^2

The alpha-orbit is totally ordered so there is no spacelike separation along tau^1. Spacelike separation arises on the fiber T^2: two events at the same refinement depth n but different fiber coordinates (B_1,C_1) != (B_2,C_2) are simultaneous but spatially separated.

Book V Part 1 Ch. 4

Lean Formalization

Module: TauLib.BookV.Temporal.BaseCircle

Symbol: Tau.BookV.Temporal.SpacelikeSeparationOnT2