The two-site exchange with both sites detuned

Category: 3-Local (CV; the carrier side of BACKLOG #198, the autonomous echo).

In the echo of #199 both stations carry a pointer, so both sites of the exchange are detuned by their own back-reaction: the carrier's Hamiltonian is

H = J X + Δ_A n_A + Δ_B n_B = H(Δ_B − Δ_A) + Δ_A P,

with H(Δ) the detuned exchange of DetunedExchange.lean and P the one-excitation projector. P commutes with everything, so the flow is the detuned exchange in the difference times a phase on the one-excitation sector:

U(t) = e^{−iΔ_A t/ħ · P} · U_{Δ_B − Δ_A}(t).

The sector phase is invisible to every observable that preserves the sector and to the rays of the two messages, so the whole of #194's carrier algebra transfers to the two-site case with Δ = Δ_B − Δ_A, and nothing new happens beyond the difference. What is new in this file is the return: at the detuned round trip πħ/Ω' the carrier is back at A, as a ray, exactly.

• twoDetunedH, ★ twoDetunedH_eq — H = H(Δ_B − Δ_A) + Δ_A P; sectorGen, twoDetunedGen, twoDetunedGen_eq, twoDetunedGen_zero_left — at Δ_A = 0 it is the detuned exchange;
• ★ twoDetunedFlow J ħ Δ_A Δ_B : FieldStructuredFlow 2 2 — the two-site detuned exchange is a field-structured flow on the one edge; sectorPhase, sectorPhase_eq, sectorPhase_unitary, sectorPhase_commute; ★★ twoDetunedFlow_val_eq — the flow is the sector phase times the detuned exchange in the difference, by exp_add_of_commute;
• ★★ arenaObs_twoDetunedFlow — every observable commuting with P reads the same along both flows, at every arena point; occB_twoDetunedFlow, occA_twoDetunedFlow, arenaObs_oneExc_twoDetunedFlow (the sector is conserved);
• ★★ twoDetunedFlow_arenaFlow_msgPoint_one — on the ray of message 1 the two flows agree; twoDetunedFlow_msgPoint_zero — the vacuum is fixed;
• ★★ twoDetuned_readout_B_one, twoDetuned_readout_A_one — the occupancies for message 1 are (J/Ω')² sin²(Ω't/ħ) at B and 1 − (J/Ω')² sin²(Ω't/ħ) at A, Ω' = √(J² + (Δ_B − Δ_A)²/4); twoDetuned_readout_B_zero, twoDetuned_readout_A_zero — both vanish for message 0;
• detunedRoundTrip — πħ/Ω' = 2 × detunedHopTime; ★★★ detunedFlow_return, twoDetuned_return — at the detuned round trip the carrier is back at A as a ray, for the detuned exchange and for the two-site flow; twoDetuned_return_occA, twoDetuned_return_occB — with n_A = 1, n_B = 0 there;
• occHistA, occHistA_eq, continuous_occHistA_prod, occAccumA, occAccumA_eq, hasDerivAt_occAccumA — the occupancy history of A and its integral, in terms of the detuned exchange's occHist/occAccum, continuous jointly in the ray and both detunings — what the pointer at A in #199 integrates; continuous_twoDetunedFlow_prod.

Honest scope

• Nothing here is a record; the pointers that produce Δ_A, Δ_B and read the occupancies are #199's. This file is the carrier.
• Δ_A, Δ_B are real parameters; in #199 they are functions of conserved torus angles, so the flow at fixed angles is exactly this one.
• J > 0 is assumed where the closed form divides by Ω'; ħ > 0 where the round trip is computed.

References: specs/BACKLOG.md #198, #199, #194, #183; CV/DetunedExchange.lean (detunedH, detunedFlow, detunedFlow_val_eq, occHist, occAccum), CV/SignalExchange.lean (hopX, oneExc, occB, msgPoint), Mathlib/Analysis/Normed/Algebra/ExpUnique.lean (exp_smul_eq_cosh_sinh).

More of the algebra of P, n_A, n_B

theorem CSD.CV.oneExc_conjTranspose : oneExc.conjTranspose = oneExc

theorem CSD.CV.oneExc_mul_occB : oneExc * occB = occB

theorem CSD.CV.occB_mul_oneExc : occB * oneExc = occB

theorem CSD.CV.oneExc_mul_occA : oneExc * occA = occA

theorem CSD.CV.occA_mul_oneExc : occA * oneExc = occA

theorem CSD.CV.mul_oneExc_apply_excA (M : Matrix HopConfig HopConfig ℂ) (c : HopConfig) : (M * oneExc) c excA = M c excA

A matrix times P, read in the column of A: P fixes e_A.

theorem CSD.CV.mul_oneExc_apply_vacC (M : Matrix HopConfig HopConfig ℂ) (c : HopConfig) : (M * oneExc) c vacC = 0

A matrix times P, read in the vacuum column: P kills the vacuum.

theorem CSD.CV.oneExc_apply_excA_excA : oneExc excA excA = 1

theorem CSD.CV.oneExc_apply_ne_excA {c : HopConfig} (hc : c ≠ excA) : oneExc c excA = 0

theorem CSD.CV.commute_oneExc_detunedH (J Δ : ℝ) : Commute oneExc (detunedH J Δ)

theorem CSD.CV.commute_oneExc_detunedGen (J ħ Δ : ℝ) : Commute oneExc (detunedGen J ħ Δ)

theorem CSD.CV.oneExc_commute_detunedFlowVal (J ħ Δ t : ℝ) : oneExc * ↑((detunedFlow J ħ Δ).flow t) = ↑((detunedFlow J ħ Δ).flow t) * oneExc

P commutes with the detuned flow.

The Hamiltonian with both sites detuned

noncomputable def CSD.CV.twoDetunedH (J ΔA ΔB : ℝ) : Matrix HopConfig HopConfig ℂ

H = J X + Δ_A n_A + Δ_B n_B.

Equations

• CSD.CV.twoDetunedH J ΔA ΔB = ↑J • CSD.CV.hopX + ↑ΔA • CSD.CV.occA + ↑ΔB • CSD.CV.occB

theorem CSD.CV.twoDetunedH_conjTranspose (J ΔA ΔB : ℝ) : (twoDetunedH J ΔA ΔB).conjTranspose = twoDetunedH J ΔA ΔB

theorem CSD.CV.twoDetunedH_eq (J ΔA ΔB : ℝ) : twoDetunedH J ΔA ΔB = detunedH J (ΔB - ΔA) + ↑ΔA • oneExc

★ The two-site Hamiltonian is the detuned exchange in the difference plus a sector energy: H = H(Δ_B − Δ_A) + Δ_A P.

theorem CSD.CV.twoDetunedH_zero_left (J Δ : ℝ) : twoDetunedH J 0 Δ = detunedH J Δ

At Δ_A = 0 the two-site Hamiltonian is the detuned exchange.

noncomputable def CSD.CV.sectorGen (ħ ΔA : ℝ) : Matrix HopConfig HopConfig ℂ

The sector generator −(i Δ_A/ħ) P.

Equations

• CSD.CV.sectorGen ħ ΔA = -(Complex.I * ↑(ΔA / ħ)) • CSD.CV.oneExc

theorem CSD.CV.sectorGen_skew (ħ ΔA : ℝ) : (sectorGen ħ ΔA).conjTranspose = -sectorGen ħ ΔA

noncomputable def CSD.CV.twoDetunedGen (J ħ ΔA ΔB : ℝ) : Matrix HopConfig HopConfig ℂ

The Schrödinger generator −(i/ħ) H.

Equations

• CSD.CV.twoDetunedGen J ħ ΔA ΔB = -(Complex.I * ↑(1 / ħ)) • CSD.CV.twoDetunedH J ΔA ΔB

theorem CSD.CV.twoDetunedGen_skew (J ħ ΔA ΔB : ℝ) : (twoDetunedGen J ħ ΔA ΔB).conjTranspose = -twoDetunedGen J ħ ΔA ΔB

theorem CSD.CV.twoDetunedGen_eq (J ħ ΔA ΔB : ℝ) : twoDetunedGen J ħ ΔA ΔB = detunedGen J ħ (ΔB - ΔA) + sectorGen ħ ΔA

The generator splits as the detuned exchange's plus the sector generator.

theorem CSD.CV.twoDetunedGen_zero_left (J ħ Δ : ℝ) : twoDetunedGen J ħ 0 Δ = detunedGen J ħ Δ

At Δ_A = 0 the generator is the detuned exchange's.

theorem CSD.CV.commute_sectorGen_detunedGen (J ħ ΔA Δ : ℝ) : Commute (sectorGen ħ ΔA) (detunedGen J ħ Δ)

theorem CSD.CV.commute_oneExc_twoDetunedGen (J ħ ΔA ΔB : ℝ) : Commute oneExc (twoDetunedGen J ħ ΔA ΔB)

theorem CSD.CV.continuous_twoDetunedGen (J ħ : ℝ) : Continuous fun (x : ℝ × ℝ) => twoDetunedGen J ħ x.1 x.2

The flow

noncomputable def CSD.CV.twoDetunedFlow (J ħ ΔA ΔB : ℝ) : FieldStructuredFlow 2 2

★ The two-site detuned exchange as a field-structured flow: the one edge (A, B) carrying −(i/ħ)(J X + Δ_A n_A + Δ_B n_B).

Equations

• CSD.CV.twoDetunedFlow J ħ ΔA ΔB = { edges := {(0, 1)}, piece := fun (x : Fin 2 × Fin 2) => CSD.CV.twoDetunedGen J ħ ΔA ΔB, piece_supported := ⋯, gen_skew := ⋯ }

theorem CSD.CV.twoDetunedFlow_val (J ħ ΔA ΔB t : ℝ) : ↑((twoDetunedFlow J ħ ΔA ΔB).flow t) = NormedSpace.exp (t • twoDetunedGen J ħ ΔA ΔB)

theorem CSD.CV.twoDetunedFlow_isom (J ħ ΔA ΔB t : ℝ) : (↑((twoDetunedFlow J ħ ΔA ΔB).flow t)).conjTranspose * ↑((twoDetunedFlow J ħ ΔA ΔB).flow t) = 1

theorem CSD.CV.continuous_twoDetunedFlowVal_prod (J ħ : ℝ) : Continuous fun (x : (ℝ × ℝ) × ℝ) => ↑((twoDetunedFlow J ħ x.1.1 x.1.2).flow x.2)

The flow is continuous jointly in both detunings and the time.

theorem CSD.CV.continuous_twoDetunedFlow_prod (J ħ : ℝ) : Continuous fun (x : (ℝ × ℝ) × ℝ) => (twoDetunedFlow J ħ x.1.1 x.1.2).flow x.2

theorem CSD.CV.hasDerivAt_twoDetunedFlowVal (J ħ ΔA ΔB t : ℝ) : HasDerivAt (fun (t : ℝ) => ↑((twoDetunedFlow J ħ ΔA ΔB).flow t)) (twoDetunedGen J ħ ΔA ΔB * ↑((twoDetunedFlow J ħ ΔA ΔB).flow t)) t

The Schrödinger equation of the two-site flow.

The sector phase

noncomputable def CSD.CV.sectorPhase (ħ ΔA t : ℝ) : Matrix HopConfig HopConfig ℂ

The sector phase e^{−i Δ_A t/ħ · P}.

Equations

• CSD.CV.sectorPhase ħ ΔA t = NormedSpace.exp (t • CSD.CV.sectorGen ħ ΔA)

theorem CSD.CV.sectorPhase_eq (ħ ΔA t : ℝ) : sectorPhase ħ ΔA t = 1 + (Complex.exp (↑(-(ΔA * t / ħ)) * Complex.I) - 1) • oneExc

e^{c P} = 1 + (e^c − 1) P.

theorem CSD.CV.sectorPhase_unitary (ħ ΔA t : ℝ) : (sectorPhase ħ ΔA t).conjTranspose * sectorPhase ħ ΔA t = 1

The sector phase is unitary.

theorem CSD.CV.sectorPhase_commute (ħ ΔA t : ℝ) {A : Matrix HopConfig HopConfig ℂ} (hA : oneExc * A = A * oneExc) : sectorPhase ħ ΔA t * A = A * sectorPhase ħ ΔA t

The sector phase commutes with everything P commutes with.

theorem CSD.CV.sectorPhase_mul_apply_excA (ħ ΔA t : ℝ) {M : Matrix HopConfig HopConfig ℂ} (hM : oneExc * M = M * oneExc) (c : HopConfig) : (sectorPhase ħ ΔA t * M) c excA = Complex.exp (↑(-(ΔA * t / ħ)) * Complex.I) * M c excA

The sector phase is the scalar e^{−iΔ_A t/ħ} on the column of A of anything commuting with P.

theorem CSD.CV.sectorPhase_mul_apply_vacC (ħ ΔA t : ℝ) {M : Matrix HopConfig HopConfig ℂ} (hM : oneExc * M = M * oneExc) (c : HopConfig) : (sectorPhase ħ ΔA t * M) c vacC = M c vacC

The sector phase is the identity on the vacuum column.

theorem CSD.CV.twoDetunedFlow_val_eq (J ħ ΔA ΔB t : ℝ) : ↑((twoDetunedFlow J ħ ΔA ΔB).flow t) = sectorPhase ħ ΔA t * ↑((detunedFlow J ħ (ΔB - ΔA)).flow t)

★★ The two-site flow is the sector phase times the detuned exchange in the difference.

Observables and rays agree with the detuned exchange

theorem CSD.CV.arenaObs_twoDetunedFlow (J ħ ΔA ΔB : ℝ) {A : Matrix HopConfig HopConfig ℂ} (hA : oneExc * A = A * oneExc) (p : FieldArena 2 2) (t : ℝ) : arenaObs A ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t p) = arenaObs A ((detunedFlow J ħ (ΔB - ΔA)).arenaFlow t p)

★★ Every observable commuting with P reads the same along the two-site flow and the detuned exchange in the difference, at every arena point.

theorem CSD.CV.occB_twoDetunedFlow (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (t : ℝ) : arenaObs occB ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t p) = occHist J ħ (ΔB - ΔA) p t

The occupancy of B along the two-site flow is the detuned exchange's history.

theorem CSD.CV.occA_twoDetunedFlow (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (t : ℝ) : arenaObs occA ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t p) = arenaObs occA ((detunedFlow J ħ (ΔB - ΔA)).arenaFlow t p)

theorem CSD.CV.arenaObs_oneExc_eq (p : FieldArena 2 2) : arenaObs oneExc p = arenaObs occA p + arenaObs occB p

The one-excitation weight is the sum of the two occupancies.

theorem CSD.CV.arenaObs_oneExc_twoDetunedFlow (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (t : ℝ) : arenaObs oneExc ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t p) = arenaObs oneExc p

The one-excitation sector is conserved along the two-site flow.

theorem CSD.CV.twoDetunedFlow_arenaFlow_msgPoint_one (J ħ ΔA ΔB t : ℝ) : (twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 1) = (detunedFlow J ħ (ΔB - ΔA)).arenaFlow t (msgPoint 1)

★★ On the ray of message 1 the two-site flow is the detuned exchange in the difference.

theorem CSD.CV.twoDetunedFlow_apply_vacC {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB t : ℝ) (c : HopConfig) : ↑((twoDetunedFlow J ħ ΔA ΔB).flow t) c vacC = if c = vacC then 1 else 0

The vacuum column of the two-site flow is the vacuum.

theorem CSD.CV.twoDetunedFlow_msgPoint_zero {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB t : ℝ) : (twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 0) = msgPoint 0

The vacuum is fixed: message 0 never moves.

The readouts of the two messages

theorem CSD.CV.arenaObs_occA_msgPoint_one : arenaObs occA (msgPoint 1) = 1

theorem CSD.CV.arenaObs_occB_msgPoint_one : arenaObs occB (msgPoint 1) = 0

theorem CSD.CV.arenaObs_occA_msgPoint_zero : arenaObs occA (msgPoint 0) = 0

theorem CSD.CV.arenaObs_occB_msgPoint_zero : arenaObs occB (msgPoint 0) = 0

theorem CSD.CV.twoDetuned_readout_B_one {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB t : ℝ) : arenaObs occB ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 1)) = (J / rabiFreq J (ΔB - ΔA)) ^ 2 * Real.sin (rabiAngle J ħ (ΔB - ΔA) t) ^ 2

★★ The receiver's occupancy for message 1: (J/Ω')² sin²(Ω't/ħ) with Ω' = √(J² + (Δ_B − Δ_A)²/4).

theorem CSD.CV.twoDetuned_readout_A_one {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB t : ℝ) : arenaObs occA ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 1)) = 1 - (J / rabiFreq J (ΔB - ΔA)) ^ 2 * Real.sin (rabiAngle J ħ (ΔB - ΔA) t) ^ 2

★★ The sender's occupancy for message 1: 1 − (J/Ω')² sin²(Ω't/ħ).

theorem CSD.CV.twoDetuned_readout_B_zero {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB t : ℝ) : arenaObs occB ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 0)) = 0

theorem CSD.CV.twoDetuned_readout_A_zero {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB t : ℝ) : arenaObs occA ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 0)) = 0

The detuned round trip: the carrier returns to A

noncomputable def CSD.CV.detunedRoundTrip (J ħ Δ : ℝ) : ℝ

The detuned round trip πħ/Ω.

Equations

• CSD.CV.detunedRoundTrip J ħ Δ = Real.pi * ħ / CSD.CV.rabiFreq J Δ

theorem CSD.CV.detunedRoundTrip_eq (J ħ Δ : ℝ) : detunedRoundTrip J ħ Δ = 2 * detunedHopTime J ħ Δ

theorem CSD.CV.detunedRoundTrip_pos {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : 0 < detunedRoundTrip J ħ Δ

theorem CSD.CV.detunedRoundTrip_zero {J : ℝ} (hJ : 0 ≤ J) (ħ : ℝ) : detunedRoundTrip J ħ 0 = roundTrip J ħ

At zero detuning the detuned round trip is the round trip of #183.

theorem CSD.CV.rabiAngle_detunedRoundTrip {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : rabiAngle J ħ Δ (detunedRoundTrip J ħ Δ) = Real.pi

theorem CSD.CV.toEuclideanLin_detunedFlow_roundTrip {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : (Matrix.toEuclideanLin ↑((detunedFlow J ħ Δ).flow (detunedRoundTrip J ħ Δ))) (basisVec excA) = -Complex.exp (↑(-dynPhase ħ Δ (detunedRoundTrip J ħ Δ)) * Complex.I) • basisVec excA

At the detuned round trip the detuned flow acts on e_A as the scalar −e^{−iΔ πħ/(2Ωħ)}.

theorem CSD.CV.detunedFlow_return {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : (detunedFlow J ħ Δ).arenaFlow (detunedRoundTrip J ħ Δ) (msgPoint 1) = msgPoint 1

★★★ The return: at the detuned round trip the carrier is back at A, as a ray, exactly.

theorem CSD.CV.twoDetuned_return {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (ΔA ΔB : ℝ) : (twoDetunedFlow J ħ ΔA ΔB).arenaFlow (detunedRoundTrip J ħ (ΔB - ΔA)) (msgPoint 1) = msgPoint 1

★★★ The return of the two-site flow: at the detuned round trip in the difference, the carrier of message 1 is back at A as a ray.

theorem CSD.CV.twoDetuned_return_occA {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (ΔA ΔB : ℝ) : arenaObs occA ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow (detunedRoundTrip J ħ (ΔB - ΔA)) (msgPoint 1)) = 1

theorem CSD.CV.twoDetuned_return_occB {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (ΔA ΔB : ℝ) : arenaObs occB ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow (detunedRoundTrip J ħ (ΔB - ΔA)) (msgPoint 1)) = 0

theorem CSD.CV.twoDetuned_return_nsmul {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (ΔA ΔB : ℝ) (n : ℕ) : (twoDetunedFlow J ħ ΔA ΔB).arenaFlow (↑n * detunedRoundTrip J ħ (ΔB - ΔA)) (msgPoint 1) = msgPoint 1

The return repeats: every multiple of the detuned round trip returns the carrier.

The occupancy history of A

noncomputable def CSD.CV.occHistA (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s : ℝ) : ℝ

The sender's occupancy history along the two-site flow from p.

Equations

• CSD.CV.occHistA J ħ ΔA ΔB p s = CSD.CV.arenaObs CSD.CV.occA ((CSD.CV.twoDetunedFlow J ħ ΔA ΔB).arenaFlow s p)

theorem CSD.CV.occHistA_eq (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s : ℝ) : occHistA J ħ ΔA ΔB p s = arenaObs oneExc p - occHist J ħ (ΔB - ΔA) p s

The history of A is the conserved sector weight minus the history of B.

theorem CSD.CV.occHistA_nonneg (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s : ℝ) : 0 ≤ occHistA J ħ ΔA ΔB p s

theorem CSD.CV.occHistA_le_one (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s : ℝ) : occHistA J ħ ΔA ΔB p s ≤ 1

theorem CSD.CV.continuous_occHistA_prod (J ħ : ℝ) : Continuous (Function.uncurry fun (x : FieldArena 2 2 × ℝ × ℝ) (s : ℝ) => occHistA J ħ x.2.1 x.2.2 x.1 s)

The history of A is continuous jointly in the ray, both detunings and the time.

theorem CSD.CV.continuous_occHistA (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) : Continuous fun (s : ℝ) => occHistA J ħ ΔA ΔB p s

noncomputable def CSD.CV.occAccumA (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (t : ℝ) : ℝ

The accumulated occupancy of A ∫₀ᵗ n_A(p(s)) ds.

Equations

• CSD.CV.occAccumA J ħ ΔA ΔB p t = ∫ (s : ℝ) in 0..t, CSD.CV.occHistA J ħ ΔA ΔB p s

theorem CSD.CV.occAccumA_eq (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (t : ℝ) : occAccumA J ħ ΔA ΔB p t = t * arenaObs oneExc p - occAccum J ħ (ΔB - ΔA) p t

The accumulated occupancy of A is t × (sector weight) − (accumulated occupancy of B).

theorem CSD.CV.occAccumA_zero (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) : occAccumA J ħ ΔA ΔB p 0 = 0

theorem CSD.CV.hasDerivAt_occAccumA (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (t : ℝ) : HasDerivAt (fun (t : ℝ) => occAccumA J ħ ΔA ΔB p t) (occHistA J ħ ΔA ΔB p t) t

theorem CSD.CV.continuous_occAccumA_prod (J ħ t : ℝ) : Continuous fun (x : FieldArena 2 2 × ℝ × ℝ) => occAccumA J ħ x.2.1 x.2.2 x.1 t

The accumulated occupancy of A is continuous jointly in the ray and both detunings.

theorem Continuous.occAccumA {X : Type u_1} [TopologicalSpace X] {ΔA ΔB : X → ℝ} {p : X → CSD.CV.FieldArena 2 2} (hA : Continuous ΔA) (hB : Continuous ΔB) (hp : Continuous p) (J ħ t : ℝ) : Continuous fun (x : X) => CSD.CV.occAccumA J ħ (ΔA x) (ΔB x) (p x) t

The accumulated occupancy of A along continuous ray and detuning families, in the applied form (the uncurried statement is continuous_occAccumA_prod; unifying it against an expected type unfolds the arena and times out, so consumers take this form).

theorem Continuous.occAccum {X : Type u_1} [TopologicalSpace X] {Δ : X → ℝ} {p : X → CSD.CV.FieldArena 2 2} (hΔ : Continuous Δ) (hp : Continuous p) (J ħ t : ℝ) : Continuous fun (x : X) => CSD.CV.occAccum J ħ (Δ x) (p x) t

The accumulated occupancy of B along continuous ray and detuning families, in the applied form.

theorem CSD.CV.occHistA_msgPoint_one {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB s : ℝ) : occHistA J ħ ΔA ΔB (msgPoint 1) s = 1 - (J / rabiFreq J (ΔB - ΔA)) ^ 2 * Real.sin (rabiAngle J ħ (ΔB - ΔA) s) ^ 2

The history of A for message 1: 1 − (J/Ω')² sin²(Ω's/ħ).

theorem CSD.CV.occHistA_msgPoint_zero {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB s : ℝ) : occHistA J ħ ΔA ΔB (msgPoint 0) s = 0

theorem CSD.CV.occAccumA_msgPoint_one (J ħ ΔA ΔB t : ℝ) : occAccumA J ħ ΔA ΔB (msgPoint 1) t = t - occAccum J ħ (ΔB - ΔA) (msgPoint 1) t

The accumulated occupancy of A for message 1: t − (accumulated occupancy of B).

theorem CSD.CV.occAccumA_msgPoint_zero {J : ℝ} (hJ : 0 < J) (ħ ΔA ΔB t : ℝ) : occAccumA J ħ ΔA ΔB (msgPoint 0) t = 0

Group laws along the two-site flow, and the joint energy

theorem CSD.CV.occHistA_arenaFlow (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s u : ℝ) : occHistA J ħ ΔA ΔB ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow s p) u = occHistA J ħ ΔA ΔB p (u + s)

The history of A from the evolved ray is the shifted history.

theorem CSD.CV.occAccumA_add (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s t : ℝ) : occAccumA J ħ ΔA ΔB p (s + t) = occAccumA J ħ ΔA ΔB p s + occAccumA J ħ ΔA ΔB ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow s p) t

★ The group law of the accumulated occupancy of A along the two-site flow.

theorem CSD.CV.occHist_twoDetunedFlow_arenaFlow (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s u : ℝ) : occHist J ħ (ΔB - ΔA) ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow s p) u = occHist J ħ (ΔB - ΔA) p (u + s)

The history of B from the ray evolved by the two-site flow is the shifted history.

theorem CSD.CV.occAccum_twoDetuned_add (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) (s t : ℝ) : occAccum J ħ (ΔB - ΔA) p (s + t) = occAccum J ħ (ΔB - ΔA) p s + occAccum J ħ (ΔB - ΔA) ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow s p) t

★ The group law of the accumulated occupancy of B along the two-site flow.

theorem CSD.CV.occAccumA_nonneg (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ occAccumA J ħ ΔA ΔB p t

theorem CSD.CV.occAccumA_le (J ħ ΔA ΔB : ℝ) (p : FieldArena 2 2) {t : ℝ} (ht : 0 ≤ t) : occAccumA J ħ ΔA ΔB p t ≤ t

theorem CSD.CV.twoDetunedH_commute_flow (J ħ ΔA ΔB t : ℝ) : Commute (twoDetunedH J ΔA ΔB) ↑((twoDetunedFlow J ħ ΔA ΔB).flow t)

theorem CSD.CV.arenaObs_twoDetunedH_arenaFlow (J ħ ΔA ΔB t : ℝ) (p : FieldArena 2 2) : arenaObs (twoDetunedH J ΔA ΔB) ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t p) = arenaObs (twoDetunedH J ΔA ΔB) p

★ Energy conservation on the carrier: ⟨H⟩ is constant along the two-site flow.

theorem CSD.CV.arenaObs_twoDetunedH (J ΔA ΔB : ℝ) (p : FieldArena 2 2) : arenaObs (twoDetunedH J ΔA ΔB) p = J * arenaObs hopX p + ΔA * Projectivization.momentMap p excA + ΔB * Projectivization.momentMap p excB

The energy of the two-site Hamiltonian at a ray: J⟨X⟩ + Δ_A n_A + Δ_B n_B.

theorem CSD.CV.two_site_detuned {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (ΔA ΔB : ℝ) : (∀ (t : ℝ), ↑((twoDetunedFlow J ħ ΔA ΔB).flow t) = sectorPhase ħ ΔA t * ↑((detunedFlow J ħ (ΔB - ΔA)).flow t)) ∧ (∀ (t : ℝ), arenaObs occB ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 1)) = (J / rabiFreq J (ΔB - ΔA)) ^ 2 * Real.sin (rabiAngle J ħ (ΔB - ΔA) t) ^ 2) ∧ (∀ (t : ℝ), arenaObs occA ((twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 1)) = 1 - (J / rabiFreq J (ΔB - ΔA)) ^ 2 * Real.sin (rabiAngle J ħ (ΔB - ΔA) t) ^ 2) ∧ (∀ (t : ℝ), (twoDetunedFlow J ħ ΔA ΔB).arenaFlow t (msgPoint 0) = msgPoint 0) ∧ 0 < detunedRoundTrip J ħ (ΔB - ΔA) ∧ (twoDetunedFlow J ħ ΔA ΔB).arenaFlow (detunedRoundTrip J ħ (ΔB - ΔA)) (msgPoint 1) = msgPoint 1

★ The two-site exchange with both sites detuned, in one statement: the flow is the detuned exchange in the difference up to the sector phase; the two messages' occupancies at both sites; the vacuum fixed; and the return of the carrier to A at the detuned round trip.