The chain and the exchange under chronological precedence: where the inflation comes from

Category: 7-SigmaLayer (the record layer — the witness half of #192). BACKLOG #192 (out of #39; the second of #191–#197).

CV/ChronoPrecedes.lean bounds the longest chrono chain by the elapsed periods. This file runs the two inflated witnesses of the programme through it and shows exactly which steps the inflation used.

• The chain of #190. ★ not_chronoPrecedes_pairEvent — the inserted step pairEvent k → siteEvent (k+1) of two_mul_le_causalDist is not a chrono step: both events sit at period k + 1. The site steps are (siteEvent_strictChrono_succ), so ★★ chronoDist_siteEvents — the chrono distance from the emission to the reception at site m is exactly m, the clock's elapsed ticks under T = τ_hop (#190), while ★ chronoDist_lt_causalDist — the causal distance is strictly larger for every m ≥ 1; two_mul_le_causalDist is untouched.
• The exchange of #186/#188. exchange_chrono_chain — emission ⪯ reception ⪯ return are chrono steps; ★ not_chronoPrecedes_bothSites_reception — the inserted bothSitesAtOne → reception step of three_le_causalDist is not; ★★ chronoDist_exchange = 2 — the chrono distance from emission to return is the two elapsed ticks (elapsed_ticks_emission_return), against three_le_causalDist.
• ★★★ chain_chrono — the package.

What this says and does not say

The longest-chain quantity causalDist counts strict steps of permitted influence, and a region inclusion at an unchanged period is such a step; so it measures the depth of the influence order, not time. The clock measures ticks of a calibrated register. On these two witnesses the chrono distance coincides with the clock, because each hop is one period and the schedule gives one hop per period; the general statement is the inequality chronoDist_le_elapsed, and the coincidence is the witness's. CausalPrecedes and both inflation theorems keep their names and their content.

References: specs/BACKLOG.md #192, #188, #190, #39; CV/ChronoPrecedes.lean, RecordLayer/ChainClocks.lean (siteEvent, pairEvent, two_mul_le_causalDist), RecordLayer/ClockCalibration.lean (bothSitesAtOne, three_le_causalDist).

The chain

theorem CSD.RecordLayer.siteEvent_time_lt_succ {n : ℕ} (k : Fin n) : (siteEvent k.castSucc).time < (siteEvent k.succ).time

theorem CSD.RecordLayer.siteEvent_chrono_succ {n : ℕ} (k : Fin n) : CV.ChronoPrecedes (CV.pathGraph n) (siteEvent k.castSucc) (siteEvent k.succ)

Consecutive site events are chrono-ordered.

theorem CSD.RecordLayer.siteEvent_strictChrono_succ {n : ℕ} (k : Fin n) : (siteEvent k.castSucc, siteEvent k.succ) ∈ CV.strictChrono (CV.pathGraph n)

A site step is a strict chrono step.

theorem CSD.RecordLayer.siteEvent_zero_chrono {n : ℕ} (j : Fin (n + 1)) : CV.ChronoPrecedes (CV.pathGraph n) (siteEvent 0) (siteEvent j)

The emission chrono-precedes every site event.

theorem CSD.RecordLayer.not_chronoPrecedes_pairEvent {n : ℕ} (k : Fin n) : ¬CV.ChronoPrecedes (CV.pathGraph n) (pairEvent k) (siteEvent k.succ)

★ The inserted step of the inflation is not a chrono step: pairEvent k and siteEvent (k+1) sit at the same period k + 1, so the region inclusion that two_mul_le_causalDist counts has no elapsed period.

theorem CSD.RecordLayer.le_chronoDist_siteEvents {n : ℕ} (m : ℕ) (hm : m ≤ n) : m ≤ CV.chronoDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)

The site chain gives chronoDist ≥ m.

theorem CSD.RecordLayer.chronoDist_siteEvents {n : ℕ} (m : ℕ) (hm : m ≤ n) : CV.chronoDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩) = m

★★ The chrono distance from the emission to the reception at site m is exactly m — the elapsed periods, which under T = τ_hop are the clock's elapsed ticks (#190).

theorem CSD.RecordLayer.chronoDist_lt_causalDist {n m : ℕ} (hm : m ≤ n) (hm1 : 1 ≤ m) : CV.chronoDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩) < CV.causalDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)

★ The causal distance is strictly larger than the chrono distance for every site m ≥ 1: the inflation of two_mul_le_causalDist is entirely in same-period steps.

The exchange

theorem CSD.RecordLayer.exchange_causal_steps : CV.CausalPrecedes hopGraph { region := {0}, time := 0 } { region := {1}, time := 1 } ∧ CV.CausalPrecedes hopGraph { region := {1}, time := 1 } { region := {0}, time := 2 }

The events of the exchange under the calibration T = τ_hop: emission, reception, return.

theorem CSD.RecordLayer.exchange_chrono_chain : CV.ChronoPrecedes hopGraph { region := {0}, time := 0 } { region := {1}, time := 1 } ∧ CV.ChronoPrecedes hopGraph { region := {1}, time := 1 } { region := {0}, time := 2 } ∧ CV.ChronoPrecedes hopGraph { region := {0}, time := 0 } { region := {0}, time := 2 }

The exchange's chain is a chrono chain: each step moves one period.

theorem CSD.RecordLayer.not_chronoPrecedes_bothSites_reception : ¬CV.ChronoPrecedes hopGraph bothSitesAtOne { region := {1}, time := 1 }

★ The inserted step of #188's inflation is not a chrono step: bothSitesAtOne and the reception both sit at period 1.

theorem CSD.RecordLayer.chronoDist_exchange : CV.chronoDist hopGraph { region := {0}, time := 0 } { region := {0}, time := 2 } = 2

★★ The chrono distance from emission to return is the two elapsed ticks, against three_le_causalDist.

theorem CSD.RecordLayer.chronoDist_exchange_lt_causalDist {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 2 ≤ K) {x : XArena K} (hx : x ∈ XReady K) (b : Fin 2) : CV.chronoDist hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (returnOcc J ħ b)) < CV.causalDist hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (returnOcc J ħ b))

The chrono distance of the exchange is strictly below its causal distance.

The package

theorem CSD.RecordLayer.chain_chrono {n K : ℕ} : (∀ (m : ℕ) (hm : m ≤ n), CV.chronoDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩) = m) ∧ (∀ (k : Fin n), ¬CV.ChronoPrecedes (CV.pathGraph n) (pairEvent k) (siteEvent k.succ)) ∧ (∀ (m : ℕ) (hm : m ≤ n), 1 ≤ m → CV.chronoDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩) < CV.causalDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)) ∧ CV.chronoDist hopGraph { region := {0}, time := 0 } { region := {0}, time := 2 } = 2 ∧ ¬CV.ChronoPrecedes hopGraph bothSitesAtOne { region := {1}, time := 1 } ∧ ∀ (E : Finset (Fin K × Fin K)) (e₁ e₂ : CV.RecordEvent K), CV.chronoDist E e₁ e₂ ≤ e₂.time - e₁.time ∧ CV.chronoDist E e₁ e₂ ≤ CV.causalDist E e₁ e₂

★★★ Where the inflation comes from. On the path graph the chrono distance from the emission to site m is exactly m and the inserted pair step is not a chrono step; on the exchange the chrono distance from emission to return is 2 and the inserted both-sites step is not a chrono step; in both cases the causal distance is strictly larger, and in general the chrono distance is bounded by the elapsed periods and by the causal distance.