Coupled reception: the activated write against the uncoupled transfer

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

#183 transferred the excitation exactly and read it by a schedule; #194 let the receiver's own pointer be set in motion by the arriving carrier, at the price of a detuning Δ = g f(θ₂) on the carrier. This module is the compatibility theorem between the two: how far the coupled reception is from the uncoupled one, when the receiver still tells the two messages apart, when the write forms, and where its event sits in the causal order of the hop graph.

• detuned_readout_one_zero_detuning — at Δ = 0 the coupled occupancy is the uncoupled sin²(Jt/ħ) of #183: the detuned law contains the exact transfer;
• abs_sin_sq_sub_sin_sq_le, rabiFreq_sub_le, ★★ occupancy_loss_le — the loss is continuous, quadratic in the detuning: |n_B^Δ(t) − n_B^0(t)| ≤ (1/(4J²) + |t|/(8Jħ)) Δ², hence ≤ C |Δ| for |Δ| ≤ 1 (occupancy_loss_le_of_abs_le_one); the two pieces are the peak loss (Δ/2)²/Ω² and the phase drift |Ω − J| |t|/ħ;
• ★★ readBit_detuned_one, readBit_detuned_zero, ★★ receiver_bit_distinguishes — the receiver's thresholded bit of #186 still distinguishes the two preparations at the detuned hop time whenever |Δ| ≤ 2J, i.e. whenever the peak loss stays at or below the threshold 1/2;
• ★ formation_interval — the formation interval of the write from the occupancy integral and the preparation: the write of #194 is an IsRecordWrite with interval [1/(6κ), 2/(3κ) + 1/(2ω)], and the lifted displacement is pinched between 0 and κ t; retention per #194 (message_one_returns);
• ClockedArena, clockedEvolve — the arena of #194 with the record clock of #185: a two-time, measure-preserving dynamics (clockedEvolve_comp, clockedEvolve_measurePreserving); ★★ clockedRegister — the activated write registered on it as an ActualOccurrence (#191); clockedReading, emissionEvent, ★★ emission_causalPrecedes_reception — the occurrence's event, labelled by the arena clock, is causally preceded on the hop graph by the emission, as soon as the clock has ticked once before the write completes; receptionEvent_time_le bounds the label by the periods elapsed;
• ★★★ coupled_reception — the package.

Honest scope

• The clock is #185's: a scheduled device, a modelling input indexed by t_Σ, exactly as there. What is internal is the activation of the write; the labelling of its event by the clock is a reading of a second device in the arena, not a second internal activation.
• The loss bound is stated for message 1 from the vacuum at B; the hypotheses 0 < J, 0 < ħ are those of #183. Nothing is claimed about a universal rate or a metric; the event order is CausalPrecedes on the assumed hop graph, permitted influence, as in #186.

References: specs/BACKLOG.md #196, #194, #195, #186, #185, #183, #39; CV/DetunedExchange.lean (detuned_readout_one, detuned_readout_one_peak, one_sub_div_rabiFreq_sq), CV/SignalExchange.lean (receiver_readout_one), RecordLayer/ActivatedWrite.lean (activatedRegister, message_one_returns), RecordLayer/RecordedExchange.lean (readBit, hopGraph, causal_chain), RecordLayer/RecordClock.lean (tickCount_ge, tickCount_le), CV/RecordCausalOrder.lean.

Compatibility with the uncoupled transfer

theorem CSD.RecordLayer.detuned_readout_one_zero_detuning {J : ℝ} (hJ : 0 < J) (ħ t : ℝ) : CV.arenaObs CV.occB ((CV.detunedFlow J ħ 0).arenaFlow t (CV.msgPoint 1)) = Real.sin (CV.hopAngle J ħ t) ^ 2

At zero detuning the coupled occupancy is the uncoupled one of #183.

theorem CSD.RecordLayer.abs_sin_sq_sub_sin_sq_le (a b : ℝ) : |Real.sin a ^ 2 - Real.sin b ^ 2| ≤ |a - b|

sin² is 1-Lipschitz.

theorem CSD.RecordLayer.rabiFreq_sub_le {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : CV.rabiFreq J Δ - J ≤ Δ ^ 2 / (8 * J)

The Rabi energy exceeds J by at most Δ²/(8J).

theorem CSD.RecordLayer.one_sub_div_rabiFreq_sq_le {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : 1 - (J / CV.rabiFreq J Δ) ^ 2 ≤ Δ ^ 2 / (4 * J ^ 2)

The peak loss is at most Δ²/(4J²).

theorem CSD.RecordLayer.abs_rabiAngle_sub_hopAngle_le {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ t : ℝ) : |CV.rabiAngle J ħ Δ t - CV.hopAngle J ħ t| ≤ |t| * Δ ^ 2 / (8 * J * ħ)

The phase drift: |Ωt/ħ − Jt/ħ| ≤ |t| Δ²/(8Jħ).

theorem CSD.RecordLayer.occupancy_loss_le {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ t : ℝ) : |CV.arenaObs CV.occB ((CV.detunedFlow J ħ Δ).arenaFlow t (CV.msgPoint 1)) - CV.arenaObs CV.occB ((CV.hopFlow J ħ).arenaFlow t (CV.msgPoint 1))| ≤ (1 / (4 * J ^ 2) + |t| / (8 * J * ħ)) * Δ ^ 2

★★ The loss of coupled reception is continuous in the detuning, quadratically: the occupancy of B for message 1 under detuning Δ differs from the uncoupled occupancy by at most (1/(4J²) + |t|/(8Jħ)) Δ².

theorem CSD.RecordLayer.occupancy_loss_le_of_abs_le_one {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {Δ : ℝ} (hΔ : |Δ| ≤ 1) (t : ℝ) : |CV.arenaObs CV.occB ((CV.detunedFlow J ħ Δ).arenaFlow t (CV.msgPoint 1)) - CV.arenaObs CV.occB ((CV.hopFlow J ħ).arenaFlow t (CV.msgPoint 1))| ≤ (1 / (4 * J ^ 2) + |t| / (8 * J * ħ)) * |Δ|

The row's form: for |Δ| ≤ 1 the loss is at most C |Δ|.

The receiver's thresholded bit still distinguishes the messages

theorem CSD.RecordLayer.half_le_div_rabiFreq_sq {J Δ : ℝ} (hJ : 0 < J) (hΔ : |Δ| ≤ 2 * J) : 1 / 2 ≤ (J / CV.rabiFreq J Δ) ^ 2

Under |Δ| ≤ 2J the peak occupancy is at least the threshold 1/2.

theorem CSD.RecordLayer.readBit_detuned_one {J ħ Δ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hΔ : |Δ| ≤ 2 * J) : readBit CV.excB ((CV.detunedFlow J ħ Δ).arenaFlow (CV.detunedHopTime J ħ Δ) (CV.msgPoint 1)) = 1

★★ The receiver's bit reads 1 for message 1 at the detuned hop time whenever |Δ| ≤ 2J.

theorem CSD.RecordLayer.readBit_detuned_zero {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : readBit CV.excB ((CV.detunedFlow J ħ Δ).arenaFlow t (CV.msgPoint 0)) = 0

The receiver's bit reads 0 for message 0, at every time and every detuning.

theorem CSD.RecordLayer.receiver_bit_distinguishes {J ħ Δ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hΔ : |Δ| ≤ 2 * J) : readBit CV.excB ((CV.detunedFlow J ħ Δ).arenaFlow (CV.detunedHopTime J ħ Δ) (CV.msgPoint 1)) ≠ readBit CV.excB ((CV.detunedFlow J ħ Δ).arenaFlow (CV.detunedHopTime J ħ Δ) (CV.msgPoint 0))

★★ The thresholded reception bit distinguishes the two messages under detuning whenever the peak loss stays below the threshold: |Δ| ≤ 2J.

The formation interval of the write

theorem CSD.RecordLayer.formation_interval {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) : IsRecordWrite (fun (t : ℝ) => displayed (activeEvolve J ħ g hf 0 t (CV.msgPoint 1, q))) 0 (writeStart (driftRate J ħ g hf q.2)) (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))) true ∧ ∀ (t : ℝ), 0 ≤ t → 0 ≤ pointerAmount J ħ g hf t (CV.msgPoint 1, q) ∧ pointerAmount J ħ g hf t (CV.msgPoint 1, q) ≤ driftRate J ħ g hf q.2 * t

★ The formation interval from the occupancy integral and the preparation: the write of #194 is an IsRecordWrite on [1/(6κ), 2/(3κ) + 1/(2ω)], and the lifted displacement from the occupancy integral is pinched between 0 and κ t.

The arena with the record clock, and the event order

@[reducible, inline]

abbrev CSD.RecordLayer.ClockedArena (K : ℕ) : Type

The arena of the activated write with the record clock of #185.

Equations

• CSD.RecordLayer.ClockedArena K = (CSD.RecordLayer.ActiveArena × CSD.RecordLayer.ClockArena K)

noncomputable def CSD.RecordLayer.clockedEvolve {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (T : ℝ) (s t : SigmaLayer.OnticTime) : ClockedArena K → ClockedArena K

The joint two-time propagator: the activated dynamics and the clock.

Equations

• CSD.RecordLayer.clockedEvolve J ħ g hf T s t = Prod.map (CSD.RecordLayer.activeEvolve J ħ g hf s t) (CSD.RecordLayer.clockEvolve T s t)

theorem CSD.RecordLayer.clockedEvolve_self {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (T : ℝ) (t : SigmaLayer.OnticTime) : clockedEvolve J ħ g hf T t t = id

theorem CSD.RecordLayer.clockedEvolve_comp {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (T : ℝ) (s t u : SigmaLayer.OnticTime) : clockedEvolve J ħ g hf T t u ∘ clockedEvolve J ħ g hf T s t = clockedEvolve J ħ g hf T s u

The two-time law on the clocked arena.

theorem CSD.RecordLayer.measurable_clockedEvolve {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) (T : ℝ) (s t : SigmaLayer.OnticTime) : Measurable (clockedEvolve J ħ g hf T s t)

theorem CSD.RecordLayer.clockedEvolve_measurePreserving {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) (T : ℝ) (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena 2 2) : MeasureTheory.MeasurePreserving (clockedEvolve J ħ g hf T s t) (((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume).prod MeasureTheory.volume) (((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume).prod MeasureTheory.volume)

Liouville on the clocked arena.

noncomputable def CSD.RecordLayer.clockedRegister {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) {c : ClockArena K} (hc : c ∈ ClockReady K) (T : ℝ) : ActualOccurrence (ClockedArena K) Bool 2

★★ The activated write registered on the clocked arena (#191), the clock ready alongside the pointer.

Equations

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

noncomputable def CSD.RecordLayer.clockedReading {K : ℕ} (x : ClockedArena K) : ℕ

The arena clock's reading.

Equations

• CSD.RecordLayer.clockedReading x = CSD.RecordLayer.tickCount x.2

def CSD.RecordLayer.emissionEvent : CV.RecordEvent 2

The emission event: the message at A, period 0.

Equations

• CSD.RecordLayer.emissionEvent = { region := {0}, time := 0 }

theorem CSD.RecordLayer.receptionEvent_region {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) {c : ClockArena K} (hc : c ∈ ClockReady K) (T : ℝ) : ((clockedRegister J ħ g hf hJ hħ hf1 hq hκ hslow hc T).toRecordEvent clockedReading).region = {1}

theorem CSD.RecordLayer.receptionEvent_time {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) {c : ClockArena K} (hc : c ∈ ClockReady K) (T : ℝ) : ((clockedRegister J ħ g hf hJ hħ hf1 hq hκ hslow hc T).toRecordEvent clockedReading).time = tickCount (clockEvolve T 0 (writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2))) c)

The reception event's period is the clock's tick count at the completion of the write.

theorem CSD.RecordLayer.receptionEvent_time_le {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) {c : ClockArena K} (hc : c ∈ ClockReady K) {T : ℝ} (hT : 0 < T) {n : ℕ} (hn : writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) ≤ ↑n * T) : ((clockedRegister J ħ g hf hJ hħ hf1 hq hκ hslow hc T).toRecordEvent clockedReading).time ≤ n

The label is at most the number of periods elapsed at the completion of the write.

theorem CSD.RecordLayer.emission_causalPrecedes_reception {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) (hK : 0 < K) {c : ClockArena K} (hc : c ∈ ClockReady K) {T : ℝ} (hT : 0 < T) (hone : T ≤ writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2))) : CV.CausalPrecedes hopGraph emissionEvent ((clockedRegister J ħ g hf hJ hħ hf1 hq hκ hslow hc T).toRecordEvent clockedReading)

★★ The emission causally precedes the reception on the hop graph, as soon as the clock has ticked once before the write completes (T ≤ writeEnd).

The package

theorem CSD.RecordLayer.coupled_reception {K : ℕ} {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) (hK : 0 < K) {c : ClockArena K} (hc : c ∈ ClockReady K) {T : ℝ} (hT : 0 < T) (hone : T ≤ writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2))) : (∀ (Δ t : ℝ), CV.arenaObs CV.occB ((CV.detunedFlow J ħ Δ).arenaFlow t (CV.msgPoint 1)) = (J / CV.rabiFreq J Δ) ^ 2 * Real.sin (CV.rabiAngle J ħ Δ t) ^ 2) ∧ (∀ (t : ℝ), CV.arenaObs CV.occB ((CV.detunedFlow J ħ 0).arenaFlow t (CV.msgPoint 1)) = Real.sin (CV.hopAngle J ħ t) ^ 2) ∧ (∀ (Δ t : ℝ), |CV.arenaObs CV.occB ((CV.detunedFlow J ħ Δ).arenaFlow t (CV.msgPoint 1)) - CV.arenaObs CV.occB ((CV.hopFlow J ħ).arenaFlow t (CV.msgPoint 1))| ≤ (1 / (4 * J ^ 2) + |t| / (8 * J * ħ)) * Δ ^ 2) ∧ (∀ (Δ : ℝ), |Δ| ≤ 2 * J → readBit CV.excB ((CV.detunedFlow J ħ Δ).arenaFlow (CV.detunedHopTime J ħ Δ) (CV.msgPoint 1)) ≠ readBit CV.excB ((CV.detunedFlow J ħ Δ).arenaFlow (CV.detunedHopTime J ħ Δ) (CV.msgPoint 0))) ∧ IsRecordWrite (fun (t : ℝ) => displayed (activeEvolve J ħ g hf 0 t (CV.msgPoint 1, q))) 0 (writeStart (driftRate J ħ g hf q.2)) (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))) true ∧ (∃ (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)) < t ∧ (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 = q) ∧ CV.CausalPrecedes hopGraph emissionEvent ((clockedRegister J ħ g hf hJ hħ hf1 hq hκ hslow hc T).toRecordEvent clockedReading)

★★★ Coupled reception. The occupancy of B under the detuning Δ is the detuned Rabi law, exact transfer at Δ = 0, with a loss quadratic in Δ; the receiver's thresholded bit distinguishes the two messages whenever |Δ| ≤ 2J; the write of #194 forms on its explicit interval with the displacement pinched by the occupancy integral; the retention is finite; and the occurrence's event, labelled by the arena clock, is causally preceded by the emission on the hop graph once the clock has ticked.