Chronological precedence: the causal order with its same-period steps removed

Category: 3-Local (CV; the event layer of ST-1). BACKLOG #192 (out of #39; the second of #191–#197).

CausalPrecedes E e₁ e₂ allows e₁.time = e₂.time with e₁.region ⊆ e₂.region-type steps: a region-inclusion step at an unchanged period index is a strict causal step, and CausalDistance.lean counts it. That is exactly how the inflation theorems of #188 and #190 are built: inserting "both ends of the edge, at the period of the reception" between the emission and the reception adds a strict step with no elapsed period. This file names the sub-relation whose strict part demands a strictly later period, and proves what it changes and what it does not.

• ChronoPrecedes E e₁ e₂ := CausalPrecedes E e₁ e₂ ∧ (e₁ = e₂ ∨ e₁.time < e₂.time); ChronoPrecedes.causalPrecedes — it is a sub-relation; chronoPrecedes_iff_of_time_ne — on events of distinct periods the two relations agree; chronoPrecedes_of_causalPrecedes_of_lt; ★ not_chronoPrecedes_of_time_eq — distinct simultaneous events are chrono-incomparable (this is how simultaneous writes are handled: neither precedes the other);
• ★ isPartialOrder_chronoPrecedes — a partial order (chronoPrecedes_refl/trans/antisymm);
• strictChrono E — the strict part as a relation chains run on; ★ time_lt_of_strictChrono — its strict part excludes every transition with unchanged period; isTrans_strictChrono, isIrrefl_strictChrono (so a strict chrono chain is acyclic: the period strictly increases along it, time_add_length_le_of_chain); strictChrono_le_strictPrecedes — every chrono step is a causal step;
• chronoChainLengths, chronoDist — the longest chrono chain, built exactly as causalDist; ★★ chronoChainLengths_le_elapsed, ★★ chronoDist_le_elapsed — the longest chrono chain is bounded by the elapsed periods e₂.time − e₁.time; ★ chronoDist_le_causalDist — and never exceeds the causal longest chain; chronoDist_add_le — the reverse triangle inequality survives; chronoDist_pos_iff.

What this is not

⚠️ CausalPrecedes is not redefined. It keeps its name, its theorems and its distance; the inflation theorems three_le_causalDist and two_mul_le_causalDist stand untouched, and this file says why they inflate: the steps they insert are strict causal steps with zero elapsed period, which strictChrono excludes (RecordLayer/ChainChrono.lean exhibits them).

⚠️ Chrono chain length is not clock time in general. The bound chronoDist ≤ elapsed periods is an inequality: a system may write several records in one period, and nothing here forces equality. Where equality holds — the site chain of the path graph, RecordLayer/ChainChrono.lean — it is a property of that witness.

⚠️ Everything is relative to the assumed coupling graph E, as in RecordCausalOrder.lean; no metric, no volume element, no continuum.

References: specs/BACKLOG.md #192, #188, #190, #111, #39; CV/RecordCausalOrder.lean (CausalPrecedes, isPartialOrder_causalPrecedes), CV/CausalDistance.lean (strictPrecedes, chainLengths, causalDist), RecordLayer/ChainClocks.lean (pairEvent, two_mul_le_causalDist).

The relation

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

Chronological precedence: causal precedence whose strict part demands a strictly later period.

Equations

• CSD.CV.ChronoPrecedes E e₁ e₂ = (CSD.CV.CausalPrecedes E e₁ e₂ ∧ (e₁ = e₂ ∨ e₁.time < e₂.time))

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

theorem CSD.CV.chronoPrecedes_refl {K : ℕ} (E : Finset (Fin K × Fin K)) (e : RecordEvent K) : ChronoPrecedes E e e

theorem CSD.CV.chronoPrecedes_of_causalPrecedes_of_lt {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : CausalPrecedes E e₁ e₂) (ht : e₁.time < e₂.time) : ChronoPrecedes E e₁ e₂

A causal step to a strictly later period is a chrono step.

theorem CSD.CV.chronoPrecedes_iff_of_time_ne {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (ht : e₁.time ≠ e₂.time) : ChronoPrecedes E e₁ e₂ ↔ CausalPrecedes E e₁ e₂

On events of distinct periods the two relations agree.

theorem CSD.CV.not_chronoPrecedes_of_time_eq {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (ht : e₁.time = e₂.time) (hne : e₁ ≠ e₂) : ¬ChronoPrecedes E e₁ e₂

★ Distinct simultaneous events are chrono-incomparable.

theorem CSD.CV.chronoPrecedes_trans {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ e₃ : RecordEvent K} (h₁ : ChronoPrecedes E e₁ e₂) (h₂ : ChronoPrecedes E e₂ e₃) : ChronoPrecedes E e₁ e₃

theorem CSD.CV.chronoPrecedes_antisymm {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h₁ : ChronoPrecedes E e₁ e₂) (h₂ : ChronoPrecedes E e₂ e₁) : e₁ = e₂

theorem CSD.CV.isPartialOrder_chronoPrecedes {K : ℕ} (E : Finset (Fin K × Fin K)) : IsPartialOrder (RecordEvent K) (ChronoPrecedes E)

★ Chronological precedence is a partial order on record events.

The strict part, as a relation chains run on

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

Strict chronological precedence: a chrono step to a different event.

Equations

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

theorem CSD.CV.mem_strictChrono {K : ℕ} {E : Finset (Fin K × Fin K)} {a b : RecordEvent K} : (a, b) ∈ strictChrono E ↔ ChronoPrecedes E a b ∧ a ≠ b

theorem CSD.CV.time_lt_of_strictChrono {K : ℕ} {E : Finset (Fin K × Fin K)} {a b : RecordEvent K} (h : (a, b) ∈ strictChrono E) : a.time < b.time

★ A strict chrono step moves to a strictly later period: no transition with unchanged occurrence time is a step.

theorem CSD.CV.strictChrono_of_causalPrecedes_of_lt {K : ℕ} {E : Finset (Fin K × Fin K)} {a b : RecordEvent K} (h : CausalPrecedes E a b) (ht : a.time < b.time) : (a, b) ∈ strictChrono E

theorem CSD.CV.strictChrono_le_strictPrecedes {K : ℕ} (E : Finset (Fin K × Fin K)) : strictChrono E ⊆ strictPrecedes E

Every chrono step is a causal step.

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

theorem CSD.CV.isIrrefl_strictChrono {K : ℕ} (E : Finset (Fin K × Fin K)) : (strictChrono E).IsIrrefl

A strict chrono step never returns: the relation is irreflexive, hence (with transitivity) acyclic.

Along a chrono chain the period strictly increases

theorem CSD.CV.time_add_le_of_chain {K : ℕ} {E : Finset (Fin K × Fin K)} (p : RelSeries (strictChrono E)) (i : Fin (p.length + 1)) : (p.toFun 0).time + ↑i ≤ (p.toFun i).time

The period at step i of a strict chrono chain is at least the head's period plus i.

theorem CSD.CV.time_add_length_le_of_chain {K : ℕ} {E : Finset (Fin K × Fin K)} (p : RelSeries (strictChrono E)) : p.head.time + p.length ≤ p.last.time

★ A strict chrono chain is acyclic and its length is at most the elapsed periods: the head's period plus the length is at most the last's period.

The chrono chain lengths and the chrono distance

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

The lengths of the strict chrono chains from e₁ to e₂.

Equations

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

theorem CSD.CV.chronoChainLengths_le_elapsed {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} {n : ℕ} (hn : n ∈ chronoChainLengths E e₁ e₂) : n ≤ e₂.time - e₁.time

★★ Every chrono chain is bounded by the elapsed periods.

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

A chrono chain is a causal chain of the same length.

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

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

The chrono distance: the length of the longest strict chrono chain, 0 when there is none.

Equations

• CSD.CV.chronoDist E e₁ e₂ = sSup (CSD.CV.chronoChainLengths E e₁ e₂)

theorem CSD.CV.chronoDist_le_elapsed {K : ℕ} (E : Finset (Fin K × Fin K)) (e₁ e₂ : RecordEvent K) : chronoDist E e₁ e₂ ≤ e₂.time - e₁.time

★★ The longest chrono chain is bounded by the elapsed periods.

theorem CSD.CV.chronoDist_le_causalDist {K : ℕ} (E : Finset (Fin K × Fin K)) (e₁ e₂ : RecordEvent K) : chronoDist E e₁ e₂ ≤ causalDist E e₁ e₂

★ The chrono distance never exceeds the causal distance.

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

theorem CSD.CV.one_mem_chronoChainLengths {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : (e₁, e₂) ∈ strictChrono E) : 1 ∈ chronoChainLengths E e₁ e₂

theorem CSD.CV.nonempty_chronoChainLengths_of_chronoPrecedes {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : ChronoPrecedes E e₁ e₂) : (chronoChainLengths E e₁ e₂).Nonempty

theorem CSD.CV.chronoDist_mem_chronoChainLengths {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : ChronoPrecedes E e₁ e₂) : chronoDist E e₁ e₂ ∈ chronoChainLengths E e₁ e₂

The longest chrono chain is attained.

theorem CSD.CV.chronoDist_eq_zero_of_not_chronoPrecedes {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ : RecordEvent K} (h : ¬ChronoPrecedes E e₁ e₂) : chronoDist E e₁ e₂ = 0

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

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

★ The chrono distance is positive exactly on the strictly chrono-related pairs.

theorem CSD.CV.chronoDist_add_le {K : ℕ} {E : Finset (Fin K × Fin K)} {e₁ e₂ e₃ : RecordEvent K} (h₁ : ChronoPrecedes E e₁ e₂) (h₂ : ChronoPrecedes E e₂ e₃) : chronoDist E e₁ e₂ + chronoDist E e₂ e₃ ≤ chronoDist E e₁ e₃

The reverse triangle inequality survives the restriction: chrono chains concatenate.