Radar coordinates from two clock readings, and their error bounds

Category: 3-Local (CV; the interface in which the clock-and-echo capstone states its conclusion). BACKLOG #184 (out of #39; the second of #183–#189).

A single radar exchange is a pair of clock readings at A: the emission reading τ₋ and the return reading τ₊, with τ₋ ≤ τ₊ as the domain of the assignment. From them

T_A = (τ₊ + τ₋) / 2, D_A = (τ₊ − τ₋) / 2, R_A = c₀ · D_A,

the radar time, the radar separation in time units, and the radar distance once a calibration constant c₀ > 0 converts time units to length units.

• RadarReadings — the two readings with their domain; radarTime, radarSep, radarDist;
• emit_le_radarTime, radarTime_le_ret, radarSep_nonneg, radarSep_eq_zero_iff — the elementary bounds;
• ★ radarTime_sub_radarSep, radarTime_add_radarSep, ext_of_radar — the readings and the coordinates determine each other: equal readings give equal coordinates (by congrArg), and equal coordinates give equal readings;
• ★ radarTime_shift, radarSep_shift, radarDist_shift — a clock-origin shift moves T_A and fixes D_A and R_A;
• ★ radarTime_rescale, radarSep_rescale, radarDist_rescale, radarDist_rescale_eq — a positive rescaling of the clock unit scales both coordinates, and the calibration constant absorbs it: unit λ with constant c₀ is unit 1 with constant c₀ λ;
• ★★ abs_radarTime_sub_le, abs_radarSep_sub_le, abs_radarDist_sub_le — bounded endpoint errors give bounded coordinate errors: |T̂ − T| ≤ δ, |D̂ − D| ≤ δ, |R̂ − R| ≤ c₀ δ;
• radarSep_eq_of_duration_eq — two exchanges of equal duration have equal separation; radarSep_roundTrip — an exchange lasting #183's round trip 2 τ_hop has separation τ_hop;
• ★★ radar_coordinates — the package.

Honest scope

• ⚠️ Algebra with a stated domain. Nothing here is a record: the readings are real numbers, not tick counts of a physical clock, and the association of the two readings with one exchange (which emission, which reflection) is part of the input. The record-level statement — that the readings are physical clock records of the constructed experiment and that the association is unambiguous — is #186's, and this module is honest only once #186 consumes it. It says so here.
• c₀ is a calibration constant and nothing in this file makes it a signal speed; radarDist_rescale_eq is exactly the statement that it absorbs the choice of time unit.
• Deterministic endpoint error only (|τ̂ − τ| ≤ δ); probabilistic failure of a write is #189.
• Zero processing delay at B; a reflection protocol with delay is a later extension of #186.
• radarSep_roundTrip is the arithmetic of #183's witness, not its record: it says what number a clock reading the hop exactly would produce.

References: specs/BACKLOG.md #184, #183, #186, #187, #39; specs/records-to-spacetime-scoping.md §4 (constants are constraints, not outputs); CV/SignalExchange.lean (hopTime, roundTrip).

Readings and coordinates

structure CSD.CV.RadarReadings : Type

One radar exchange as read at A: the emission reading τ₋ and the return reading τ₊, with τ₋ ≤ τ₊ as the domain of the assignment.

• emit : ℝ

  The clock reading at emission.

• ret : ℝ

  The clock reading at return.

• emit_le_ret : self.emit ≤ self.ret

  The domain: the return is read no earlier than the emission.

theorem CSD.CV.RadarReadings.ext {x y : RadarReadings} (emit : x.emit = y.emit) (ret : x.ret = y.ret) : x = y

theorem CSD.CV.RadarReadings.ext_iff {x y : RadarReadings} : x = y ↔ x.emit = y.emit ∧ x.ret = y.ret

noncomputable def CSD.CV.RadarReadings.radarTime (r : RadarReadings) : ℝ

The radar time T_A = (τ₊ + τ₋) / 2.

Equations

• r.radarTime = (r.ret + r.emit) / 2

noncomputable def CSD.CV.RadarReadings.radarSep (r : RadarReadings) : ℝ

The radar separation in time units, D_A = (τ₊ − τ₋) / 2.

Equations

• r.radarSep = (r.ret - r.emit) / 2

noncomputable def CSD.CV.RadarReadings.radarDist (r : RadarReadings) (c₀ : ℝ) : ℝ

The radar distance R_A = c₀ · D_A, with c₀ a calibration constant converting time units to length units.

Equations

• r.radarDist c₀ = c₀ * r.radarSep

Elementary bounds

theorem CSD.CV.RadarReadings.emit_le_radarTime (r : RadarReadings) : r.emit ≤ r.radarTime

theorem CSD.CV.RadarReadings.radarTime_le_ret (r : RadarReadings) : r.radarTime ≤ r.ret

theorem CSD.CV.RadarReadings.radarSep_nonneg (r : RadarReadings) : 0 ≤ r.radarSep

theorem CSD.CV.RadarReadings.radarSep_eq_zero_iff (r : RadarReadings) : r.radarSep = 0 ↔ r.emit = r.ret

theorem CSD.CV.RadarReadings.radarDist_nonneg (r : RadarReadings) {c₀ : ℝ} (hc : 0 ≤ c₀) : 0 ≤ r.radarDist c₀

The readings and the coordinates determine each other

theorem CSD.CV.RadarReadings.radarTime_sub_radarSep (r : RadarReadings) : r.radarTime - r.radarSep = r.emit

τ₋ = T_A − D_A.

theorem CSD.CV.RadarReadings.radarTime_add_radarSep (r : RadarReadings) : r.radarTime + r.radarSep = r.ret

τ₊ = T_A + D_A.

theorem CSD.CV.RadarReadings.ext_of_radar {r r' : RadarReadings} (hT : r.radarTime = r'.radarTime) (hD : r.radarSep = r'.radarSep) : r = r'

★ Equal coordinates give equal readings (the converse, equal readings give equal coordinates, is congrArg).

A clock-origin shift

def CSD.CV.RadarReadings.shift (r : RadarReadings) (s : ℝ) : RadarReadings

Shift the clock origin by s: both readings move by s.

Equations

• r.shift s = { emit := r.emit + s, ret := r.ret + s, emit_le_ret := ⋯ }

theorem CSD.CV.RadarReadings.radarTime_shift (r : RadarReadings) (s : ℝ) : (r.shift s).radarTime = r.radarTime + s

★ A clock-origin shift moves the radar time by the shift.

theorem CSD.CV.RadarReadings.radarSep_shift (r : RadarReadings) (s : ℝ) : (r.shift s).radarSep = r.radarSep

★ A clock-origin shift leaves the radar separation unchanged.

theorem CSD.CV.RadarReadings.radarDist_shift (r : RadarReadings) (c₀ s : ℝ) : (r.shift s).radarDist c₀ = r.radarDist c₀

A positive rescaling of the clock unit

def CSD.CV.RadarReadings.rescale (r : RadarReadings) (lam : ℝ) (hlam : 0 < lam) : RadarReadings

Rescale the clock unit by λ > 0: both readings are multiplied by λ.

Equations

• r.rescale lam hlam = { emit := lam * r.emit, ret := lam * r.ret, emit_le_ret := ⋯ }

theorem CSD.CV.RadarReadings.radarTime_rescale (r : RadarReadings) (lam : ℝ) (hlam : 0 < lam) : (r.rescale lam hlam).radarTime = lam * r.radarTime

theorem CSD.CV.RadarReadings.radarSep_rescale (r : RadarReadings) (lam : ℝ) (hlam : 0 < lam) : (r.rescale lam hlam).radarSep = lam * r.radarSep

theorem CSD.CV.RadarReadings.radarDist_rescale (r : RadarReadings) (c₀ lam : ℝ) (hlam : 0 < lam) : (r.rescale lam hlam).radarDist c₀ = lam * r.radarDist c₀

★ The coordinates transform consistently under a change of clock unit.

theorem CSD.CV.RadarReadings.radarDist_rescale_eq (r : RadarReadings) (c₀ lam : ℝ) (hlam : 0 < lam) : (r.rescale lam hlam).radarDist c₀ = r.radarDist (c₀ * lam)

The calibration constant absorbs the unit: clock unit λ with constant c₀ gives the same distance as clock unit 1 with constant c₀ λ. Nothing fixes c₀ on its own.

Bounded endpoint errors give bounded coordinate errors

theorem CSD.CV.RadarReadings.abs_radarTime_sub_le {r r' : RadarReadings} {δ : ℝ} (he : |r'.emit - r.emit| ≤ δ) (hr : |r'.ret - r.ret| ≤ δ) : |r'.radarTime - r.radarTime| ≤ δ

★★ |T̂_A − T_A| ≤ δ when each endpoint reading is off by at most δ.

theorem CSD.CV.RadarReadings.abs_radarSep_sub_le {r r' : RadarReadings} {δ : ℝ} (he : |r'.emit - r.emit| ≤ δ) (hr : |r'.ret - r.ret| ≤ δ) : |r'.radarSep - r.radarSep| ≤ δ

★★ |D̂_A − D_A| ≤ δ when each endpoint reading is off by at most δ.

theorem CSD.CV.RadarReadings.abs_radarDist_sub_le {r r' : RadarReadings} {δ c₀ : ℝ} (hc : 0 ≤ c₀) (he : |r'.emit - r.emit| ≤ δ) (hr : |r'.ret - r.ret| ≤ δ) : |r'.radarDist c₀ - r.radarDist c₀| ≤ c₀ * δ

★★ |R̂_A − R_A| ≤ c₀ δ for a fixed nonnegative calibration constant.

Reproducibility, and the arithmetic of #183's witness

theorem CSD.CV.RadarReadings.radarSep_eq_of_duration_eq {r r' : RadarReadings} (h : r.ret - r.emit = r'.ret - r'.emit) : r.radarSep = r'.radarSep

Two exchanges of equal duration have equal separation, whatever their emission readings.

def CSD.CV.RadarReadings.ofDuration (τ d : ℝ) (hd : 0 ≤ d) : RadarReadings

The readings of an exchange emitted at τ and lasting d ≥ 0.

Equations

• CSD.CV.RadarReadings.ofDuration τ d hd = { emit := τ, ret := τ + d, emit_le_ret := ⋯ }

theorem CSD.CV.RadarReadings.radarSep_ofDuration (τ d : ℝ) (hd : 0 ≤ d) : (ofDuration τ d hd).radarSep = d / 2

theorem CSD.CV.RadarReadings.radarSep_roundTrip {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (τ : ℝ) : (ofDuration τ (roundTrip J ħ) ⋯).radarSep = hopTime J ħ

The arithmetic of #183's witness: an exchange lasting the round trip 2 τ_hop has radar separation τ_hop, whatever the emission reading. This is what a clock reading the hop exactly would produce; that the readings are such records is #186.

The package

theorem CSD.CV.RadarReadings.radar_coordinates (r : RadarReadings) : (r.emit ≤ r.radarTime ∧ r.radarTime ≤ r.ret) ∧ 0 ≤ r.radarSep ∧ (r.radarTime - r.radarSep = r.emit ∧ r.radarTime + r.radarSep = r.ret) ∧ (∀ (s : ℝ), (r.shift s).radarTime = r.radarTime + s ∧ (r.shift s).radarSep = r.radarSep) ∧ (∀ (lam : ℝ) (hlam : 0 < lam), (r.rescale lam hlam).radarTime = lam * r.radarTime ∧ (r.rescale lam hlam).radarSep = lam * r.radarSep) ∧ ∀ (r' : RadarReadings) (δ c₀ : ℝ), 0 ≤ c₀ → |r'.emit - r.emit| ≤ δ → |r'.ret - r.ret| ≤ δ → |r'.radarTime - r.radarTime| ≤ δ ∧ |r'.radarSep - r.radarSep| ≤ δ ∧ |r'.radarDist c₀ - r.radarDist c₀| ≤ c₀ * δ

★★ Radar coordinates. On the domain τ₋ ≤ τ₊: τ₋ ≤ T_A ≤ τ₊, D_A ≥ 0; the readings are recovered from the coordinates; a clock-origin shift moves T_A by the shift and fixes D_A; a positive rescaling of the clock unit scales both; endpoint errors ≤ δ give coordinate errors ≤ δ and a distance error ≤ c₀ δ.