The autonomous clock-and-echo model on one arena #

Category: 7-SigmaLayer (the record layer). BACKLOG #202, the dynamics half (out of #39; the author's third operational-geometry brief's one exact deliverable: a finite autonomous clock-and-echo model whose emission and return timestamps are physical records at the same station, with a derived round-trip timing bound and explicit detector back-reaction).

#200 read the round trip off A's two records against #185's scheduled clock. Here the clock is #201's hand clock — one more carrier and one more pointer, at A — and the whole device sits on one arena with one two-time evolution:

ClockEchoArena = EchoArena × ActiveArena,

the echo's carrier with its two pointers, and the clock's carrier with its hand. Nothing in the evolution tests t_Σ: the echo's writes are activated by the echo's carrier, the clock's ticks by the clock's carrier, and the timestamps are the hand's count, read while A's emission record and A's return record display. Every detector's back-reaction is in the model as the detuning of its own carrier.

ClockEchoArena, clockEchoEvolve — one two-time, autonomous, measure-preserving evolution (clockEchoEvolve_comp, clockEchoEvolve_shift, clockEchoEvolve_measurePreserving);
★★ clockEchoEmission, clockEchoReception, clockEchoReturn, clockEchoTick — the echo's three writes and the clock's ticks as ActualOccurrences on the one arena (#191), every one of them activated by a carrier; clockEchoLabel — the hand's count as the clock label; emissionLabel_time, returnLabel_time — the two events labelled by the hand;
clockReadingAt, clockEchoReadings — the radar timestamps are the hand's readings at a time while the emission record displays and at a time while the return record displays; ★★ clockEchoReadings_eq_labels — at the write completions they are τ_tick times the two events' hand labels;
clockEchoBudget — the derived round-trip budget: the clock's resolution τ_tick + 1/(2ω_c) (#201, derived) in place of #185's T, the emission write's completion, the return write's response, the two transfers, and the retention window (input); ★★ abs_clockEchoReadings_emit_sub_le, abs_clockEchoReadings_ret_sub_le;
★★★ autonomous_clock_and_echo — the deliverable: on one arena with one autonomous evolution, both timestamps are readings of the autonomous clock at A taken at A's two records, and the radar time, separation and distance are within the derived budget of the ideal round trip (0, 2τ_hop), whose separation is τ_hop.

Honest scope #

The echo and the clock are two carrier–pointer systems on a product arena; they do not interact. The clock is colocated with A by fiat of the model — a shared site label — not by a coupling. Coupling the two (the clock's carrier detuned by the echo's) is a further row.
Hamiltonian generation of the combined arena, (ℂℙ³ × T² × T²) × (ℂℙ³ × T²), is the second half of #202 (RecordLayer/EchoHamiltonian.lean for the echo factor; the clock factor is #195).
The input bounds are the two retention windows and the clock's horizon (one turn of the hand).
No universal c, no Lorentz invariance. c₀ is a calibration constant. The #187 and #190 headers stand.

References: specs/BACKLOG.md #202, #199, #200, #201, #194, #195, #39; RecordLayer/EchoArena.lean, RecordLayer/EchoRadar.lean (echoReturnDelay, abs_detunedRoundTrip_sub_roundTrip_le), RecordLayer/HandClock.lean (hand, handReading, abs_handReading_sub_le, handCount_mono, tickWrite), CV/RadarCoordinates.lean.

The autonomous clock-and-echo model on one arena #

Honest scope #

The arena and its evolution #

The writes on the one arena #

The readings, the budget and the bound #