Operational duration: what a calibrated clock measures, against what the longest chain counts

Category: 7-SigmaLayer (the record layer — the duration half of the author's second brief). BACKLOG #193 (out of #39; the third of #191–#197).

A duration is the difference of two readings of one physical clock history. This file defines it from the record clock of #185 and proves the properties the brief asks for, naming each for what it is.

• clockHistory T τ c t — the calibrated reading of clock c, run from the switch-on, at t; duration T τ c s t — the operational duration from s to t along that history;
• ★ duration_nonneg — non-negative for chronologically ordered readings (tickCount_mono);
• duration_add — additivity on consecutive intervals is the telescoping identity: an algebraic consistency of one history with itself, not a derivation of proper time; duration_self, duration_neg;
• tickCount_clockEvolve_of_nonpos, offsetHistory, ★ duration_offset — clock-origin invariance twice over: a switch-on reference anywhere before 0 gives the same readings, and a constant offset on every reading leaves every duration unchanged;
• ★ duration_rescale — the unit rescaling τ ↦ λ τ scales every duration by λ;
• ★★ abs_duration_sub_lt — the resolution bound: calibrated with the period, a duration is within two ticks of the elapsed ontic parameter over the horizon (abs_tickReading_sub_lt twice);
• duration_eq_zero_of_writeEnd_eq — two descriptions of one write (occurrences with the same completion time, #191) are at zero duration from one another;
• edgeDuration_nonneg, ★ sum_edgeDuration — along an occurrence chain the edge durations read off one clock are non-negative and sum to the end-to-end duration (telescoping again, and named so);
• the chain witness (#190, #192): ★★ duration_reception — the clock at site m measures m τ_hop from the switch-on to the reception; ★★★ duration_eq_chronoDist_mul — that duration is the chrono distance times the tick, while two_mul_le_causalDist keeps the causal longest chain at ≥ 2m;
• ★★★ operational_duration — the package.

The deliverable, in words

causalDist e₁ e₂ is the length of the longest chain of strict steps of permitted influence on the assumed coupling graph. A region inclusion at an unchanged period is such a step, so the quantity measures the depth of the influence order and may exceed the elapsed periods without bound in the number of regions (#188, #190). chronoDist keeps only the steps that advance the period and is bounded by the elapsed periods (#192). A clock duration is the difference of two tick counts of one calibrated register, times the tick. On the chain witness, with calibration T = τ_hop and every edge on for one period, the duration from the switch-on to the reception at site m equals m ticks and equals the chrono distance; the causal longest chain is at least 2m. The calibration and the resolution of the events are hypotheses: a different T changes the tick count, and several records may be written per tick. Nothing here is a proper time, a metric, or a universal speed.

References: specs/BACKLOG.md #193, #185, #188, #190, #191, #192, #39; RecordLayer/RecordClock.lean (tickReading, tickCount_mono, abs_tickReading_sub_lt), RecordLayer/ChainClocks.lean, RecordLayer/ChainChrono.lean (chronoDist_siteEvents), RecordLayer/RecordOccurrence.lean, CV/RadarCoordinates.lean (rescale, shift).

The clock history and its durations

noncomputable def CSD.RecordLayer.clockHistory {K : ℕ} (T τ : ℝ) (c : ClockArena K) (t : ℝ) : ℝ

The clock history: the calibrated reading of clock c, run from the switch-on, at t.

Equations

• CSD.RecordLayer.clockHistory T τ c t = CSD.RecordLayer.tickReading τ (CSD.RecordLayer.clockEvolve T 0 t c)

theorem CSD.RecordLayer.clockHistory_eq {K : ℕ} (T τ : ℝ) (c : ClockArena K) (t : ℝ) : clockHistory T τ c t = ↑(tickCount (clockEvolve T 0 t c)) * τ

noncomputable def CSD.RecordLayer.duration {K : ℕ} (T τ : ℝ) (c : ClockArena K) (s t : ℝ) : ℝ

Operational duration from s to t: the difference of the two readings of one history.

Equations

• CSD.RecordLayer.duration T τ c s t = CSD.RecordLayer.clockHistory T τ c t - CSD.RecordLayer.clockHistory T τ c s

theorem CSD.RecordLayer.duration_self {K : ℕ} (T τ : ℝ) (c : ClockArena K) (t : ℝ) : duration T τ c t t = 0

theorem CSD.RecordLayer.duration_neg {K : ℕ} (T τ : ℝ) (c : ClockArena K) (s t : ℝ) : duration T τ c t s = -duration T τ c s t

theorem CSD.RecordLayer.duration_nonneg {K : ℕ} (hK : 0 < K) {T τ : ℝ} (hT : 0 < T) (hτ : 0 ≤ τ) {c : ClockArena K} (hc : c ∈ ClockReady K) {s t : ℝ} (hst : s ≤ t) : 0 ≤ duration T τ c s t

★ Non-negativity for chronologically ordered readings: the tick count is monotone.

theorem CSD.RecordLayer.duration_add {K : ℕ} (T τ : ℝ) (c : ClockArena K) (s t u : ℝ) : duration T τ c s t + duration T τ c t u = duration T τ c s u

Additivity on consecutive intervals is the telescoping identity — an algebraic consistency of one history with itself, not a derivation of proper time.

Clock-origin invariance

theorem CSD.RecordLayer.tickCount_clockEvolve_of_nonpos {K : ℕ} {T : ℝ} (hT : 0 < T) {s : ℝ} (hs : s ≤ 0) (t : SigmaLayer.OnticTime) (c : ClockArena K) : tickCount (clockEvolve T s t c) = tickCount (clockEvolve T 0 t c)

A switch-on reference anywhere before 0 gives the readings of the clock run from 0 (the general form of tickCount_clock_neg_one).

noncomputable def CSD.RecordLayer.offsetHistory {K : ℕ} (T τ : ℝ) (c : ClockArena K) (a t : ℝ) : ℝ

The history with a constant offset a on every reading: another zero of the same clock.

Equations

• CSD.RecordLayer.offsetHistory T τ c a t = CSD.RecordLayer.clockHistory T τ c t + a

theorem CSD.RecordLayer.duration_offset {K : ℕ} (T τ : ℝ) (c : ClockArena K) (a s t : ℝ) : offsetHistory T τ c a t - offsetHistory T τ c a s = duration T τ c s t

★ Clock-origin invariance: a constant offset on every reading leaves every duration unchanged.

Unit rescaling and resolution

theorem CSD.RecordLayer.duration_rescale {K : ℕ} (T τ lam : ℝ) (c : ClockArena K) (s t : ℝ) : duration T (lam * τ) c s t = lam * duration T τ c s t

★ Unit rescaling: measuring in the unit λ τ scales every duration by λ.

theorem CSD.RecordLayer.abs_duration_sub_lt {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {c : ClockArena K} (hc : c ∈ ClockReady K) {s t : ℝ} (hs0 : 0 ≤ s) (hsK : s ≤ ↑K * T) (ht0 : 0 ≤ t) (htK : t ≤ ↑K * T) : |duration T T c s t - (t - s)| < 2 * T

★★ The resolution bound: calibrated with the period, a duration is within two ticks of the elapsed ontic parameter, for readings inside the horizon.

Duplicate descriptions and occurrence chains

theorem CSD.RecordLayer.duration_eq_zero_of_writeEnd_eq {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] {L : ℕ} (o₁ o₂ : ActualOccurrence X Ω L) (h : o₁.writeEnd = o₂.writeEnd) (T τ : ℝ) (c : ClockArena K) : duration T τ c o₁.writeEnd o₂.writeEnd = 0

Two descriptions of one write are at zero duration: occurrences completing at the same time (#191) have no duration between them, on any clock.

theorem CSD.RecordLayer.edgeDuration_nonneg {K : ℕ} (hK : 0 < K) {T τ : ℝ} (hT : 0 < T) (hτ : 0 ≤ τ) {c : ClockArena K} (hc : c ∈ ClockReady K) {ts : ℕ → ℝ} (hts : Monotone ts) (i : ℕ) : 0 ≤ duration T τ c (ts i) (ts (i + 1))

Along an occurrence chain with non-decreasing completion times, every edge duration is non-negative.

theorem CSD.RecordLayer.sum_edgeDuration {K : ℕ} (T τ : ℝ) (c : ClockArena K) (ts : ℕ → ℝ) (m : ℕ) : ∑ i ∈ Finset.range m, duration T τ c (ts i) (ts (i + 1)) = duration T τ c (ts 0) (ts m)

★ The edge durations of an occurrence chain sum to the end-to-end duration — telescoping, named as such.

The chain witness: duration against chrono and causal distance

theorem CSD.RecordLayer.duration_reception {K n : ℕ} {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) (m : ℕ) (hm : m ≤ n) : duration T T (c ⟨m, ⋯⟩) 0 (↑m * CV.hopTime J ħ) = ↑m * T

★★ The clock at site m measures m ticks from the switch-on to the reception.

theorem CSD.RecordLayer.duration_eq_chronoDist_mul {K n : ℕ} {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) (m : ℕ) (hm : m ≤ n) : duration T T (c ⟨m, ⋯⟩) 0 (↑m * CV.hopTime J ħ) = ↑(CV.chronoDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)) * T ∧ 2 * m ≤ CV.causalDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)

★★★ Clock duration is the chrono distance times the tick on the chain witness, while the causal longest chain is at least twice the tick count.

The package

theorem CSD.RecordLayer.operational_duration {K n : ℕ} {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) : (∀ (j : Fin (n + 1)) (τ : ℝ), 0 ≤ τ → ∀ (s t : ℝ), s ≤ t → 0 ≤ duration T τ (c j) s t) ∧ (∀ (j : Fin (n + 1)) (τ s t u : ℝ), duration T τ (c j) s t + duration T τ (c j) t u = duration T τ (c j) s u) ∧ (∀ (j : Fin (n + 1)) (τ a s t : ℝ), offsetHistory T τ (c j) a t - offsetHistory T τ (c j) a s = duration T τ (c j) s t) ∧ (∀ (j : Fin (n + 1)) (τ lam s t : ℝ), duration T (lam * τ) (c j) s t = lam * duration T τ (c j) s t) ∧ (∀ (j : Fin (n + 1)) (s t : ℝ), 0 ≤ s → s ≤ ↑K * T → 0 ≤ t → t ≤ ↑K * T → |duration T T (c j) s t - (t - s)| < 2 * T) ∧ ∀ (m : ℕ) (hm : m ≤ n), duration T T (c ⟨m, ⋯⟩) 0 (↑m * CV.hopTime J ħ) = ↑(CV.chronoDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)) * T ∧ 2 * m ≤ CV.causalDist (CV.pathGraph n) (siteEvent 0) (siteEvent ⟨m, ⋯⟩)

★★★ Operational duration. Non-negative for ordered readings; additive (telescoping); invariant under a constant offset of the readings; scaling under unit rescaling; within two ticks of the elapsed ontic parameter when calibrated with the period; zero between two descriptions of one write; and on the chain witness the clock at site m measures m ticks, equal to the chrono distance, while the causal longest chain is at least 2m.