Operational geometry of the clock-and-echo witness: the capstone

Category: 7-SigmaLayer (the record layer — the terminal statement of the clock-and-echo programme). BACKLOG #187 (out of #39; the fifth of #183–#189).

On the explicit finite arena of #186, from the stated ready preparation with message b, the one constructed evolution produces persistent clock records (#185) and persistent exchange records (#186) from the actual transfer (#183); the clock's readings at emission and return define radar coordinates (#184) that every repeated exchange reproduces; the represented events respect the causal order; and bounded readout errors give bounded coordinate errors.

• arenaFlow_cycles — the exchange returns to the message point after every round trip, so the stationary witness repeats itself: cycle m emits at 2m τ_hop, is received at (2m+1) τ_hop (receiver_cycle), returns at (2m+2) τ_hop;
• clockReading — the physical clock's calibrated reading in the arena at an ontic time; cycleReadings m — the radar readings of cycle m are the clock's readings at its emission and return, a RadarReadings whose domain condition is the monotonicity of the tick count;
• ★★ radarSep_cycle, radarTime_cycle — under the calibration T = τ_hop, cycle m has radar separation τ_tick and radar time (2m+1) τ_tick: repeated exchanges reproduce the same separation;
• ★★★ operational_geometry — the capstone, twelve conjuncts, every one consumed from #183–#186 and #184 and none carried by a structure field.

Capstone discipline (CONVENTIONS.md §8.3b)

The corpus's records→spacetime capstone, record_influence_le_of_separated (CV/TwoCones.lean, #98), is a statement about cone containment: a record cannot be steered from outside the Lieb–Robinson cone. This theorem is a statement about operational coordinates: what two clock readings of one experiment define, and how they transform and err. The two are different claim surfaces, so this stands as its own terminal statement rather than as a conjunct on #98 — the decision #187 asked to be confirmed against the rule, confirmed here: adding these conjuncts to #98 would fragment neither surface into the other but merge two unrelated citations.

What is not claimed

No metric and no volume element on the event order (specs/records-to-spacetime-scoping.md §8). No universal signal speed: c₀ is a calibration constant, and radarDist_rescale_eq says it absorbs the clock unit. The cone of the corpus moves one edge per period in a preferred frame (#98). The schedule — switch-on, readout times, clock windows — is a modelling input indexed by t_Σ, and the identification of the clock's tick count with the record event's period index is the stated choice T = τ_hop, not a dynamical fact. Hamiltonian generation of the propagator is not formalised.

References: specs/BACKLOG.md #187, #183–#186, #39; CONVENTIONS.md §8.3b; RecordLayer/RecordedExchange.lean, RecordLayer/RecordClock.lean, CV/SignalExchange.lean, CV/RadarCoordinates.lean, CV/TwoCones.lean.

The stationary witness repeats itself

theorem CSD.RecordLayer.arenaFlow_cycles {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (m : ℕ) : (CV.hopFlow J ħ).arenaFlow (↑m * CV.roundTrip J ħ) (CV.msgPoint 1) = CV.msgPoint 1

After every round trip the exchange is back at the message point.

theorem CSD.RecordLayer.arenaFlow_cycle_reception {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (m : ℕ) : (CV.hopFlow J ħ).arenaFlow (↑m * CV.roundTrip J ħ + CV.hopTime J ħ) (CV.msgPoint 1) = Projectivization.mk ℂ (CV.basisVec CV.excB) ⋯

At the reception time of cycle m the exchange is the excitation at B.

theorem CSD.RecordLayer.receiver_cycle {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (m : ℕ) : CV.arenaObs CV.occB ((CV.hopFlow J ħ).arenaFlow (↑m * CV.roundTrip J ħ + CV.hopTime J ħ) (CV.msgPoint 1)) = 1

The receiver responds in every cycle: the readout at B is 1 at every reception time.

theorem CSD.RecordLayer.xEvolve_exchange_of_nonneg {K : ℕ} (J ħ T : ℝ) {t : SigmaLayer.OnticTime} (ht : 0 ≤ t) (x : XArena K) : (xEvolve J ħ T (-1) t x).1 = (CV.hopFlow J ħ).arenaFlow t x.1

The exchange factor of the arena at a nonnegative time is the hop run for that time.

The clock's readings as radar readings

noncomputable def CSD.RecordLayer.clockReading {K : ℕ} (J ħ T τtick : ℝ) (x : XArena K) (t : SigmaLayer.OnticTime) : ℝ

The physical clock's calibrated reading in the arena at ontic time t, unit τ_tick.

Equations

• CSD.RecordLayer.clockReading J ħ T τtick x t = CSD.RecordLayer.tickReading τtick (CSD.RecordLayer.xEvolve J ħ T (-1) t x).2.1

theorem CSD.RecordLayer.clockReading_eq {K : ℕ} {J ħ T : ℝ} (hT : 0 < T) (τtick : ℝ) (x : XArena K) (t : SigmaLayer.OnticTime) : clockReading J ħ T τtick x t = ↑(tickCount (clockEvolve T 0 t x.2.1)) * τtick

theorem CSD.RecordLayer.clockReading_mono {K : ℕ} {J ħ T τtick : ℝ} (hK : 0 < K) (hT : 0 < T) (hτ : 0 ≤ τtick) {x : XArena K} (hx : x ∈ XReady K) {s t : SigmaLayer.OnticTime} (hst : s ≤ t) : clockReading J ħ T τtick x s ≤ clockReading J ħ T τtick x t

The clock's reading is nondecreasing in ontic time.

theorem CSD.RecordLayer.clockReading_at_period {K : ℕ} {J ħ T τtick : ℝ} (hK : 0 < K) (hT : 0 < T) {x : XArena K} (hx : x ∈ XReady K) {m : ℕ} (hm : m ≤ K) : clockReading J ħ T τtick x (↑m * T) = ↑m * τtick

At a tick boundary within the horizon the clock reads the tick.

noncomputable def CSD.RecordLayer.cycleReadings {K : ℕ} {J ħ T τtick : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hK : 0 < K) (hT : 0 < T) (hτ : 0 ≤ τtick) {x : XArena K} (hx : x ∈ XReady K) (m : ℕ) : CV.RadarReadings

The radar readings of cycle m: the clock's readings at the cycle's emission 2m τ_hop and return (2m+2) τ_hop. The domain condition τ₋ ≤ τ₊ is the monotonicity of the tick count.

Equations

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

theorem CSD.RecordLayer.cycleReadings_emit {K : ℕ} {J ħ T τtick : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hK : 0 < K) (hT : 0 < T) (hτ : 0 ≤ τtick) {x : XArena K} (hx : x ∈ XReady K) (m : ℕ) : (cycleReadings hJ hħ hK hT hτ hx m).emit = clockReading J ħ T τtick x (↑(2 * m) * CV.hopTime J ħ)

theorem CSD.RecordLayer.cycleReadings_ret {K : ℕ} {J ħ T τtick : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hK : 0 < K) (hT : 0 < T) (hτ : 0 ≤ τtick) {x : XArena K} (hx : x ∈ XReady K) (m : ℕ) : (cycleReadings hJ hħ hK hT hτ hx m).ret = clockReading J ħ T τtick x (↑(2 * m + 2) * CV.hopTime J ħ)

theorem CSD.RecordLayer.radarSep_cycle {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) {m : ℕ} (hm : 2 * m + 2 ≤ K) : (cycleReadings hJ hħ hK hT hτ hx m).radarSep = τtick

★★ Under the calibration T = τ_hop, every cycle has radar separation τ_tick: repeated exchanges reproduce the same separation.

theorem CSD.RecordLayer.radarTime_cycle {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) {m : ℕ} (hm : 2 * m + 2 ≤ K) : (cycleReadings hJ hħ hK hT hτ hx m).radarTime = (2 * ↑m + 1) * τtick

Under the calibration, cycle m has radar time (2m+1) τ_tick.

The capstone

theorem CSD.RecordLayer.operational_geometry {K : ℕ} {J ħ T τtick : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hTcal : T = CV.hopTime J ħ) (hK : 2 ≤ K) {c : ClockArena K} (hc : c ∈ ClockReady K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (hτ : 0 < τtick) (b : Fin 2) : have hT := ⋯; have hK0 := ⋯; have hx := ⋯; have x := xPrep b c r; (∀ (s t u : SigmaLayer.OnticTime), xEvolve J ħ T t u ∘ xEvolve J ħ T s t = xEvolve J ħ T s u) ∧ (∀ (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena 2 2), MeasureTheory.MeasurePreserving (xEvolve J ħ T s t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)) ∧ (∀ (n : Fin K) (s t : SigmaLayer.OnticTime), (↑↑n + 1) * T ≤ s → s ≤ t → (xEvolve J ħ T (-1) t x).2.1.2 n ∈ writtenArc K) ∧ (∀ (i : Fin 3) (t : SigmaLayer.OnticTime), readTime J ħ i ≤ t → (xEvolve J ħ T (-1) t x).2.2 i ∈ pointerArc 2 b) ∧ (∀ (t : SigmaLayer.OnticTime), CV.hopTime J ħ ≤ t → (xEvolve J ħ T (-1) t (xPrep 1 c r)).2.2 1 ≠ (xEvolve J ħ T (-1) t (xPrep 0 c r)).2.2 1) ∧ (CV.arenaObs CV.occB (xEvolve J ħ T (-1) (CV.hopTime J ħ) (xPrep 1 c r)).1 = 1 ∧ CV.arenaObs CV.occB (xEvolve J ħ T (-1) (CV.hopTime J ħ) (xPrep 0 c r)).1 = 0) ∧ 0 < CV.roundTrip J ħ ∧ ((cycleReadings hJ hħ hK0 hT ⋯ hx 0).radarSep = τtick ∧ (cycleReadings hJ hħ hK0 hT ⋯ hx 0).radarTime = τtick) ∧ (∀ (m : ℕ), 2 * m + 2 ≤ K → (cycleReadings hJ hħ hK0 hT ⋯ hx m).radarSep = τtick ∧ (CV.hopFlow J ħ).arenaFlow (↑m * CV.roundTrip J ħ) (CV.msgPoint 1) = CV.msgPoint 1 ∧ CV.arenaObs CV.occB ((CV.hopFlow J ħ).arenaFlow (↑m * CV.roundTrip J ħ + CV.hopTime J ħ) (CV.msgPoint 1)) = 1) ∧ (CV.CausalPrecedes hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (reception J ħ b)) ∧ CV.CausalPrecedes hopGraph (eventOf J ħ T x (reception J ħ b)) (eventOf J ħ T x (returnOcc J ħ b)) ∧ CV.CausalPrecedes hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (returnOcc J ħ b))) ∧ (∀ (r' : CV.RadarReadings) (δ c₀ : ℝ), 0 ≤ c₀ → |r'.emit - (cycleReadings hJ hħ hK0 hT ⋯ hx 0).emit| ≤ δ → |r'.ret - (cycleReadings hJ hħ hK0 hT ⋯ hx 0).ret| ≤ δ → |r'.radarTime - (cycleReadings hJ hħ hK0 hT ⋯ hx 0).radarTime| ≤ δ ∧ |r'.radarSep - (cycleReadings hJ hħ hK0 hT ⋯ hx 0).radarSep| ≤ δ ∧ |r'.radarDist c₀ - (cycleReadings hJ hħ hK0 hT ⋯ hx 0).radarDist c₀| ≤ c₀ * δ) ∧ ∀ (t : SigmaLayer.OnticTime), tickCount (xEvolve J ħ T (-1) t x).2.1 ≤ K

★★★ Operational geometry of the clock-and-echo witness. With J, ħ > 0, clock period calibrated to the hop time, a horizon of at least two ticks, the ready preparation with message b, and a clock unit τ_tick > 0:

1. the joint evolution obeys the two-time law and
2. preserves Liouville measure (Fubini–Study × Haar × Haar) — one dynamics on one arena;
3. the clock's records persist: a tick once written stays written through the horizon;
4. the exchange records persist: each register displays the message from its readout time on;
5. the two messages are distinguishable at the receiver's record;
6. the receiver responds: readout 1 for message 1 and 0 for message 0 at τ_hop;
7. the round trip is nonzero;
8. the clock's readings at emission and return define radar coordinates with separation τ_tick and time τ_tick;
9. every repeated cycle within the horizon reproduces the separation τ_tick, returns the exchange to the message point, and is received with readout 1;
10. the represented events satisfy emission ⪯ reception ⪯ return on the hop graph;
11. readings with endpoint errors ≤ δ give coordinate errors ≤ δ and a distance error ≤ c₀ δ;
12. memory is finite: the tick count never exceeds the horizon.