Radar with a detector: the activated reception read as a radar coordinate

Category: 7-SigmaLayer (the record layer). BACKLOG #197 (out of #39; the last row of the author's second operational-geometry brief, #191–#197; the brief's §7).

#187 read radar coordinates off a clock whose registers were written by a schedule. Here the reception is #196's: the detector at B is set in motion by the arriving carrier and completes its write over an interval, so the reading at the detection is later than the arrival by a detector delay, and the carrier it reads arrived under the detuning its own back-reaction imposed. Every contribution to the radar error is derived for this witness; the two input bounds are labelled.

• transferError, ★ abs_detunedHopTime_sub_hopTime_le — the transfer error: the detuned arrival πħ/(2Ω) differs from #183's τ_hop = πħ/(2J) by at most πħ Δ²/(16 J³);
• detectorDelay — the detector delay of the witness, the completion of the write minus the detuned arrival, 2/(3κ) + 1/(2ω) − π/(2ω), explicit in the preparation's κ and ω;
• detectorReadings, detectorReadings_emit, ★★ abs_detectorReadings_ret_sub_le — the measured readings are the arena clock at the emission (0, exactly) and at a reading time inside the retention window; the return reading is within T + retention + |detectorDelay| + transferError of τ_hop: clock resolution (abs_tickReading_sub_lt, derived), the retention window (input bound: the reading is taken while the record displays), the detector delay (derived), the transfer error (derived);
• ★★★ radar_with_detector — one bound on radar time, separation and distance through abs_radarTime_sub_le / abs_radarSep_sub_le / abs_radarDist_sub_le against the ideal one-way readings (0, τ_hop), with the record displayed at the reading time;
• ★ radarTime_delayed, radarSep_delayed — the interpretation: a detector with response time d shifts both radar coordinates by d/2; the shift is a property of the detector, read off the coordinates, not of the signal.

Honest scope

• One clock, at A, and a one-way flight. The "return" reading is the detection, so the radar separation is half the time of flight plus half the detector delay. Nothing here is an echo; the echo witness is #187's and stands.
• No universal c, no Lorentz invariance. c₀ is a calibration constant (radarDist), the hop time is the exchange's own, and the arena has no metric. The #187 and #190 headers stand.
• The input bounds are the retention window (the reading is taken while the record displays) and the clock horizon (t ≤ K T); everything else is derived from the witness.

References: specs/BACKLOG.md #197, #196, #194, #187, #189, #185, #183, #39; CV/RadarCoordinates.lean (RadarReadings, abs_radarTime_sub_le, abs_radarSep_sub_le, abs_radarDist_sub_le, ofDuration), RecordLayer/RecordClock.lean (abs_tickReading_sub_lt, tickCount_mono, tickCount_at_period), RecordLayer/CoupledReception.lean (rabiFreq_sub_le), RecordLayer/ActivatedWrite.lean (writeEnd, retention, message_one_displayed), CV/DetunedExchange.lean (detunedHopTime).

The transfer error

noncomputable def CSD.RecordLayer.transferError (J ħ Δ : ℝ) : ℝ

The transfer error of the detuned arrival: πħ Δ²/(16 J³).

Equations

• CSD.RecordLayer.transferError J ħ Δ = Real.pi * ħ * Δ ^ 2 / (16 * J ^ 3)

theorem CSD.RecordLayer.transferError_nonneg {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : 0 ≤ transferError J ħ Δ

theorem CSD.RecordLayer.abs_detunedHopTime_sub_hopTime_le {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : |CV.detunedHopTime J ħ Δ - CV.hopTime J ħ| ≤ transferError J ħ Δ

★ The transfer error: the detuned arrival πħ/(2Ω) is within πħ Δ²/(16 J³) of #183's τ_hop = πħ/(2J).

The interpretation: a detector delay shifts both coordinates by half of itself

theorem CSD.RecordLayer.radarTime_delayed (τ : ℝ) {a d : ℝ} (ha : 0 ≤ a) (hd : 0 ≤ d) : (CV.RadarReadings.ofDuration τ (a + d) ⋯).radarTime = (CV.RadarReadings.ofDuration τ a ha).radarTime + d / 2

One-way readings with the detection delayed by d.

theorem CSD.RecordLayer.radarSep_delayed (τ : ℝ) {a d : ℝ} (ha : 0 ≤ a) (hd : 0 ≤ d) : (CV.RadarReadings.ofDuration τ (a + d) ⋯).radarSep = (CV.RadarReadings.ofDuration τ a ha).radarSep + d / 2

★ A detector of response time d shifts the radar separation by d/2: the shift is a property of the detector, and it is read off the coordinate.

The witness: the activated reception read on the arena clock

noncomputable def CSD.RecordLayer.detectorDelay {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) : ℝ

The detector delay of the witness: the completion of the write minus the detuned arrival, 2/(3κ) + 1/(2ω) − π/(2ω).

Equations

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

theorem CSD.RecordLayer.detectorDelay_eq {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (φ : AddCircle 1) : detectorDelay J ħ g hf φ = 2 / (3 * driftRate J ħ g hf φ) + 1 / (2 * CV.rabiRate J ħ (detuningAt g hf φ)) - Real.pi / (2 * CV.rabiRate J ħ (detuningAt g hf φ))

noncomputable def CSD.RecordLayer.detectorReadings {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {c : ClockArena K} (hc : c ∈ ClockReady K) {t : ℝ} (ht : 0 ≤ t) : CV.RadarReadings

The measured readings: the arena clock at the emission (time 0) and at the reading time t. 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.detectorReadings_emit {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {c : ClockArena K} (hc : c ∈ ClockReady K) {t : ℝ} (ht : 0 ≤ t) : (detectorReadings hK hT hc ht).emit = 0

The emission reading is exactly 0: a ready clock has not ticked at the switch-on.

theorem CSD.RecordLayer.detectorReadings_ret {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) {c : ClockArena K} (hc : c ∈ ClockReady K) {t : ℝ} (ht : 0 ≤ t) : (detectorReadings hK hT hc ht).ret = tickReading T (clockEvolve T 0 t c)

noncomputable def CSD.RecordLayer.idealReadings {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : CV.RadarReadings

The ideal one-way readings: emission at 0, arrival at #183's τ_hop.

Equations

• CSD.RecordLayer.idealReadings hJ hħ = CSD.CV.RadarReadings.ofDuration 0 (CSD.CV.hopTime J ħ) ⋯

theorem CSD.RecordLayer.idealReadings_emit {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (idealReadings hJ hħ).emit = 0

theorem CSD.RecordLayer.idealReadings_ret {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (idealReadings hJ hħ).ret = CV.hopTime J ħ

noncomputable def CSD.RecordLayer.radarBudget {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) (T : ℝ) : ℝ

The total error budget of the witness.

Equations

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

theorem CSD.RecordLayer.abs_detectorReadings_ret_sub_le {K : ℕ} {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hK : 0 < K) {T : ℝ} (hT : 0 < T) {c : ClockArena K} (hc : c ∈ ClockReady K) {q : LF4.KTorus} {t : ℝ} (ht : 0 ≤ t) (htK : t ≤ ↑K * T) (hdet : writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) ≤ t ∧ t ≤ writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) + retention (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2))) : |(detectorReadings hK hT hc ht).ret - CV.hopTime J ħ| ≤ radarBudget J ħ g hf q.2 T

★★ The return reading is within the budget of τ_hop. Clock resolution (derived), the retention window (input: the reading is taken while the record displays), the detector delay (derived), the transfer error (derived).

theorem CSD.RecordLayer.radar_with_detector {K : ℕ} {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hK : 0 < K) {T : ℝ} (hT : 0 < T) {c : ClockArena K} (hc : c ∈ ClockReady K) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) {t : ℝ} (ht : 0 ≤ t) (htK : t ≤ ↑K * T) (hdet : writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) ≤ t ∧ t ≤ writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) + retention (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2))) {c₀ : ℝ} (hc₀ : 0 ≤ c₀) : (detectorReadings hK hT hc ht).emit = 0 ∧ (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 ∈ displayArc ∧ |(detectorReadings hK hT hc ht).radarTime - (idealReadings hJ hħ).radarTime| ≤ radarBudget J ħ g hf q.2 T ∧ |(detectorReadings hK hT hc ht).radarSep - (idealReadings hJ hħ).radarSep| ≤ radarBudget J ħ g hf q.2 T ∧ |(detectorReadings hK hT hc ht).radarDist c₀ - (idealReadings hJ hħ).radarDist c₀| ≤ c₀ * radarBudget J ħ g hf q.2 T

★★★ Radar with a detector. Against the ideal one-way readings (0, τ_hop), the measured radar time, separation and distance are within the budget T + retention + |detectorDelay| + transferError (times c₀ for the distance), the emission reading is exactly 0, and the record displays at the reading time.