The record clock: a periodic register plus fresh slots, read as a tick count

Category: 7-SigmaLayer (the record layer — the first physical clock in the corpus). BACKLOG #185 (out of #39; the third of #183–#189).

A periodic subsystem does not count its cycles: after one period it is back where it was (osc_period). A clock is a periodic register together with fresh record slots, one written per cycle, and its reading is the number of written slots. This file builds that clock on one arena, with the record machinery of ShearWitness.lean (the arcs, pshift, rep) and presents each slot as a MeasurementProtocol, so that the corpus's own persistence theorem applies to every tick.

The arena. ClockArena K = KTorus × (Fin K → KTorus): the oscillator register and K slot registers, each a copy of the pointer torus. K is the observation horizon: the apparatus memory, one slot per tick.

The dynamics. clockEvolve T s t: the oscillator turns at rate 1/T; slot n is translated by the gap δ = shearGap K during its own window [n T, (n+1) T] (winElapsed), from the ready arc (0, ε] into the written arc (δ, δ + ε], and is frozen outside its window. It is a two-time propagator (clockEvolve_self, clockEvolve_comp), measurable, and preserves Liouville measure on the arena (clockEvolve_measurePreserving). ⚠️ The window schedule is a modelling input indexed by ontic time t_Σ, stated as such: it is the switching of the slot couplings, exactly as elapsed is the switching of the shear coupling in ShearWitness.lean. It is not emergent time, and this file does not call it that.

The readout. tickCount x is the number of slots in the written arc; tickReading τ_tick x = tickCount x · τ_tick is the calibrated reading, with the physical count and the unit τ_tick > 0 kept apart.

• ClockArena, winElapsed, clockEvolve; clockEvolve_self, ★ clockEvolve_comp, measurable_clockEvolve, ★ clockEvolve_measurePreserving — a dynamics;
• osc_period — the oscillator alone cannot count: its state after one period is its state;
• writtenArc, writtenArc_eq_pointerArc_zero, readyArc_disjoint_writtenArc;
• ★ slot_ready_before, ★ slot_written_after, ★ slot_written_mono — a concrete evolution writes tick n from the ready preparation, during window n, once and for all;
• tickCount, ★ measurable_tickCount — the readout is well defined and measurable; tickCount_le_horizon;
• ★★ tickCount_mono — the tick count is nondecreasing;
• ★★ tickCount_ge, tickCount_le, tickCount_at_period — the relation between tick count and the evolution parameter: after n + 1 full periods at least n + 1 ticks, before n periods at most n, and exactly m at time m T;
• ★ successive_ticks_distinguishable — successive ticks occupy distinct register states;
• tickProtocol n — each slot is a MeasurementProtocol, with tickProtocol_pointerInvariant and ★ tick_persists — tick n persists through the window, by the corpus's record_persists_on_interval, not by a fresh argument;
• tickReading, ★★ abs_tickReading_sub_lt — calibrated with τ_tick = T, the clock reads within one tick of t_Σ over the horizon; ★★★ record_clock — the package.

Honest scope

• ⚠️ The writes are scheduled, not triggered by the oscillator's phase: slot n moves during the n-th period because the schedule says so, and the oscillator's role is to define the period. A counter whose next slot is armed by the previous slot's record (a ripple counter) would make the trigger dynamical; it is not built here.
• During its window a slot is in transit and may or may not read as written; the theorems about the count are stated at the window boundaries (tickCount_ge, tickCount_le) and the count is monotone throughout (tickCount_mono). Within one tick of t_Σ is the honest resolution.
• The Hamiltonian generation of clockEvolve is not formalised, exactly as for shearEvolve and swapEvolve (R-016′); the propagator is given and shown to be a measure-preserving two-time dynamics.
• K ≥ 1 is needed wherever a slot is written (gap_add_width_le_one); with K = 0 there is no memory and nothing is claimed.

References: specs/BACKLOG.md #185, #183, #186, #39; RecordLayer/ShearWitness.lean (pshift, readyArc, pointerArc, shearGap, shearWidth, rep_pshift_of_mem, measurePreserving_pshift); RecordLayer/SwapWitness.lean (the slot bank); RecordLayer/MeasurementProtocol.lean; RecordLayer/RecordPersistence.lean (record_persists_on_interval).

The arena and the window schedule

@[reducible, inline]

abbrev CSD.RecordLayer.ClockArena (K : ℕ) : Type

The clock arena: the oscillator register and K slot registers. K is the horizon.

Equations

• CSD.RecordLayer.ClockArena K = (CSD.LF4.KTorus × (Fin K → CSD.LF4.KTorus))

noncomputable def CSD.RecordLayer.winElapsed (T : ℝ) (n : ℕ) (u : ℝ) : ℝ

The fraction of slot n's window [n T, (n+1) T] elapsed by time u.

Equations

• CSD.RecordLayer.winElapsed T n u = max 0 (min ((u - ↑n * T) / T) 1)

theorem CSD.RecordLayer.winElapsed_nonneg (T : ℝ) (n : ℕ) (u : ℝ) : 0 ≤ winElapsed T n u

theorem CSD.RecordLayer.winElapsed_le_one (T : ℝ) (n : ℕ) (u : ℝ) : winElapsed T n u ≤ 1

theorem CSD.RecordLayer.winElapsed_of_le {T : ℝ} (hT : 0 < T) {n : ℕ} {u : ℝ} (hu : u ≤ ↑n * T) : winElapsed T n u = 0

theorem CSD.RecordLayer.winElapsed_of_ge {T : ℝ} (hT : 0 < T) {n : ℕ} {u : ℝ} (hu : (↑n + 1) * T ≤ u) : winElapsed T n u = 1

theorem CSD.RecordLayer.winElapsed_mono {T : ℝ} (hT : 0 < T) (n : ℕ) {s t : ℝ} (hst : s ≤ t) : winElapsed T n s ≤ winElapsed T n t

The propagator

noncomputable def CSD.RecordLayer.clockEvolve {K : ℕ} (T : ℝ) (s t : SigmaLayer.OnticTime) : ClockArena K → ClockArena K

The clock propagator over [s, t]: the oscillator turns by (t − s)/T; slot n is translated by the gap δ times the fraction of its window that elapsed.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.RecordLayer.clockEvolve_osc {K : ℕ} (T : ℝ) (s t : SigmaLayer.OnticTime) (x : ClockArena K) : (clockEvolve T s t x).1 = pshift ((t - s) / T) x.1

theorem CSD.RecordLayer.clockEvolve_slot {K : ℕ} (T : ℝ) (s t : SigmaLayer.OnticTime) (x : ClockArena K) (n : Fin K) : (clockEvolve T s t x).2 n = pshift ((winElapsed T (↑n) t - winElapsed T (↑n) s) * shearGap K) (x.2 n)

theorem CSD.RecordLayer.clockEvolve_self {K : ℕ} (T : ℝ) (t : SigmaLayer.OnticTime) : clockEvolve T t t = id

theorem CSD.RecordLayer.clockEvolve_comp {K : ℕ} (T : ℝ) (s t u : SigmaLayer.OnticTime) : clockEvolve T t u ∘ clockEvolve T s t = clockEvolve T s u

★ The two-time composition law.

theorem CSD.RecordLayer.measurable_pshift (a : ℝ) : Measurable (pshift a)

theorem CSD.RecordLayer.measurable_clockEvolve {K : ℕ} (T : ℝ) (s t : SigmaLayer.OnticTime) : Measurable (clockEvolve T s t)

theorem CSD.RecordLayer.clockEvolve_measurePreserving {K : ℕ} (T : ℝ) (s t : SigmaLayer.OnticTime) : MeasureTheory.MeasurePreserving (clockEvolve T s t) MeasureTheory.volume MeasureTheory.volume

★ The clock propagator preserves Liouville measure on the arena: it is a dynamics.

The oscillator alone cannot count

theorem CSD.RecordLayer.osc_period {T : ℝ} (hT : 0 < T) (t : ℝ) (q : LF4.KTorus) : pshift ((t + T) / T) q = pshift (t / T) q

After one period the oscillator is back where it was: a periodic subsystem does not count its cycles. This is why the slots are there.

The written arc

noncomputable def CSD.RecordLayer.writtenArc (K : ℕ) : Set LF4.KTorus

The arc a slot occupies once its tick is written: rep ∈ (δ, δ + ε].

Equations

• CSD.RecordLayer.writtenArc K = {x : CSD.LF4.KTorus | CSD.RecordLayer.rep x.1 ∈ Set.Ioc (CSD.RecordLayer.shearGap K) (CSD.RecordLayer.shearGap K + CSD.RecordLayer.shearWidth K)}

theorem CSD.RecordLayer.measurableSet_writtenArc {K : ℕ} : MeasurableSet (writtenArc K)

theorem CSD.RecordLayer.writtenArc_eq_pointerArc_zero {K : ℕ} (hK : 0 < K) : writtenArc K = pointerArc K ⟨0, hK⟩

The written arc is the pointer arc of the first outcome.

theorem CSD.RecordLayer.readyArc_disjoint_writtenArc {K : ℕ} : Disjoint (readyArc K) (writtenArc K)

theorem CSD.RecordLayer.gap_add_width_le_one {K : ℕ} (hK : 0 < K) : shearGap K + shearWidth K ≤ 1

Writing one slot

theorem CSD.RecordLayer.rep_pshift_ready {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ readyArc K) {f : ℝ} (hf0 : 0 ≤ f) (hf1 : f ≤ 1) : rep (pshift (f * shearGap K) q).1 = rep q.1 + f * shearGap K

A ready slot shifted by a fraction f ∈ [0, 1] of the gap does not wrap: rep is additive.

theorem CSD.RecordLayer.written_of_ready {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ readyArc K) : pshift (1 * shearGap K) q ∈ writtenArc K

★ A ready slot shifted by the full gap is written.

theorem CSD.RecordLayer.written_mono {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ readyArc K) {f g : ℝ} (hf0 : 0 ≤ f) (hfg : f ≤ g) (hg1 : g ≤ 1) (hw : pshift (f * shearGap K) q ∈ writtenArc K) : pshift (g * shearGap K) q ∈ writtenArc K

★ Once a ready slot reads as written, it reads as written at every later fraction: the write is monotone through the window.

The ready preparation and the slots along the evolution

def CSD.RecordLayer.ClockReady (K : ℕ) : Set (ClockArena K)

The ready preparation: every slot in the ready arc.

Equations

• CSD.RecordLayer.ClockReady K = {x : CSD.RecordLayer.ClockArena K | ∀ (n : Fin K), x.2 n ∈ CSD.RecordLayer.readyArc K}

theorem CSD.RecordLayer.measurableSet_clockReady {K : ℕ} : MeasurableSet (ClockReady K)

theorem CSD.RecordLayer.clockEvolve_slot_zero {K : ℕ} {T : ℝ} (hT : 0 < T) (t : SigmaLayer.OnticTime) (x : ClockArena K) (n : Fin K) : (clockEvolve T 0 t x).2 n = pshift (winElapsed T (↑n) t * shearGap K) (x.2 n)

Slot n along the evolution from time 0.

theorem CSD.RecordLayer.slot_ready_before {K : ℕ} {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) (n : Fin K) {t : SigmaLayer.OnticTime} (ht : t ≤ ↑↑n * T) : (clockEvolve T 0 t x).2 n ∈ readyArc K

★ Before its window, slot n is still ready.

theorem CSD.RecordLayer.slot_written_after {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) (n : Fin K) {t : SigmaLayer.OnticTime} (ht : (↑↑n + 1) * T ≤ t) : (clockEvolve T 0 t x).2 n ∈ writtenArc K

★ After its window, slot n is written: the concrete evolution writes tick n from the ready preparation.

theorem CSD.RecordLayer.slot_written_mono {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) (n : Fin K) {s t : SigmaLayer.OnticTime} (hst : s ≤ t) (hw : (clockEvolve T 0 s x).2 n ∈ writtenArc K) : (clockEvolve T 0 t x).2 n ∈ writtenArc K

★ A written tick stays written: slot membership in the written arc is monotone in time.

The tick count

noncomputable def CSD.RecordLayer.tickCount {K : ℕ} (x : ClockArena K) : ℕ

The tick count: the number of slots in the written arc.

Equations

• CSD.RecordLayer.tickCount x = {n : Fin K | x.2 n ∈ CSD.RecordLayer.writtenArc K}.card

theorem CSD.RecordLayer.tickCount_eq_sum {K : ℕ} (x : ClockArena K) : tickCount x = ∑ n : Fin K, if x.2 n ∈ writtenArc K then 1 else 0

theorem CSD.RecordLayer.measurable_tickCount {K : ℕ} : Measurable tickCount

★ The readout is measurable.

theorem CSD.RecordLayer.tickCount_le_horizon {K : ℕ} (x : ClockArena K) : tickCount x ≤ K

The count never exceeds the horizon: finite memory.

theorem CSD.RecordLayer.tickCount_mono {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) {s t : SigmaLayer.OnticTime} (hst : s ≤ t) : tickCount (clockEvolve T 0 s x) ≤ tickCount (clockEvolve T 0 t x)

★★ The tick count is nondecreasing along the evolution from the ready preparation.

theorem CSD.RecordLayer.tickCount_ge {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) (n : Fin K) {t : SigmaLayer.OnticTime} (ht : (↑↑n + 1) * T ≤ t) : ↑n + 1 ≤ tickCount (clockEvolve T 0 t x)

★★ After n + 1 full periods, at least n + 1 ticks.

theorem CSD.RecordLayer.tickCount_le {K : ℕ} {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) (n : ℕ) {t : SigmaLayer.OnticTime} (ht : t ≤ ↑n * T) : tickCount (clockEvolve T 0 t x) ≤ n

★★ Before n periods, at most n ticks.

theorem CSD.RecordLayer.tickCount_at_period {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) {m : ℕ} (hm : m ≤ K) : tickCount (clockEvolve T 0 (↑m * T) x) = m

★★ Exactly m ticks at time m T, for m up to the horizon.

theorem CSD.RecordLayer.successive_ticks_distinguishable {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) {m : ℕ} (hm : m + 1 ≤ K) : clockEvolve T 0 (↑(m + 1) * T) x ≠ clockEvolve T 0 (↑m * T) x

★ Successive ticks occupy distinguishable register states.

Each slot is a measurement protocol; ticks persist

noncomputable def CSD.RecordLayer.tickProtocol {K : ℕ} (T : ℝ) (n : Fin K) (τR : ℝ) : MeasurementProtocol (ClockArena K) 1

Slot n as a MeasurementProtocol with one outcome ("the tick is written"): start at n T, readout at (n+1) T, record lifetime τR.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.RecordLayer.tickProtocol_pointerInvariant {K : ℕ} {T : ℝ} (hT : 0 < T) (n : Fin K) (τR : ℝ) : (tickProtocol T n τR).PointerInvariantOn

After its readout the slot is frozen, so the written arc is invariant: the hypothesis the persistence theorem asks for, discharged by the dynamics.

theorem CSD.RecordLayer.tick_persists {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) (n : Fin K) {τR t : ℝ} (ht₁ : (↑↑n + 1) * T ≤ t) (ht₂ : t ≤ (↑↑n + 1) * T + τR) : (clockEvolve T 0 t x).2 n ∈ writtenArc K

★ Tick n persists from its readout through the record lifetime — by the corpus's record_persists_on_interval, applied to tickProtocol n from the state at the start of its window.

The calibrated reading

noncomputable def CSD.RecordLayer.tickReading {K : ℕ} (τtick : ℝ) (x : ClockArena K) : ℝ

The calibrated reading τ_A = tickCount · τ_tick: the physical count times the unit.

Equations

• CSD.RecordLayer.tickReading τtick x = ↑(CSD.RecordLayer.tickCount x) * τtick

theorem CSD.RecordLayer.tickReading_nonneg {K : ℕ} {τtick : ℝ} (h : 0 ≤ τtick) (x : ClockArena K) : 0 ≤ tickReading τtick x

theorem CSD.RecordLayer.abs_tickReading_sub_lt {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) {t : SigmaLayer.OnticTime} (ht0 : 0 ≤ t) (htK : t ≤ ↑K * T) : |tickReading T (clockEvolve T 0 t x) - t| < T

★★ Calibrated with the period, the clock reads within one tick of t_Σ over the horizon: |tickCount · T − t| < T for 0 ≤ t ≤ K T. The reading is a record count; t is the ontic parameter of the schedule; they agree to within the resolution of one tick, and that is the whole relation between them.

The package

theorem CSD.RecordLayer.record_clock {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {x : ClockArena K} (hx : x ∈ ClockReady K) : (∀ (s t : SigmaLayer.OnticTime), MeasureTheory.MeasurePreserving (clockEvolve T s t) MeasureTheory.volume MeasureTheory.volume) ∧ Measurable tickCount ∧ (∀ (s t : SigmaLayer.OnticTime), s ≤ t → tickCount (clockEvolve T 0 s x) ≤ tickCount (clockEvolve T 0 t x)) ∧ (∀ (t : SigmaLayer.OnticTime), tickCount (clockEvolve T 0 t x) ≤ K) ∧ (∀ m ≤ K, tickCount (clockEvolve T 0 (↑m * T) x) = m) ∧ (∀ (n : Fin K) (s t : SigmaLayer.OnticTime), (↑↑n + 1) * T ≤ s → s ≤ t → (clockEvolve T 0 t x).2 n ∈ writtenArc K) ∧ ∀ (t : SigmaLayer.OnticTime), 0 ≤ t → t ≤ ↑K * T → |tickReading T (clockEvolve T 0 t x) - t| < T

★★★ The record clock. From the ready preparation on a horizon of K ≥ 1 slots, with period T > 0: the propagator is a measure-preserving two-time dynamics; the tick count is measurable, nondecreasing, never above K, exactly m at time m T; each tick, once written, persists; and calibrated with the period the reading is within one tick of t_Σ.