The longest causal chain is a Lorentzian distance on record events

Category: 3-Local (CV; the event layer of ST-1). BACKLOG #111, the first of the two geometry bricks priced in the records→spacetime answer.

RecordCausalOrder.lean gives a partial order on record events (isPartialOrder_causalPrecedes) and #98 gives a cone with a boost symmetry. Neither gives a distance: before this file the event order carried no interval, no chain length and no numerical separation at all. This file supplies the causal-set one — the length of the longest chain — and proves the two properties that make it Lorentzian rather than metric.

What is proved

• strictPrecedes E — strict causal precedence as a relation chains can run on, with isTrans_strictPrecedes (transitive because the order is antisymmetric: a strict step cannot return);
• causalDist E e₁ e₂ — the length of the longest causal chain from e₁ to e₂, as the supremum of chainLengths. It is well defined because ★★ bddAbove_chainLengths: a chain's events are distinct and all lie between e₁ and e₂, so there are at most 2 ^ K · (e₂.time + 1 − e₁.time) of them — ★ causalDist_le states that bound, and it is the finiteness of the arena doing the work, not an assumption about the order;
• ★★★ causalDist_add_le — the reverse triangle inequality: causalDist e₁ e₂ + causalDist e₂ e₃ ≤ causalDist e₁ e₃ for e₁ ⪯ e₂ ⪯ e₃. This is the signature of Lorentzian geometry and the discrete twin paradox: going by way of e₂ is never longer than the longest path, so the longest chain is the straight one. A metric satisfies the inequality the other way;
• ★★ causalDist_pos_iff — the distance is positive exactly on the strictly causally related pairs, so it vanishes exactly on the spacelike-or-equal ones, and ★ causalDist_self, ★ causalDist_eq_zero_of_not_causalPrecedes for the two ways of vanishing;
• ★ causalDist_le_of_causalPrecedes_right — and it is monotone into the causal future, which is the reverse triangle inequality with one leg thrown away.

Honest scope

⚠️ This is not the metric, and order plus length is not order plus volume. The classical route from a causal order to a Lorentzian metric (Hawking–King–McCarthy and Malament for manifolds, "order plus number equals geometry" for causal sets) determines the metric only up to a conformal factor from the order, and fixes the factor from a volume element. This corpus has no volume element on the event order — the measure it has lives on Σ and weights events by Born probability, which is not a spacetime volume. That companion brick is not built here and nothing below pretends it is.

⚠️ No embedding, and none is available. That a discrete order with a volume is approximated by a Lorentzian manifold is a programme (sprinkling; the Hauptvermutung is open), not a theorem, so no statement here says the event order is a spacetime, or that causalDist approximates a proper time.

⚠️ Relative to a coupling graph. Everything is stated for a fixed E, exactly as ST-1 is: the causal structure is relative to an assumed interaction graph and is not derived from Σ.

⚠️ No continuum limit, no curvature, no dimension estimator. The chain length is an integer on a finite interval; nothing is said about limits of refinements, about dimension, or about any geometric invariant beyond the two properties listed.

⚠️ causalDist is 0 on unrelated pairs by construction (sSup ∅ = 0 in ℕ), which is the usual convention for a Lorentzian distance — spacelike separation has no timelike path, not a negative one. It means causalDist is not a metric and its vanishing does not imply equality; that is causalDist_pos_iff's content, not a defect.

References: records-to-spacetime-scoping.md §8 and ST-1; future-work.md; RecordCausalOrder.lean (CausalPrecedes, isPartialOrder_causalPrecedes, EventSpacelike), TwoCones.lean (#98); L. Bombelli, J. Lee, D. Meyer, R. Sorkin, Space-time as a causal set, PRL 59 (1987) 521; D. Malament, The class of continuous timelike curves determines the topology of spacetime, J. Math. Phys. 18 (1977) 1399; specs/BACKLOG.md #111, #98, #39, #38.

Strict causal precedence, as a relation chains run on

def CSD.CV.strictPrecedes {K : ℕ} (E : Finset (Fin K × Fin K)) : SetRel (RecordEvent K) (RecordEvent K)

Strict causal precedence: e₁ is in the causal past of e₂ and is a different event. The relation a causal chain steps along.

Equations

• CSD.CV.strictPrecedes E = {q : CSD.CV.RecordEvent K × CSD.CV.RecordEvent K | CSD.CV.CausalPrecedes E q.1 q.2 ∧ q.1 ≠ q.2}

theorem CSD.CV.mem_strictPrecedes {K : ℕ} {E : Finset (Fin K × Fin K)} {a b : RecordEvent K} : (a, b) ∈ strictPrecedes E ↔ CausalPrecedes E a b ∧ a ≠ b

theorem CSD.CV.causalPrecedes_of_strictPrecedes {K : ℕ} {E : Finset (Fin K × Fin K)} {a b : RecordEvent K} (h : (a, b) ∈ strictPrecedes E) : CausalPrecedes E a b

theorem CSD.CV.ne_of_strictPrecedes {K : ℕ} {E : Finset (Fin K × Fin K)} {a b : RecordEvent K} (h : (a, b) ∈ strictPrecedes E) : a ≠ b

theorem CSD.CV.isTrans_strictPrecedes {K : ℕ} (E : Finset (Fin K × Fin K)) : (strictPrecedes E).IsTrans

★ Strict precedence is transitive — and it is antisymmetry that makes it so: a strict step cannot return, so the composite is strict as well as causal.

The chain lengths between two events

def CSD.CV.chainLengths {K : ℕ} (E : Finset (Fin K × Fin K)) (e₁ e₂ : RecordEvent K) : Set ℕ

The lengths of the causal chains from e₁ to e₂.

Equations

• CSD.CV.chainLengths E e₁ e₂ = {n : ℕ | ∃ (p : RelSeries (CSD.CV.strictPrecedes E)), p.head = e₁ ∧ p.last = e₂ ∧ p.length = n}

theorem CSD.CV.chainLengths_le {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} {n : ℕ} (hn : n ∈ chainLengths E e₁ e₂) : n ≤ 2 ^ K * (e₂.time + 1 - e₁.time)

★★ A chain is bounded by the arena. Its events are distinct — a strict chain cannot repeat — and all lie between the endpoints in time, so there are at most 2 ^ K · (e₂.time + 1 − e₁.time) of them. The finiteness doing the work is the arena's, not an assumption about the order.

theorem CSD.CV.bddAbove_chainLengths {K : ℕ} (E : Finset (Fin K × Fin K)) (e₁ e₂ : RecordEvent K) : BddAbove (chainLengths E e₁ e₂)

The distance

noncomputable def CSD.CV.causalDist {K : ℕ} (E : Finset (Fin K × Fin K)) (e₁ e₂ : RecordEvent K) : ℕ

The Lorentzian distance on record events: the length of the longest causal chain from e₁ to e₂, and 0 when there is none.

Equations

• CSD.CV.causalDist E e₁ e₂ = sSup (CSD.CV.chainLengths E e₁ e₂)

theorem CSD.CV.causalDist_le {K : ℕ} (E : Finset (Fin K × Fin K)) (e₁ e₂ : RecordEvent K) : causalDist E e₁ e₂ ≤ 2 ^ K * (e₂.time + 1 - e₁.time)

★ The distance is bounded by the arena, explicitly.

theorem CSD.CV.zero_mem_chainLengths {K : ℕ} (E : Finset (Fin K × Fin K)) (e : RecordEvent K) : 0 ∈ chainLengths E e e

theorem CSD.CV.one_mem_chainLengths {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : (e₁, e₂) ∈ strictPrecedes E) : 1 ∈ chainLengths E e₁ e₂

theorem CSD.CV.nonempty_chainLengths_of_causalPrecedes {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : CausalPrecedes E e₁ e₂) : (chainLengths E e₁ e₂).Nonempty

theorem CSD.CV.causalDist_mem_chainLengths {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : CausalPrecedes E e₁ e₂) : causalDist E e₁ e₂ ∈ chainLengths E e₁ e₂

The longest chain is attained: the supremum is itself a chain length.

It vanishes exactly on the spacelike-or-equal pairs

theorem CSD.CV.causalDist_eq_zero_of_not_causalPrecedes {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : ¬CausalPrecedes E e₁ e₂) : causalDist E e₁ e₂ = 0

theorem CSD.CV.causalDist_self {K : ℕ} (E : Finset (Fin K × Fin K)) (e : RecordEvent K) : causalDist E e e = 0

★ A record is at no distance from itself.

theorem CSD.CV.causalDist_pos_iff {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} : 0 < causalDist E e₁ e₂ ↔ CausalPrecedes E e₁ e₂ ∧ e₁ ≠ e₂

★★ The distance is positive exactly on the strictly causally related pairs — so it vanishes exactly on the pairs that are spacelike or equal, which is what a Lorentzian distance does.

The reverse triangle inequality

theorem CSD.CV.causalDist_add_le {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ e₃ : RecordEvent K} (h₁ : CausalPrecedes E e₁ e₂) (h₂ : CausalPrecedes E e₂ e₃) : causalDist E e₁ e₂ + causalDist E e₂ e₃ ≤ causalDist E e₁ e₃

★★★ The reverse triangle inequality — the signature of Lorentzian geometry, and the discrete twin paradox: a path through e₂ is never longer than the longest path, so the longest chain is the straight one. A metric satisfies the inequality the other way round.

The proof is chain concatenation: the longest chains to and from e₂ are attained (causalDist_mem_chainLengths), and smashing them gives a chain of the summed length.

theorem CSD.CV.causalDist_le_of_causalPrecedes_right {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ e₃ : RecordEvent K} (h₁ : CausalPrecedes E e₁ e₂) (h₂ : CausalPrecedes E e₂ e₃) : causalDist E e₁ e₂ ≤ causalDist E e₁ e₃

★ And the distance is monotone into the causal future: the reverse triangle inequality with one leg discarded.