Round-trip radar from the sender's records #

Category: 7-SigmaLayer (the record layer). BACKLOG #200 (out of #39; the author's third operational-geometry brief, §1's proof target).

#197 read a radar coordinate off one clock at A and a detection at B: a one-way flight. Here both radar timestamps are readings of A's clock, taken at A's two records — the emission arc and the return arc of the one register at A that the carrier itself writes (#199). The arena is #199's echo arena with #185's record clock alongside; the ideal readings are (0, 2τ_hop), the round trip, whose radar separation is τ_hop (radarSep_roundTrip). Every contribution to the error is derived for the witness; the two input bounds are labelled.

EchoClockedArena, echoClockedEvolve — the echo arena with the record clock: a two-time, measure-preserving dynamics; ★★ clockedEmissionRecord, clockedReturnRecord — A's two writes registered on it (#191), with the clock ready alongside the pointers; echoClockReading, emissionEvent_time, returnEvent_time — their events, labelled by the clock at the completion of each write; ★ emission_causalPrecedes_return — the emission precedes the return on the hop graph;
★ abs_detunedRoundTrip_sub_roundTrip_le — outward transfer + return transfer: the detuned round trip is within 2 transferError of 2τ_hop;
echoReturnDelay — the detector response of the return write: its completion minus the detuned round trip, explicit in the preparation (echoReturnDelay_eq); the emission write's response is its completion emitEnd itself;
echoReadings — the measured readings: A's clock at a time in the emission window and at a time in the return window; ★★ echoReadings_eq_labels — taken at the completions of the two writes, the radar timestamps are T times the clock labels of A's two record events;
echoRadarBudget — T + senderWindow + emitEnd + |echoReturnDelay| + 2 transferError: clock resolution (derived), the retention window (input: each reading is taken while its record displays), the two detector responses (derived), the two transfers (derived); ★★ abs_echoReadings_emit_sub_le, abs_echoReadings_ret_sub_le;
★★★ radar_from_sender_records — one bound on radar time, separation and distance against the ideal round-trip readings (0, 2τ_hop), both records displayed at their reading times, the ideal separation being τ_hop: a radar separation read entirely at one station.

Honest scope #

The emission timestamp is late by the emission write's completion: the pointer at A reaches its first arc only after the carrier has left. This is a detector response, derived, and it enters the budget as emitEnd.
The clock is still #185's scheduled device; the internally driven clock is #201, and the two on one arena is #202.
No universal c, no Lorentz invariance. c₀ is a calibration constant, the hop time is the exchange's own, the arena has no metric. The #187 and #190 headers stand.
The input bounds are the two retention windows and the clock horizon (t ≤ K T).

References: specs/BACKLOG.md #200, #199, #197, #187, #185, #39; RecordLayer/EchoArena.lean, RecordLayer/RadarDetector.lean (transferError, abs_detunedHopTime_sub_hopTime_le), CV/RadarCoordinates.lean (RadarReadings, ofDuration, radarSep_roundTrip, abs_radarTime_sub_le), RecordLayer/RecordClock.lean (tickReading, abs_tickReading_sub_lt, tickCount_mono), RecordLayer/CoupledReception.lean (the clocked-arena pattern).

Round-trip radar from the sender's records #

Honest scope #

Both transfers #

The echo arena with the record clock #

A's two writes on the clocked arena #

The readings, the budget and the bound #

`A`'s two writes on the clocked arena #