The drift pointer as an autonomous hand clock

Category: 7-SigmaLayer (the record layer). BACKLOG #201 (out of #39; the author's third operational-geometry brief, §2: make the reference clock internally driven).

#185's record clock writes its ticks by a schedule: slot n is written on the window [nT, (n+1)T] of t_Σ. Here the clock is #194's activated write read differently. One carrier (message 1, prepared at A) and one pointer (at B, prepared in the first half-arc) are the whole device; the carrier shuttles between the sites on its own, the pointer turns at the rate −(2g/ħ) f'(θ₂) n_B only while the carrier is at B, and its lifted displacement after time t is D(t) = κ (ωt − sin ωt cos ωt)/(2ω) with κ = −(2g/ħ) f'(θ₂)(J/Ω)², ω = Ω/ħ: a staircase of mean slope κ/2 whose steps are the carrier's visits. Read in K equal arcs, the pointer is a hand and each arc crossing is a tick written by the carrier itself. The smallest finite clock whose internal state activates its tick writes: one carrier, one pointer, K arcs, against #185's K slot tori.

• handCount, handReading, handArc, ★ handCount_eq_iff — the hand read in K arcs: the tick count is the arc index of the pointer's representative, and the arcs are disjoint intervals; handReady — the preparation (first half-arc);
• hand, hand_eq — the hand's motion is #194's pointer, pshift (pointerDrift κ ω t) q; ★ pointerDrift_mono — the hand never turns back (the group law of the accumulated occupancy); rep_hand_of_le — no wrap below one turn;
• tickTime — the derived calibration τ_tick = 2/(Kκ): the time in which the mean slope crosses one arc; ★ pointerDrift_tickTime — after n τ_tick the hand has crossed n arcs up to the band κ/(4ω); handHorizon — the horizon, one turn: (2/κ)(1 − 1/K) − 1/(2ω); handHorizon_pos;
• ★★ handCount_mono — ticks persist: the count is non-decreasing over the horizon; ★★ abs_handReading_sub_le — the resolution bound |handReading − t| ≤ τ_tick + 1/(2ω) over the horizon: one arc of count uncertainty plus the band of the staircase about its mean;
• tickStart, tickEnd, tickWindow; ★★ hand_before_tick, hand_at_tick — tick n is a write: before (2n−1)/(2Kκ) the count is below n, and on [n τ_tick + 1/(2ω), n τ_tick + 1/(2ω) + (τ_tick/2 − 1/ω)] it is exactly n, under the slowness Kκ ≤ ω (the hand gains at most one arc per Rabi radian); ★★★ tickWrite — each tick as an ActualOccurrence (#191) at site {B}, from the start 0, value n, for 1 ≤ n ≤ K − 1; tickWrite_value_ne — successive ticks are distinguishable; tickEnd_succ — they are spaced by τ_tick; ★ handTick_persists — once written, the count never drops below n over the horizon;
• ★ handClock_generated — generation inherited from #195: the clock's dynamics is the flow of the activated energy on the arena, no new geometry;
• ★★★ hand_clock — the package.

Honest scope

• The controller is explicit and in the model: the carrier of message 1, with its back-reaction (the detuning g f(θ₂)) on the hand's own dynamics. There is no schedule anywhere; the only parameter is the time t at which the arena is inspected.
• The hand is a staircase, not a uniform rotation: it moves while the carrier is at B and is nearly still while the carrier is at A (the loss 1 − (J/Ω)² keeps it from stopping exactly). The resolution bound pays for this with the band 1/(2ω), which is the clock's intrinsic jitter — half a Rabi radian.
• Over one turn only; wrapping is the horizon. A clock that counts turns is a further register.
• The preparation is the first half-arc, finer than #194's ready arc: the record windows need the preparation width below the arc width, as #194's analysis showed.

References: specs/BACKLOG.md #201, #194, #195, #185, #202, #39; RecordLayer/ActivatedWrite.lean (activeFlow, pointerDrift, driftRate, pointerDrift_lower, pointerDrift_upper, pointerAmount_add), RecordLayer/ActivatedHamiltonian.lean (hamiltonianFlow_activeFlow), RecordLayer/RecordClock.lean (the scheduled clock this replaces), RecordLayer/RecordOccurrence.lean.

The hand read in K arcs

noncomputable def CSD.RecordLayer.handCount (K : ℕ) (q : LF4.KTorus) : ℕ

The tick count: the arc index of the pointer's representative among K equal arcs (n/K, (n+1)/K].

Equations

• CSD.RecordLayer.handCount K q = ⌈↑K * CSD.RecordLayer.rep q.1⌉₊ - 1

theorem CSD.RecordLayer.measurable_handCount (K : ℕ) : Measurable (handCount K)

noncomputable def CSD.RecordLayer.handReading (K : ℕ) (τ : ℝ) (q : LF4.KTorus) : ℝ

The clock reading: the tick count times the calibration.

Equations

• CSD.RecordLayer.handReading K τ q = ↑(CSD.RecordLayer.handCount K q) * τ

def CSD.RecordLayer.handArc (K n : ℕ) : Set LF4.KTorus

The arc displaying count n.

Equations

• CSD.RecordLayer.handArc K n = {q : CSD.LF4.KTorus | CSD.RecordLayer.handCount K q = n}

theorem CSD.RecordLayer.handArc_disjoint (K : ℕ) {n m : ℕ} (h : n ≠ m) : Disjoint (handArc K n) (handArc K m)

theorem CSD.RecordLayer.handCount_eq_iff {K : ℕ} (hK : 0 < K) (q : LF4.KTorus) (n : ℕ) : handCount K q = n ↔ rep q.1 ∈ Set.Ioc (↑n / ↑K) ((↑n + 1) / ↑K)

★ The arcs are intervals: handCount q = n iff rep q ∈ (n/K, (n+1)/K].

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

The hand's preparation: the first half-arc.

Equations

• CSD.RecordLayer.handReady K = {q : CSD.LF4.KTorus | CSD.RecordLayer.rep q.1 ∈ Set.Ioc 0 (1 / (2 * ↑K))}

theorem CSD.RecordLayer.measurableSet_handReady (K : ℕ) : MeasurableSet (handReady K)

The hand's motion

noncomputable def CSD.RecordLayer.handRate {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (q : LF4.KTorus) : ℝ

The hand's mean rate κ = −(2g/ħ) f'(θ₂) (J/Ω)².

Equations

• CSD.RecordLayer.handRate J ħ g hf q = CSD.RecordLayer.driftRate J ħ g hf q.2

noncomputable def CSD.RecordLayer.handFreq {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (q : LF4.KTorus) : ℝ

The hand's Rabi rate ω = Ω/ħ.

Equations

• CSD.RecordLayer.handFreq J ħ g hf q = CSD.CV.rabiRate J ħ (CSD.RecordLayer.detuningAt g hf q.2)

noncomputable def CSD.RecordLayer.hand {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) (q : LF4.KTorus) : LF4.KTorus

The hand: the pointer of #194's activated write with the carrier prepared as message 1.

Equations

• CSD.RecordLayer.hand J ħ g hf t q = (CSD.RecordLayer.activeFlow J ħ g hf t (CSD.CV.msgPoint 1, q)).2

theorem CSD.RecordLayer.handFreq_pos {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (q : LF4.KTorus) : 0 < handFreq J ħ g hf q

theorem CSD.RecordLayer.hand_eq {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (t : ℝ) (q : LF4.KTorus) : hand J ħ g hf t q = pshift (pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t) q

The hand's motion in closed form: the drift κ (ωt − sin ωt cos ωt)/(2ω).

theorem CSD.RecordLayer.hand_zero {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (q : LF4.KTorus) : hand J ħ g hf 0 q = q

theorem CSD.RecordLayer.rateAt_pos_of_handRate_pos {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) {q : LF4.KTorus} (hκ : 0 < handRate J ħ g hf q) : 0 < rateAt g ħ hf q.2

The pointer's own rate is positive when the mean rate is.

theorem CSD.RecordLayer.pointerDrift_mono {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {q : LF4.KTorus} (hκ : 0 < handRate J ħ g hf q) {s t : ℝ} (hst : s ≤ t) : pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) s ≤ pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t

★ The hand never turns back: the drift is non-decreasing, by the group law of the accumulated occupancy.

theorem CSD.RecordLayer.rep_hand_of_le {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {q : LF4.KTorus} (hq0 : 0 < rep q.1) {t : ℝ} (hD : 0 ≤ pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t) (h : rep q.1 + pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t ≤ 1) : rep (hand J ħ g hf t q).1 = rep q.1 + pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t

No wrap: below one turn the representative of the hand is the prepared representative plus the drift.

Calibration and horizon

noncomputable def CSD.RecordLayer.tickTime (K : ℕ) (κ : ℝ) : ℝ

The derived calibration: the time τ_tick = 2/(Kκ) in which the mean slope κ/2 crosses one arc 1/K.

Equations

• CSD.RecordLayer.tickTime K κ = 2 / (↑K * κ)

noncomputable def CSD.RecordLayer.handHorizon (K : ℕ) (κ ω : ℝ) : ℝ

The horizon: one turn, (2/κ)(1 − 1/K) − 1/(2ω).

Equations

• CSD.RecordLayer.handHorizon K κ ω = 2 / κ * (1 - 1 / ↑K) - 1 / (2 * ω)

theorem CSD.RecordLayer.tickTime_pos {K : ℕ} (hK : 0 < K) {κ : ℝ} (hκ : 0 < κ) : 0 < tickTime K κ

theorem CSD.RecordLayer.mul_tickTime {K : ℕ} (hK : 0 < K) {κ : ℝ} (hκ : 0 < κ) : ↑K * κ * tickTime K κ = 2

theorem CSD.RecordLayer.handHorizon_pos {K : ℕ} (hK : 2 ≤ K) {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) (hslow : κ ≤ ω) : 0 < handHorizon K κ ω

A hand slower than its Rabi rate has a positive horizon once K ≥ 2.

theorem CSD.RecordLayer.band_at_handHorizon {K : ℕ} {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) : κ * (handHorizon K κ ω / 2 + 1 / (4 * ω)) = 1 - 1 / ↑K

At the horizon the upper band reaches 1 − 1/K.

theorem CSD.RecordLayer.pointerDrift_tickTime {K : ℕ} (hK : 0 < K) {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) (n : ℕ) : ↑n / ↑K - κ / (4 * ω) ≤ pointerDrift κ ω (↑n * tickTime K κ) ∧ pointerDrift κ ω (↑n * tickTime K κ) ≤ ↑n / ↑K + κ / (4 * ω)

★ The calibration is derived: after n tick times the hand has crossed n arcs, up to the band κ/(4ω).

Persistence and resolution

theorem CSD.RecordLayer.rep_hand {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q)) : rep (hand J ħ g hf t q).1 = rep q.1 + pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t

Over the horizon the hand has not wrapped.

theorem CSD.RecordLayer.handCount_mono {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) (ht : t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q)) : handCount K (hand J ħ g hf s q) ≤ handCount K (hand J ħ g hf t q)

★★ Ticks persist: over the horizon the count never decreases.

theorem CSD.RecordLayer.abs_handCount_sub_le {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q)) : |↑(handCount K (hand J ħ g hf t q)) - ↑K * pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t| ≤ 1

The count is within one of K times the drift (the preparation lies in the first half-arc).

theorem CSD.RecordLayer.abs_handReading_sub_le {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q)) : |handReading K (tickTime K (handRate J ħ g hf q)) (hand J ħ g hf t q) - t| ≤ tickTime K (handRate J ħ g hf q) + 1 / (2 * handFreq J ħ g hf q)

★★ The resolution bound: calibrated with τ_tick = 2/(Kκ), the hand reads within τ_tick + 1/(2ω) of t over the horizon — one arc of count uncertainty plus the staircase's band about its mean.

Each tick as a write

noncomputable def CSD.RecordLayer.tickStart (K : ℕ) (κ : ℝ) (n : ℕ) : ℝ

Tick n cannot have been written before (2n − 1)/(2Kκ).

Equations

• CSD.RecordLayer.tickStart K κ n = (2 * ↑n - 1) / (2 * ↑K * κ)

noncomputable def CSD.RecordLayer.tickEnd (K : ℕ) (κ ω : ℝ) (n : ℕ) : ℝ

Tick n is written by n τ_tick + 1/(2ω).

Equations

• CSD.RecordLayer.tickEnd K κ ω n = ↑n * CSD.RecordLayer.tickTime K κ + 1 / (2 * ω)

noncomputable def CSD.RecordLayer.tickWindow (K : ℕ) (κ ω : ℝ) : ℝ

The window on which tick n displays: τ_tick/2 − 1/ω.

Equations

• CSD.RecordLayer.tickWindow K κ ω = CSD.RecordLayer.tickTime K κ / 2 - 1 / ω

theorem CSD.RecordLayer.tickEnd_succ (K : ℕ) (κ ω : ℝ) (n : ℕ) : tickEnd K κ ω (n + 1) = tickEnd K κ ω n + tickTime K κ

theorem CSD.RecordLayer.tickStart_nonneg {K : ℕ} (hK : 0 < K) {κ : ℝ} (hκ : 0 < κ) {n : ℕ} (hn : 1 ≤ n) : 0 ≤ tickStart K κ n

theorem CSD.RecordLayer.tickStart_le_tickEnd {K : ℕ} (hK : 0 < K) {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) (n : ℕ) : tickStart K κ n ≤ tickEnd K κ ω n

theorem CSD.RecordLayer.tickWindow_nonneg {K : ℕ} (hK : 0 < K) {κ ω : ℝ} (hκ : 0 < κ) (hslow : ↑K * κ ≤ ω) : 0 ≤ tickWindow K κ ω

The window is a window exactly when the hand gains at most one arc per Rabi radian: Kκ ≤ ω.

theorem CSD.RecordLayer.band_at_tickEnd {K : ℕ} (hK : 0 < K) {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) (n : ℕ) : κ * (tickEnd K κ ω n / 2 - 1 / (4 * ω)) = ↑n / ↑K

theorem CSD.RecordLayer.band_at_tickWindow_end {K : ℕ} (hK : 0 < K) {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) (n : ℕ) : κ * ((tickEnd K κ ω n + tickWindow K κ ω) / 2 + 1 / (4 * ω)) = ↑n / ↑K + 1 / (2 * ↑K)

theorem CSD.RecordLayer.hand_before_tick {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) {n : ℕ} (hn1 : 1 ≤ n) (hnK : n + 1 ≤ K) {t : ℝ} (ht0 : 0 ≤ t) (ht : t < tickStart K (handRate J ħ g hf q) n) : handCount K (hand J ħ g hf t q) < n

★★ Before its start, tick n has not been written: the count is below n.

theorem CSD.RecordLayer.hand_at_tick {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) {n : ℕ} (hnK : n + 1 ≤ K) {t : ℝ} (ht₁ : tickEnd K (handRate J ħ g hf q) (handFreq J ħ g hf q) n ≤ t) (ht₂ : t ≤ tickEnd K (handRate J ħ g hf q) (handFreq J ħ g hf q) n + tickWindow K (handRate J ħ g hf q) (handFreq J ħ g hf q)) : handCount K (hand J ħ g hf t q) = n

★★ Through its window, tick n displays: the count is exactly n.

noncomputable def CSD.RecordLayer.tickWrite {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) (hslow : ↑K * handRate J ħ g hf q ≤ handFreq J ħ g hf q) {n : ℕ} (hn1 : 1 ≤ n) (hnK : n + 1 ≤ K) : ActualOccurrence ActiveArena ℕ 2

★★★ Tick n as an actual occurrence (#191): the hand at B (site {1}), history from 0, value n, write interval [(2n−1)/(2Kκ), n τ_tick + 1/(2ω)], window τ_tick/2 − 1/ω. The hypotheses: the hand prepared in the first half-arc, a positive mean rate, the slowness Kκ ≤ ω, and 1 ≤ n ≤ K − 1.

Equations

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

theorem CSD.RecordLayer.tickWrite_value_ne {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) (hslow : ↑K * handRate J ħ g hf q ≤ handFreq J ħ g hf q) {n : ℕ} (hn1 : 1 ≤ n) (hnK : n + 2 ≤ K) : (tickWrite J ħ g hf hJ hħ hf1 hK hq hκ hslow hn1 ⋯).value ≠ (tickWrite J ħ g hf hJ hħ hf1 hK hq hκ hslow ⋯ hnK).value

Successive ticks are distinguishable: their values differ, so their arcs are disjoint.

theorem CSD.RecordLayer.handTick_persists {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) (hslow : ↑K * handRate J ħ g hf q ≤ handFreq J ħ g hf q) {n : ℕ} (hnK : n + 1 ≤ K) {t : ℝ} (ht₁ : tickEnd K (handRate J ħ g hf q) (handFreq J ħ g hf q) n ≤ t) (ht : t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q)) : n ≤ handCount K (hand J ħ g hf t q)

★ Once written, a tick persists: from the completion of tick n to the horizon the count is at least n.

theorem CSD.RecordLayer.handClock_generated {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hc : ContDiff ℝ (↑⊤) f) (t : ℝ) (q : LF4.KTorus) : ⋯.hamiltonianFlow ⋯ t ((CV.fibredArenaEquiv 2 2) (CV.msgPoint 1, q)) = (CV.fibredArenaEquiv 2 2) (activeFlow J ħ g hf t (CV.msgPoint 1, q))

★ Generation inherited from #195, no new geometry: the hand clock's dynamics is the flow of the activated energy on the arena, read at the clock's preparation.

theorem CSD.RecordLayer.hand_clock {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {K : ℕ} (hK : 0 < K) {q : LF4.KTorus} (hq : q ∈ handReady K) (hκ : 0 < handRate J ħ g hf q) (hslow : ↑K * handRate J ħ g hf q ≤ handFreq J ħ g hf q) : (∀ (t : ℝ), hand J ħ g hf t q = pshift (pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t) q) ∧ (∀ (s t : ℝ), s ≤ t → pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) s ≤ pointerDrift (handRate J ħ g hf q) (handFreq J ħ g hf q) t) ∧ (∀ (s t : ℝ), 0 ≤ s → s ≤ t → t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q) → handCount K (hand J ħ g hf s q) ≤ handCount K (hand J ħ g hf t q)) ∧ (∀ (t : ℝ), 0 ≤ t → t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q) → |handReading K (tickTime K (handRate J ħ g hf q)) (hand J ħ g hf t q) - t| ≤ tickTime K (handRate J ħ g hf q) + 1 / (2 * handFreq J ħ g hf q)) ∧ (∀ (n : ℕ) (hn1 : 1 ≤ n) (hnK : n + 1 ≤ K), (tickWrite J ħ g hf hJ hħ hf1 hK hq hκ hslow hn1 hnK).site = {1} ∧ (tickWrite J ħ g hf hJ hħ hf1 hK hq hκ hslow hn1 hnK).prep = (CV.msgPoint 1, q) ∧ (tickWrite J ħ g hf hJ hħ hf1 hK hq hκ hslow hn1 hnK).value = n ∧ (tickWrite J ħ g hf hJ hħ hf1 hK hq hκ hslow hn1 hnK).writeEnd = tickEnd K (handRate J ħ g hf q) (handFreq J ħ g hf q) n) ∧ (∀ (n : ℕ), tickEnd K (handRate J ħ g hf q) (handFreq J ħ g hf q) (n + 1) = tickEnd K (handRate J ħ g hf q) (handFreq J ħ g hf q) n + tickTime K (handRate J ħ g hf q)) ∧ ∀ (n : ℕ), n + 1 ≤ K → ∀ (t : ℝ), tickEnd K (handRate J ħ g hf q) (handFreq J ħ g hf q) n ≤ t → t ≤ handHorizon K (handRate J ħ g hf q) (handFreq J ħ g hf q) → n ≤ handCount K (hand J ħ g hf t q)

★★★ The hand clock. One carrier and one pointer, read in K arcs, with the mean rate κ and the Rabi rate ω of the preparation: the hand is #194's pointer; it never turns back; its count never decreases over the horizon; calibrated with τ_tick = 2/(Kκ) it reads within τ_tick + 1/(2ω) of t; each tick n with 1 ≤ n ≤ K − 1 is an ActualOccurrence at site {B} from the start 0 with value n, successive ticks spaced by τ_tick, and once written a tick persists to the horizon.