Clocks along the chain: clock delay against graph distance, and chain length

Category: 7-SigmaLayer (the record layer — the network witness of the clock-and-echo programme). BACKLOG #190 (out of #39; the residue of #188).

The scheduled chain of CV/ChainExchange.lean carries one excitation from site 0 to site k in exactly k hop times. Here a physical record clock of #185 sits at every site, all started at the switch-on and all calibrated to the hop time — the synchronisation and calibration conventions of #186 and #188, stated as hypotheses — on one arena with the exchange, under one two-time measure-preserving evolution.

• ChainArena n K, chainEvolve J ħ T s t — the common arena and its two-time propagator: the scheduled exchange and the n + 1 clocks; chainEvolve_self, ★ chainEvolve_comp (the two-time law, from Schedule.evolve_comp and clockEvolve_comp), measurable_chainEvolve, ★ chainEvolve_measurePreserving — Liouville (Fubini–Study × Haar on every clock) is preserved: it is a dynamics;
• ChainReady, chainPrep b c — the ready preparation with message b; siteReading — the reading of site j's clock at ontic time t;
• ★★ reception_reading — the clock at site k reads k τ_hop when the signal arrives, i.e. tickCount_at_reception: k ticks; ★★★ clock_delay_eq_graphDist — and k is the graph distance from site 0 to site k on the path graph: on this witness, with this schedule, clock delay equals graph distance, for every site; ★★ reception_readout — at the same moment the receiver at k reads the message;
• eventOfReception, eventOfReception_eq — the reception at k as a RecordEvent labelled by the physical clock: ⟨{k}, k⟩ (siteEvent k); pairEvent k = ⟨{k, k+1}, k+1⟩; siteEvent_precedes_pairEvent, pairEvent_precedes_siteEvent, siteEvent_zero_precedes — the site events form a CausalPrecedes chain on the path graph;
• ★ le_causalDist_siteEvents — the experiment's own chain of site events gives causalDist ≥ k, matching the clock; ★★ two_mul_le_causalDist — inserting the event "both ends of edge j at period j+1" between consecutive site events doubles the chain: causalDist ≥ 2k; hence ★★ clock_time_lt_causalDist: for k ≥ 1 the clock's elapsed ticks k are strictly less than the longest-chain separation. This is #188's inflation (three_le_causalDist) for every k: the longest-chain distance over all record events is not clock time; they agree only at the fixed resolution of the site events;
• ★★★ chain_clocks — the package.

What this says about an effective cone

The clock delay equals the graph distance because every edge is switched on for the same hop time τ_hop = πħ/2J: the schedule gives the network one edge per τ_hop, and that is the only reason the two agree. A universal effective cone for this network would have to be exactly that — the same hop time on every edge, supplied by the schedule, not derived from the graph. Nothing here says the cone is universal, and nothing identifies 1 / τ_hop with a limiting speed; cf. the containment, never identification, of CV/TwoCones.lean.

Honest scope

• ⚠️ The schedule is a modelling input (the brief's own warning); a uniform chain Hamiltonian does not transfer exactly, and no claim is made about one.
• ⚠️ All clocks are started at the switch-on (0) and calibrated to τ_hop: the synchronisation convention and the calibration are hypotheses (hT : T = hopTime J ħ, the common start in chainEvolve), as in #186 and #188. A different start at site k shifts its reading by the offset.
• causalDist carries no resolution parameter; "the fixed resolution of the site events" is the chain le_causalDist_siteEvents exhibits, not a restricted distance.
• The clocks' horizon must cover the chain: n ≤ K.

References: specs/BACKLOG.md #190, #188, #186, #185, #39; CV/ChainExchange.lean, RecordLayer/RecordClock.lean, RecordLayer/ClockCalibration.lean, CV/CausalDistance.lean (causalDist, causalDist_add_le, causalDist_pos_iff), CV/TwoCones.lean.

The arena and its two-time propagator

@[reducible, inline]

abbrev CSD.RecordLayer.ChainArena (n K : ℕ) : Type

The common arena: the scheduled exchange on n + 1 sites and a record clock at every site.

Equations

• CSD.RecordLayer.ChainArena n K = (CSD.CV.FieldArena (n + 1) 2 × (Fin (n + 1) → CSD.RecordLayer.ClockArena K))

theorem CSD.RecordLayer.chainKick_eq_smul {n : ℕ} (U : ↥(Matrix.unitaryGroup (CV.ChainConfig (n + 1)) ℂ)) (p : CV.FieldArena (n + 1) 2) : CV.arenaKick U p = U • p

theorem CSD.RecordLayer.measurable_chainKick {n : ℕ} (U : ↥(Matrix.unitaryGroup (CV.ChainConfig (n + 1)) ℂ)) : Measurable (CV.arenaKick U)

theorem CSD.RecordLayer.chainKick_one {n : ℕ} (p : CV.FieldArena (n + 1) 2) : CV.arenaKick 1 p = p

noncomputable def CSD.RecordLayer.chainEvolve {n K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) : ChainArena n K → ChainArena n K

The joint two-time propagator: the scheduled exchange from s to t, and every clock on its own schedule, all started at the switch-on 0.

Equations

• CSD.RecordLayer.chainEvolve J ħ T s t x = (CSD.CV.arenaKick ((CSD.CV.chainSchedule n J ħ).evolve s t) x.1, fun (j : Fin (n + 1)) => CSD.RecordLayer.clockEvolve T s t (x.2 j))

theorem CSD.RecordLayer.chainEvolve_exchange {n K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (x : ChainArena n K) : (chainEvolve J ħ T s t x).1 = CV.arenaKick ((CV.chainSchedule n J ħ).evolve s t) x.1

theorem CSD.RecordLayer.chainEvolve_clock {n K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (x : ChainArena n K) (j : Fin (n + 1)) : (chainEvolve J ħ T s t x).2 j = clockEvolve T s t (x.2 j)

theorem CSD.RecordLayer.chainEvolve_self {n K : ℕ} (J ħ T : ℝ) (t : SigmaLayer.OnticTime) : chainEvolve J ħ T t t = id

theorem CSD.RecordLayer.chainEvolve_comp {n K : ℕ} (J ħ T : ℝ) (s t u : SigmaLayer.OnticTime) : chainEvolve J ħ T t u ∘ chainEvolve J ħ T s t = chainEvolve J ħ T s u

★ The two-time composition law on the common arena.

theorem CSD.RecordLayer.measurable_chainEvolve {n K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) : Measurable (chainEvolve J ħ T s t)

theorem CSD.RecordLayer.chainEvolve_measurePreserving {n K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena (n + 1) 2) : MeasureTheory.MeasurePreserving (chainEvolve J ħ T s t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)

★ The joint propagator preserves Liouville measure — Fubini–Study on the exchange, Haar on every clock — for every reference point of the Fubini–Study measure: it is a dynamics.

Readiness, preparation, readings

def CSD.RecordLayer.ChainReady (n K : ℕ) : Set (ChainArena n K)

Every clock ready.

Equations

• CSD.RecordLayer.ChainReady n K = {x : CSD.RecordLayer.ChainArena n K | ∀ (j : Fin (n + 1)), x.2 j ∈ CSD.RecordLayer.ClockReady K}

noncomputable def CSD.RecordLayer.chainPrep {n K : ℕ} (b : Fin 2) (c : Fin (n + 1) → ClockArena K) : ChainArena n K

The ready preparation with message b: the message point and the clocks c.

Equations

• CSD.RecordLayer.chainPrep b c = (CSD.CV.chainMsg n b, c)

theorem CSD.RecordLayer.chainPrep_mem_ready {n K : ℕ} {c : Fin (n + 1) → ClockArena K} (hc : ∀ (j : Fin (n + 1)), c j ∈ ClockReady K) (b : Fin 2) : chainPrep b c ∈ ChainReady n K

noncomputable def CSD.RecordLayer.siteReading {n K : ℕ} (J ħ T τ : ℝ) (x : ChainArena n K) (j : Fin (n + 1)) (t : SigmaLayer.OnticTime) : ℝ

The reading of site j's clock, unit τ, at ontic time t from the switch-on.

Equations

• CSD.RecordLayer.siteReading J ħ T τ x j t = CSD.RecordLayer.tickReading τ ((CSD.RecordLayer.chainEvolve J ħ T 0 t x).2 j)

theorem CSD.RecordLayer.siteReading_eq {n K : ℕ} (J ħ T τ : ℝ) (x : ChainArena n K) (j : Fin (n + 1)) (t : SigmaLayer.OnticTime) : siteReading J ħ T τ x j t = tickReading τ (clockEvolve T 0 t (x.2 j))

theorem CSD.RecordLayer.chainEvolve_exchange_zero {n K : ℕ} (J ħ T : ℝ) (t : SigmaLayer.OnticTime) (x : ChainArena n K) : (chainEvolve J ħ T 0 t x).1 = CV.chainArenaFlow J ħ t x.1

From the switch-on, the exchange factor is the scheduled arena flow.

Clock delay against graph distance

theorem CSD.RecordLayer.tickCount_at_reception {n K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) (hnK : n ≤ K) {x : ChainArena n K} (hx : x ∈ ChainReady n K) (k : Fin (n + 1)) : tickCount ((chainEvolve J ħ T 0 (↑↑k * CV.hopTime J ħ) x).2 k) = ↑k

The clock at site k shows k ticks when the signal arrives.

theorem CSD.RecordLayer.reception_reading {n K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) (hnK : n ≤ K) {x : ChainArena n K} (hx : x ∈ ChainReady n K) (k : Fin (n + 1)) : siteReading J ħ T T x k (↑↑k * CV.hopTime J ħ) = ↑↑k * CV.hopTime J ħ

★★ The clock at site k, calibrated to the hop time, reads k τ_hop when the signal arrives — the transmission delay in the clock's own units.

theorem CSD.RecordLayer.clock_delay_eq_graphDist {n K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) (hnK : n ≤ K) {x : ChainArena n K} (hx : x ∈ ChainReady n K) (k : Fin (n + 1)) : tickCount ((chainEvolve J ħ T 0 (↑↑k * CV.hopTime J ħ) x).2 k) = CV.graphDist (CV.pathGraph n) {0} k

★★★ Clock delay equals graph distance on this witness: the ticks shown at site k when the signal arrives are the graph distance from site 0 to site k on the path graph.

theorem CSD.RecordLayer.reception_readout {n K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (c : Fin (n + 1) → ClockArena K) (k : Fin (n + 1)) : CV.arenaObs (CV.occAt k) (chainEvolve J ħ T 0 (↑↑k * CV.hopTime J ħ) (chainPrep 1 c)).1 = 1 ∧ CV.arenaObs (CV.occAt k) (chainEvolve J ħ T 0 (↑↑k * CV.hopTime J ħ) (chainPrep 0 c)).1 = 0

★★ At the same moment the receiver at k reads the message: 1 for message 1, 0 for message 0.

The reception as a record event labelled by the clock

noncomputable def CSD.RecordLayer.eventOfReception {n K : ℕ} (J ħ T : ℝ) (x : ChainArena n K) (k : Fin (n + 1)) : CV.RecordEvent (n + 1)

The reception at site k, as a record event: the site, at the period its own clock shows.

Equations

• CSD.RecordLayer.eventOfReception J ħ T x k = { region := {k}, time := CSD.RecordLayer.tickCount ((CSD.RecordLayer.chainEvolve J ħ T 0 (↑↑k * CSD.CV.hopTime J ħ) x).2 k) }

def CSD.RecordLayer.siteEvent {n : ℕ} (k : Fin (n + 1)) : CV.RecordEvent (n + 1)

The site event ⟨{k}, k⟩.

Equations

• CSD.RecordLayer.siteEvent k = { region := {k}, time := ↑k }

def CSD.RecordLayer.pairEvent {n : ℕ} (k : Fin n) : CV.RecordEvent (n + 1)

The inserted event: both ends of edge (k, k+1), at period k + 1.

Equations

• CSD.RecordLayer.pairEvent k = { region := {k.castSucc, k.succ}, time := ↑k + 1 }

theorem CSD.RecordLayer.eventOfReception_eq {n K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) (hnK : n ≤ K) {x : ChainArena n K} (hx : x ∈ ChainReady n K) (k : Fin (n + 1)) : eventOfReception J ħ T x k = siteEvent k

The reception at k is the site event ⟨{k}, k⟩, under the stated calibration.

theorem CSD.RecordLayer.mem_graphBall_of_mem {n : ℕ} {E : Finset (Fin (n + 1) × Fin (n + 1))} {R : Finset (Fin (n + 1))} {k : Fin (n + 1)} (hk : k ∈ R) (d : ℕ) : k ∈ CV.graphBall E R d

theorem CSD.RecordLayer.succ_mem_graphBall_one {n : ℕ} (k : Fin n) : k.succ ∈ CV.graphBall (CV.pathGraph n) {k.castSucc} 1

theorem CSD.RecordLayer.siteEvent_precedes_pairEvent {n : ℕ} (k : Fin n) : CV.CausalPrecedes (CV.pathGraph n) (siteEvent k.castSucc) (pairEvent k)

theorem CSD.RecordLayer.pairEvent_precedes_siteEvent {n : ℕ} (k : Fin n) : CV.CausalPrecedes (CV.pathGraph n) (pairEvent k) (siteEvent k.succ)

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

Consecutive site events are causally ordered.

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

The emission precedes every reception.

theorem CSD.RecordLayer.siteEvent_ne_pairEvent {n : ℕ} (k : Fin n) : siteEvent k.castSucc ≠ pairEvent k

theorem CSD.RecordLayer.pairEvent_ne_siteEvent {n : ℕ} (k : Fin n) : pairEvent k ≠ siteEvent k.succ

theorem CSD.RecordLayer.siteEvent_ne_succ {n : ℕ} (k : Fin n) : siteEvent k.castSucc ≠ siteEvent k.succ

theorem CSD.RecordLayer.two_le_causalDist_step {n : ℕ} (k : Fin n) : 2 ≤ CV.causalDist (CV.pathGraph n) (siteEvent k.castSucc) (siteEvent k.succ)

One edge of the chain already has two strict steps through the inserted event.

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

★ The experiment's own chain of site events gives causalDist ≥ k, matching the clock.

theorem CSD.RecordLayer.two_mul_le_causalDist {n : ℕ} (m : ℕ) (hm : m ≤ n) : 2 * m ≤ CV.causalDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)

★★ Inserting events doubles the chain: through the pair events the longest chain from the emission to the reception at site m has at least 2m steps, while the clock shows m ticks.

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

★★ Clock time is not chain length: for every site m ≥ 1 the clock's elapsed ticks m are strictly less than the longest-chain separation from the emission.

The package

theorem CSD.RecordLayer.chain_clocks {n K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) (hnK : n ≤ K) {c : Fin (n + 1) → ClockArena K} (hc : ∀ (j : Fin (n + 1)), c j ∈ ClockReady K) : (∀ (s t u : SigmaLayer.OnticTime), chainEvolve J ħ T t u ∘ chainEvolve J ħ T s t = chainEvolve J ħ T s u) ∧ (∀ (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena (n + 1) 2), MeasureTheory.MeasurePreserving (chainEvolve J ħ T s t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)) ∧ (∀ (b : Fin 2) (k : Fin (n + 1)), tickCount ((chainEvolve J ħ T 0 (↑↑k * CV.hopTime J ħ) (chainPrep b c)).2 k) = CV.graphDist (CV.pathGraph n) {0} k) ∧ (∀ (k : Fin (n + 1)), CV.arenaObs (CV.occAt k) (chainEvolve J ħ T 0 (↑↑k * CV.hopTime J ħ) (chainPrep 1 c)).1 = 1 ∧ CV.arenaObs (CV.occAt k) (chainEvolve J ħ T 0 (↑↑k * CV.hopTime J ħ) (chainPrep 0 c)).1 = 0) ∧ (∀ (b : Fin 2) (k : Fin (n + 1)), eventOfReception J ħ T (chainPrep b c) k = siteEvent k) ∧ ∀ (m : ℕ) (hm : m ≤ n), m ≤ CV.causalDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩) ∧ 2 * m ≤ CV.causalDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)

★★★ Clocks along the chain. One two-time measure-preserving dynamics carries the scheduled exchange and a clock at every site; for every ready preparation the clock at site k shows k ticks when the signal arrives, which is the graph distance from site 0 to site k; the receiver at k reads the message at that moment; the reception is the record event ⟨{k}, k⟩; the site events alone give causalDist ≥ k, the inserted events give ≥ 2k, so clock time is below the longest chain for every k ≥ 1.