Two clocks: calibration consistency, and clock time against chain length

Category: 7-SigmaLayer (the record layer — the second clock of the clock-and-echo programme). BACKLOG #188 (out of #39; the sixth of #183–#189).

A second physical clock of the kind built in #185, on one arena with the first, with a product evolution. Three questions, each answered with its hypothesis visible:

1. Colocated clocks. Two clocks of periods T₁, T₂, each calibrated to its own period — the justified calibration, since abs_tickReading_sub_lt says each then reads t_Σ to within one of its ticks — agree to within T₁ + T₂ over the common horizon (★★ colocated_agreement). Under the hypothesis of equal rates T₁ = T₂ they agree exactly at every tick boundary (equal_rate_agreement_at_period). A clock whose unit is not its period drifts linearly from t_Σ (miscalibrated_drift): calibration is necessary, not decorative, and nothing here reports agreement as a dynamical fact.
2. A separated clock at the receiver. A clock at B, calibrated to the hop time and started at the switch-on together with A's — the synchronisation convention, stated as a hypothesis — reads, at the reception of the signal, exactly A's radar time of that exchange (★★ reception_reading_eq_radarTime). The transmission delay is one tick, and B is one edge from A (delay_eq_graph_separation): in this witness the clock delay equals the graph separation.
3. Clock time against the longest chain. The clock's elapsed time from emission to return is 2 ticks (elapsed_ticks_emission_return), and the experiment's own chain emission ≺ reception ≺ return has two steps, so causalDist ≥ 2 (two_le_causalDist). But causalDist is the longest chain over all record events, and inserting the event "both sites at period 1" between emission and reception lengthens the chain to three (★★ three_le_causalDist): the longest-chain separation exceeds the clock's elapsed time, and the two agree only at the fixed resolution of the experiment's three events. This is the distinction the row asked for, proved on the witness rather than asserted.

Honest scope

• ⚠️ Two sites only. For a longer chain of sites the relation between clock readings, per-edge delays and graph separation needs a sequentially activated coupling schedule that this corpus does not build; it is BACKLOG #190.
• The synchronisation of B's clock with A's is a hypothesis (common start at switch-on). It is the Einstein convention of this witness, not a derived fact; a different start shifts B's reading by the offset, as radarTime_shift says of A's.
• causalDist carries no resolution parameter; the "fixed resolution" statement is the pair of strict precedences of the experiment's three events, not a restricted distance.

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

Two clocks on one arena

@[reducible, inline]

abbrev CSD.RecordLayer.TwoClocks (K K' : ℕ) : Type

Two record clocks on one arena.

Equations

• CSD.RecordLayer.TwoClocks K K' = (CSD.RecordLayer.ClockArena K × CSD.RecordLayer.ClockArena K')

noncomputable def CSD.RecordLayer.twoClockEvolve {K K' : ℕ} (T₁ T₂ : ℝ) (s t : SigmaLayer.OnticTime) : TwoClocks K K' → TwoClocks K K'

The product evolution: each clock runs on its own period.

Equations

• CSD.RecordLayer.twoClockEvolve T₁ T₂ s t = Prod.map (CSD.RecordLayer.clockEvolve T₁ s t) (CSD.RecordLayer.clockEvolve T₂ s t)

theorem CSD.RecordLayer.twoClockEvolve_self {K K' : ℕ} (T₁ T₂ : ℝ) (t : SigmaLayer.OnticTime) : twoClockEvolve T₁ T₂ t t = id

theorem CSD.RecordLayer.twoClockEvolve_comp {K K' : ℕ} (T₁ T₂ : ℝ) (s t u : SigmaLayer.OnticTime) : twoClockEvolve T₁ T₂ t u ∘ twoClockEvolve T₁ T₂ s t = twoClockEvolve T₁ T₂ s u

theorem CSD.RecordLayer.measurable_twoClockEvolve {K K' : ℕ} (T₁ T₂ : ℝ) (s t : SigmaLayer.OnticTime) : Measurable (twoClockEvolve T₁ T₂ s t)

theorem CSD.RecordLayer.twoClockEvolve_measurePreserving {K K' : ℕ} (T₁ T₂ : ℝ) (s t : SigmaLayer.OnticTime) : MeasureTheory.MeasurePreserving (twoClockEvolve T₁ T₂ s t) MeasureTheory.volume MeasureTheory.volume

noncomputable def CSD.RecordLayer.reading₁ {K K' : ℕ} (T₁ T₂ τ₁ : ℝ) (x : TwoClocks K K') (t : SigmaLayer.OnticTime) : ℝ

The reading of the first clock, unit τ₁, at ontic time t.

Equations

• CSD.RecordLayer.reading₁ T₁ T₂ τ₁ x t = CSD.RecordLayer.tickReading τ₁ (CSD.RecordLayer.twoClockEvolve T₁ T₂ 0 t x).1

noncomputable def CSD.RecordLayer.reading₂ {K K' : ℕ} (T₁ T₂ τ₂ : ℝ) (x : TwoClocks K K') (t : SigmaLayer.OnticTime) : ℝ

The reading of the second clock, unit τ₂, at ontic time t.

Equations

• CSD.RecordLayer.reading₂ T₁ T₂ τ₂ x t = CSD.RecordLayer.tickReading τ₂ (CSD.RecordLayer.twoClockEvolve T₁ T₂ 0 t x).2

theorem CSD.RecordLayer.reading₁_eq {K K' : ℕ} (T₁ T₂ τ₁ : ℝ) (x : TwoClocks K K') (t : SigmaLayer.OnticTime) : reading₁ T₁ T₂ τ₁ x t = tickReading τ₁ (clockEvolve T₁ 0 t x.1)

theorem CSD.RecordLayer.reading₂_eq {K K' : ℕ} (T₁ T₂ τ₂ : ℝ) (x : TwoClocks K K') (t : SigmaLayer.OnticTime) : reading₂ T₁ T₂ τ₂ x t = tickReading τ₂ (clockEvolve T₂ 0 t x.2)

Colocated clocks

theorem CSD.RecordLayer.colocated_agreement {K K' : ℕ} (hK : 0 < K) (hK' : 0 < K') {T₁ T₂ : ℝ} (hT₁ : 0 < T₁) (hT₂ : 0 < T₂) {x : TwoClocks K K'} (hx₁ : x.1 ∈ ClockReady K) (hx₂ : x.2 ∈ ClockReady K') {t : SigmaLayer.OnticTime} (ht0 : 0 ≤ t) (ht₁ : t ≤ ↑K * T₁) (ht₂ : t ≤ ↑K' * T₂) : |reading₁ T₁ T₂ T₁ x t - reading₂ T₁ T₂ T₂ x t| < T₁ + T₂

★★ Colocated clocks, each calibrated to its own period, agree to within T₁ + T₂ over the common horizon. Both read t_Σ to within one of their own ticks; the bound is the sum.

theorem CSD.RecordLayer.equal_rate_agreement_at_period {K K' : ℕ} (hK : 0 < K) (hK' : 0 < K') {T : ℝ} (hT : 0 < T) (τ : ℝ) {x : TwoClocks K K'} (hx₁ : x.1 ∈ ClockReady K) (hx₂ : x.2 ∈ ClockReady K') {m : ℕ} (hm : m ≤ K) (hm' : m ≤ K') : reading₁ T T τ x (↑m * T) = reading₂ T T τ x (↑m * T)

Under the hypothesis of equal rates, two ready clocks agree exactly at every tick boundary within both horizons (with a common unit τ). The equality of rates is assumed, not derived.

theorem CSD.RecordLayer.miscalibrated_drift {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) (τ : ℝ) {c : ClockArena K} (hc : c ∈ ClockReady K) {m : ℕ} (hm : m ≤ K) : tickReading τ (clockEvolve T 0 (↑m * T) c) - ↑m * T = ↑m * (τ - T)

A miscalibrated clock drifts linearly: with unit τ instead of its period T, its reading at the m-th tick boundary differs from t_Σ by exactly m (τ − T).

A separated clock at the receiver

theorem CSD.RecordLayer.reception_reading_eq_radarTime {K K' : ℕ} {J ħ T τtick : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hK : 0 < K) (hT : 0 < T) (hTcal : T = CV.hopTime J ħ) (hτ : 0 ≤ τtick) {x : XArena K} (hx : x ∈ XReady K) (hK2 : 2 ≤ K) (hK' : 1 ≤ K') {cB : ClockArena K'} (hcB : cB ∈ ClockReady K') : tickReading τtick (clockEvolve T 0 (CV.hopTime J ħ) cB) = (cycleReadings hJ hħ hK hT hτ hx 0).radarTime

★★ A clock at B, calibrated to the hop time and started at the switch-on with A's, reads A's radar time of the exchange at the reception. The common start is the synchronisation convention, a hypothesis; the agreement is what it buys.

theorem CSD.RecordLayer.delay_eq_graph_separation : 1 ∉ CV.graphBall hopGraph {0} 0 ∧ 1 ∈ CV.graphBall hopGraph {0} 1

The transmission delay is one tick and B is one edge from A: B is outside the zero-period cone of A and inside its one-period cone. In this witness the clock delay of the signal equals the graph separation of the sites.

Clock time against the longest chain

theorem CSD.RecordLayer.elapsed_ticks_emission_return {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) : (eventOf J ħ T x (returnOcc J ħ b)).time - (eventOf J ħ T x (emission b)).time = 2

The clock's elapsed time from emission to return is two ticks.

theorem CSD.RecordLayer.emission_ne_reception : { region := {0}, time := 0 } ≠ { region := {1}, time := 1 }

theorem CSD.RecordLayer.reception_ne_return : { region := {1}, time := 1 } ≠ { region := {0}, time := 2 }

theorem CSD.RecordLayer.two_le_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) : 2 ≤ CV.causalDist hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (returnOcc J ħ b))

The experiment's own chain has two steps: causalDist ≥ 2, matching the clock.

def CSD.RecordLayer.bothSitesAtOne : CV.RecordEvent 2

The inserted event: both sites, at period 1.

Equations

• CSD.RecordLayer.bothSitesAtOne = { region := {0, 1}, time := 1 }

theorem CSD.RecordLayer.emission_precedes_bothSites : CV.CausalPrecedes hopGraph { region := {0}, time := 0 } bothSitesAtOne

theorem CSD.RecordLayer.bothSites_precedes_reception : CV.CausalPrecedes hopGraph bothSitesAtOne { region := {1}, time := 1 }

theorem CSD.RecordLayer.emission_ne_bothSites : { region := {0}, time := 0 } ≠ bothSitesAtOne

theorem CSD.RecordLayer.bothSites_ne_reception : bothSitesAtOne ≠ { region := {1}, time := 1 }

theorem CSD.RecordLayer.three_le_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) : 3 ≤ CV.causalDist hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (returnOcc J ħ b))

★★ Inserting an event lengthens the chain: through "both sites at period 1" the longest chain from emission to return has at least three steps, while the clock's elapsed time is two ticks. The longest-chain separation over all record events is not the clock time; they agree only at the fixed resolution of the experiment's three events.

theorem CSD.RecordLayer.elapsed_ticks_ne_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) : (eventOf J ħ T x (returnOcc J ħ b)).time - (eventOf J ħ T x (emission b)).time ≠ CV.causalDist hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (returnOcc J ħ b))

Clock time is not chain length: the elapsed ticks are 2, the longest chain is at least 3.

The package

theorem CSD.RecordLayer.clock_calibration {K K' : ℕ} (hK : 0 < K) (hK' : 0 < K') {T₁ T₂ : ℝ} (hT₁ : 0 < T₁) (hT₂ : 0 < T₂) {x : TwoClocks K K'} (hx₁ : x.1 ∈ ClockReady K) (hx₂ : x.2 ∈ ClockReady K') : (∀ (t : SigmaLayer.OnticTime), 0 ≤ t → t ≤ ↑K * T₁ → t ≤ ↑K' * T₂ → |reading₁ T₁ T₂ T₁ x t - reading₂ T₁ T₂ T₂ x t| < T₁ + T₂) ∧ (∀ (τ : ℝ), ∀ m ≤ K, tickReading τ (clockEvolve T₁ 0 (↑m * T₁) x.1) - ↑m * T₁ = ↑m * (τ - T₁)) ∧ 1 ∉ CV.graphBall hopGraph {0} 0 ∧ 1 ∈ CV.graphBall hopGraph {0} 1

★★ Calibration consistency. Colocated clocks calibrated to their own periods agree within T₁ + T₂; equal rates give exact agreement at tick boundaries; a miscalibrated clock drifts linearly; a synchronised clock at B reads A's radar time at reception; the clock delay is one tick and one edge; and the clock's elapsed time between emission and return is 2 while the longest chain is at least 3.