Failure of the exchange, and the retention window

Category: 7-SigmaLayer (the record layer — robustness of the clock-and-echo capstone). BACKLOG #189 (out of #39; the seventh of #183–#189).

#184 bounded the deterministic timing error. This file bounds the probability that the complete exchange is invalid — some record failing to display the message — and states the retention condition under which the records are all alive when the coordinates are read.

Failure. The exchange is valid for message b when all three registers display b at their readout times. A register fails only if it was not ready or the exchange state it read did not carry the message: recordFailure ⊆ notReady ∪ messageFailure (★ recordFailure_subset_union), because a ready register reading b is written with b (register_at_readout). Hence, for any preparation measure, by the union bound over the three writes — no independence is proved and none is used —

μ {invalid} ≤ Σ_i μ (recordFailure i) ≤ Σ_i (μ (notReady i) + μ (messageFailure i))

(★★ measure_invalid_le, measure_invalid_le'), and for a probability measure μ {valid} ≥ 1 − Σ_i μ (recordFailure i) (prob_valid_ge). The exact witness never fails (exchangeValid_xPrep). The quantitative input for a register prepared off the ready arc is the band bound of #103 — the Haar measure of a rep-band is at most its width (volume_band_le, consuming volume_rep_preimage_Ioc_le) — and the write has no tolerance: a register just past the ready arc misses the pointer arc by exactly its excess (★ pshift_shearAmt_notMem_pointerArc). That is a finding about the arc mechanism of ShearWitness.lean, not a defect of this file.

Retention. A record lifetime τ_R ≥ 2 τ_hop is sufficient: every record is alive at the return readout, where the radar coordinates are formed (★★ retention_sufficient, records_at_return), through the corpus's record_persists_on_interval. Here it is also exact: after its readout a register is frozen (register_frozen), so the window is unbounded.

Honest scope

• ⚠️ carrier_persistence_window (CV/CarrierPersistence.lean) is not consumed: it bounds the drift of a field-mode readout under a periodic unitary perturbation, and this arena's records are torus arcs with no perturbation model. Where a perturbed carrier is the record, that theorem is the quantitative retention statement; here retention is exact and needs no rate.
• The failure bound is a union bound. Independence of the three writes is neither claimed nor needed, and a product bound would require a product preparation measure, which is not assumed.
• messageFailure is the exchange state at a readout time not reading the message. For the exact message point it is empty; for a perturbed exchange state its measure is the input, not an output.

References: specs/BACKLOG.md #189, #184, #186, #187, #39; RecordLayer/RecordedExchange.lean, RecordLayer/MacrostateStability.lean (volume_rep_preimage_Ioc_le, #103), RecordLayer/RecordPersistence.lean, CV/CarrierPersistence.lean.

Validity and the failure events

def CSD.RecordLayer.ExchangeValid {K : ℕ} (J ħ T : ℝ) (b : Fin 2) (x : XArena K) : Prop

The exchange is valid for message b: all three registers display b at their readout times.

Equations

• CSD.RecordLayer.ExchangeValid J ħ T b x = ∀ (i : Fin 3), (CSD.RecordLayer.xEvolve J ħ T (-1) (CSD.RecordLayer.readTime J ħ i) x).2.2 i ∈ CSD.RecordLayer.pointerArc 2 b

def CSD.RecordLayer.recordFailure {K : ℕ} (J ħ T : ℝ) (b : Fin 2) (i : Fin 3) : Set (XArena K)

Register i fails: it does not display b at its readout time.

Equations

• CSD.RecordLayer.recordFailure J ħ T b i = {x : CSD.RecordLayer.XArena K | (CSD.RecordLayer.xEvolve J ħ T (-1) (CSD.RecordLayer.readTime J ħ i) x).2.2 i ∉ CSD.RecordLayer.pointerArc 2 b}

def CSD.RecordLayer.notReady {K : ℕ} (i : Fin 3) : Set (XArena K)

Register i was not ready.

Equations

• CSD.RecordLayer.notReady i = {x : CSD.RecordLayer.XArena K | x.2.2 i ∉ CSD.RecordLayer.readyArc 2}

def CSD.RecordLayer.messageFailure {K : ℕ} (J ħ : ℝ) (b : Fin 2) (i : Fin 3) : Set (XArena K)

The exchange state register i reads does not carry the message.

Equations

• CSD.RecordLayer.messageFailure J ħ b i = {x : CSD.RecordLayer.XArena K | CSD.RecordLayer.readAt J ħ i (-1) x.1 ≠ b}

theorem CSD.RecordLayer.register_at_readout {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (x : XArena K) (i : Fin 3) : (xEvolve J ħ T (-1) (readTime J ħ i) x).2.2 i = pshift (shearAmt 2 (readAt J ħ i (-1) x.1)) (x.2.2 i)

At its readout time, register i is the ready register shifted by the bit it read.

theorem CSD.RecordLayer.recordFailure_subset_union {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) (i : Fin 3) : recordFailure J ħ T b i ⊆ notReady i ∪ messageFailure J ħ b i

★ A register fails only if it was not ready or read the wrong message.

theorem CSD.RecordLayer.not_exchangeValid_iff {K : ℕ} (J ħ T : ℝ) (b : Fin 2) (x : XArena K) : ¬ExchangeValid J ħ T b x ↔ ∃ (i : Fin 3), x ∈ recordFailure J ħ T b i

theorem CSD.RecordLayer.invalid_eq_iUnion {K : ℕ} (J ħ T : ℝ) (b : Fin 2) : {x : XArena K | ¬ExchangeValid J ħ T b x} = ⋃ (i : Fin 3), recordFailure J ħ T b i

theorem CSD.RecordLayer.measurableSet_recordFailure {K : ℕ} (J ħ T : ℝ) (b : Fin 2) (i : Fin 3) : MeasurableSet (recordFailure J ħ T b i)

theorem CSD.RecordLayer.measurableSet_invalid {K : ℕ} (J ħ T : ℝ) (b : Fin 2) : MeasurableSet {x : XArena K | ¬ExchangeValid J ħ T b x}

The union bound

theorem CSD.RecordLayer.measure_invalid_le {K : ℕ} (μ : MeasureTheory.Measure (XArena K)) (J ħ T : ℝ) (b : Fin 2) : μ {x : XArena K | ¬ExchangeValid J ħ T b x} ≤ ∑ i : Fin 3, μ (recordFailure J ħ T b i)

★★ The union bound over the three writes, for any preparation measure.

theorem CSD.RecordLayer.measure_invalid_le' {K : ℕ} (μ : MeasureTheory.Measure (XArena K)) {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) : μ {x : XArena K | ¬ExchangeValid J ħ T b x} ≤ ∑ i : Fin 3, (μ (notReady i) + μ (messageFailure J ħ b i))

The union bound with the two failure sources separated: not ready, or wrong message.

theorem CSD.RecordLayer.prob_valid_ge {K : ℕ} (μ : MeasureTheory.Measure (XArena K)) [MeasureTheory.IsProbabilityMeasure μ] (J ħ T : ℝ) (b : Fin 2) : 1 - ∑ i : Fin 3, μ (recordFailure J ħ T b i) ≤ μ {x : XArena K | ExchangeValid J ħ T b x}

For a probability measure, the exchange is valid with probability at least 1 − Σ_i μ (recordFailure i).

The exact witness never fails

theorem CSD.RecordLayer.exchangeValid_xPrep {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (c : ClockArena K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) : ExchangeValid J ħ T b (xPrep b c r)

Every ready register reading the message point is written: the exact preparation is valid.

theorem CSD.RecordLayer.dirac_invalid_eq_zero {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (c : ClockArena K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) : (MeasureTheory.Measure.dirac (xPrep b c r)) {x : XArena K | ¬ExchangeValid J ħ T b x} = 0

The invalid set misses every exact preparation: a Dirac preparation fails with probability 0.

The quantitative input: bands, and no tolerance

theorem CSD.RecordLayer.volume_band_le (a b : ℝ) : MeasureTheory.volume {q : LF4.KTorus | rep q.1 ∈ Set.Ioc a b} ≤ ENNReal.ofReal (b - a)

The band bound (#103, transported to the register torus): the Haar measure of the registers whose rep lies in (a, b] is at most b − a.

theorem CSD.RecordLayer.pshift_shearAmt_notMem_pointerArc {K' : ℕ} (i : Fin K') {q : LF4.KTorus} (hq : shearWidth K' < rep q.1) (hq' : rep q.1 + shearAmt K' i ≤ 1) : pshift (shearAmt K' i) q ∉ pointerArc K' i

★ The write has no tolerance: a register whose rep exceeds the ready width, shifted by the message's amount without wrapping, misses the pointer arc. The arcs of ShearWitness.lean are exactly as wide as the ready arc, so any preparation error past it is a record failure.

Retention

theorem CSD.RecordLayer.retention_sufficient {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {c : ClockArena K} {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) {τR : ℝ} (hτR : CV.roundTrip J ħ ≤ τR) (i : Fin 3) {t : SigmaLayer.OnticTime} (ht₁ : readTime J ħ i ≤ t) (ht₂ : t ≤ CV.roundTrip J ħ) : (xEvolve J ħ T (-1) t (xPrep b c r)).2.2 i ∈ pointerArc 2 b

★★ A record lifetime of at least the round trip is sufficient: every record is alive at every time from its readout to the return readout, where the radar coordinates are formed.

theorem CSD.RecordLayer.records_at_return {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {c : ClockArena K} {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) (i : Fin 3) : (xEvolve J ħ T (-1) (CV.roundTrip J ħ) (xPrep b c r)).2.2 i ∈ pointerArc 2 b

At the return readout all three records display the message: emission and return, the two readings the radar coordinates are formed from, and reception.

The package

theorem CSD.RecordLayer.exchange_failure {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {c : ClockArena K} {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) : (∀ (μ : MeasureTheory.Measure (XArena K)), μ {x : XArena K | ¬ExchangeValid J ħ T b x} ≤ ∑ i : Fin 3, (μ (notReady i) + μ (messageFailure J ħ b i))) ∧ ExchangeValid J ħ T b (xPrep b c r) ∧ (∀ (τR : ℝ), CV.roundTrip J ħ ≤ τR → ∀ (i : Fin 3) (t : SigmaLayer.OnticTime), readTime J ħ i ≤ t → t ≤ CV.roundTrip J ħ → (xEvolve J ħ T (-1) t (xPrep b c r)).2.2 i ∈ pointerArc 2 b) ∧ ∀ (i : Fin 2) (q : LF4.KTorus), shearWidth 2 < rep q.1 → rep q.1 + shearAmt 2 i ≤ 1 → pshift (shearAmt 2 i) q ∉ pointerArc 2 i

★★ Failure and retention. For any preparation measure the probability of an invalid exchange is at most the sum over the three writes of (not ready) + (wrong message); the exact preparation is valid; a record lifetime of at least the round trip keeps every record alive through the return readout; and the write mechanism tolerates no preparation error past the ready arc.