The detuned exchange: the hop with a state-dependent energy at the receiver

Category: 3-Local (CV; the carrier side of BACKLOG #194, the first internally activated write).

The signal exchange of SignalExchange.lean is the hop H = J X. When the receiver's site carries an energy Δ — in #194 the back-reaction of a pointer coupled to the occupancy of B — the carrier's Hamiltonian becomes

H(Δ) = J X + Δ n_B = (Δ/2) P + Ω Y, Ω = √(J² + Δ²/4), Y = (J X + (Δ/2) Z)/Ω,

with P the one-excitation projector and Z = n_B − n_A. The two pieces commute, Y² = P, and the flow is the product of two closed-form exponentials (ExpUnique.lean):

U(t) = 1 + (e^{−iΔt/2ħ} cos(Ωt/ħ) − 1) P − i e^{−iΔt/2ħ} sin(Ωt/ħ) Y.

The receiver's occupancy for message 1 is the detuned Rabi formula (J/Ω)² sin²(Ωt/ħ): the transfer is no longer complete, and the loss 1 − (J/Ω)² = (Δ/2)²/Ω² is the explicit price of the back-reaction. The vacuum is fixed, so message 0 produces no occupancy at all.

• occA, zOp, rabiFreq, rabiY, detunedH, detunedGen, ★ detunedFlow J ħ Δ : FieldStructuredFlow 2 2 — the detuned exchange is a field-structured flow on the same edge; detunedGen_zero — at Δ = 0 it is the hop of #183;
• ★★ detunedFlow_val_eq — the flow in closed form, by exp_add_of_commute and two uses of exp_smul_eq_cosh_sinh; detunedFlow_msgPoint_zero — the vacuum is fixed;
• ★★ detuned_readout_one — the receiver's occupancy for message 1 is (J/Ω)² sin²(Ωt/ħ); detuned_readout_zero; ★ detuned_readout_one_le, detuned_readout_one_peak, detuned_readout_one_lt_one, one_sub_div_rabiFreq_sq — the detuning loss, attained at the detuned hop time and strictly positive whenever Δ ≠ 0;
• ★ arenaObs_detunedH_arenaFlow — the carrier's energy ⟨H(Δ)⟩ is conserved along the flow;
• occHist, occAccum — the receiver's occupancy history and its time integral, for every arena point; ★ occAccum_add — the integral obeys the flow's group law; ★ hasDerivAt_occAccum — its derivative is the occupancy; ★★ occAccum_msgPoint_one — the closed form for message 1, (J/Ω)² (Ωt/ħ − sin cos)/(2Ω/ħ); occAccum_msgPoint_zero = 0;
• continuous_arenaDM, continuous_arenaObs_prod, ★ continuous_arenaKick_prod — the arena density, the observables and the unitary kick are continuous, jointly in all arguments, by descent through the open quotient map mk'; continuous_occHist_prod, continuous_occAccum_prod — the history and its integral are continuous jointly in the ray and the detuning, which is what #194's skew product needs.

Honest scope

• Nothing here is a record. The pointer that produces Δ and reads the occupancy is RecordLayer/ActivatedWrite.lean; this file is its carrier.
• Δ is a real parameter. In #194 it is a function of a conserved torus angle, so the flow at fixed angle is exactly this one; no time dependence appears anywhere.
• J > 0 is assumed where the closed form divides by Ω; ħ enters only through the angles.

References: specs/BACKLOG.md #194, #183, #195; CV/SignalExchange.lean (hopX, oneExc, occB, msgPoint, receiver_readout_one), CV/FieldStructuredFlow.lean, CV/ArenaBridge.lean (arenaObs_kick_conj, arenaDM_mk), Mathlib/Analysis/Normed/Algebra/ExpUnique.lean, Mathlib/LinearAlgebra/Projectivization/Topology.lean (isOpenQuotientMap_mk').

Continuity on the arena, jointly in all arguments

theorem CSD.CV.continuous_arenaDM {ι : Type u_1} [Fintype ι] : Continuous arenaDM

The arena density is continuous, by descent through the quotient map mk': arenaDM is defined through Projectivization.rep, which is not continuous, but arenaDM (mk v) = dmVec v and dmVec is continuous on the nonzero vectors.

theorem CSD.CV.continuous_arenaObs_prod {ι : Type u_1} [Fintype ι] : Continuous fun (x : GenArena ι × Matrix ι ι ℂ) => arenaObs x.2 x.1

Arena observables are continuous jointly in the ray and the operator.

theorem CSD.CV.continuous_arenaObs {ι : Type u_1} [Fintype ι] (A : Matrix ι ι ℂ) : Continuous fun (p : GenArena ι) => arenaObs A p

theorem Continuous.arenaObs {ι : Type u_1} [Fintype ι] {X : Type u_2} [TopologicalSpace X] {M : X → Matrix ι ι ℂ} {p : X → CSD.CV.GenArena ι} (hM : Continuous M) (hp : Continuous p) : Continuous fun (x : X) => CSD.CV.arenaObs (M x) (p x)

An arena observable of a continuous operator family at a continuous family of rays is continuous. Stated in applied form so that it composes without unfolding arenaObs.

theorem CSD.CV.continuous_arenaKick_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Continuous fun (x : ↥(Matrix.unitaryGroup ι ℂ) × GenArena ι) => arenaKick x.1 x.2

★ The unitary kick is continuous jointly in the unitary and the ray: id × mk' is an open quotient map, and the lift (U, v) ↦ mk (U v) is continuous.

theorem Continuous.arenaKick {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Type u_2} [TopologicalSpace X] {U : X → ↥(Matrix.unitaryGroup ι ℂ)} {p : X → CSD.CV.GenArena ι} (hU : Continuous U) (hp : Continuous p) : Continuous fun (x : X) => CSD.CV.arenaKick (U x) (p x)

The kick of a continuous family of unitaries at a continuous family of rays is continuous.

theorem CSD.CV.arenaKick_eq_smul' {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (p : GenArena ι) : arenaKick U p = U • p

The kick is the unitary action (general index type).

theorem CSD.CV.arenaKick_measurePreserving {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (p₀ : GenArena ι) : MeasureTheory.MeasurePreserving (arenaKick U) (Matrix.UnitaryGroup.fsMeasure p₀) (Matrix.UnitaryGroup.fsMeasure p₀)

Every unitary kick preserves the Fubini–Study measure at every reference point.

theorem CSD.CV.arenaObs_add {ι : Type u_1} [Fintype ι] (A B : Matrix ι ι ℂ) (p : GenArena ι) : arenaObs (A + B) p = arenaObs A p + arenaObs B p

theorem CSD.CV.arenaObs_real_smul {ι : Type u_1} [Fintype ι] (r : ℝ) (A : Matrix ι ι ℂ) (p : GenArena ι) : arenaObs (↑r • A) p = r * arenaObs A p

theorem CSD.CV.arenaObs_single_eq_momentMap {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) (p : GenArena ι) : arenaObs (Matrix.single j j 1) p = Projectivization.momentMap p j

The expectation of a basis projector at a ray is its moment coordinate.

Generic facts about field-structured flows

theorem CSD.CV.FieldStructuredFlow.flow_zero {K N : ℕ} (F : FieldStructuredFlow K N) : F.flow 0 = 1

theorem CSD.CV.FieldStructuredFlow.arenaFlow_zero' {K N : ℕ} (F : FieldStructuredFlow K N) (p : FieldArena K N) : F.arenaFlow 0 p = p

theorem CSD.CV.FieldStructuredFlow.arenaFlow_measurePreserving {K N : ℕ} (F : FieldStructuredFlow K N) (t : ℝ) (p₀ : FieldArena K N) : MeasureTheory.MeasurePreserving (F.arenaFlow t) (Matrix.UnitaryGroup.fsMeasure p₀) (Matrix.UnitaryGroup.fsMeasure p₀)

The occupancy of A, the imbalance Z, and their algebra

noncomputable def CSD.CV.occA : Matrix HopConfig HopConfig ℂ

The occupancy of A.

Equations

• CSD.CV.occA = Matrix.single CSD.CV.excA CSD.CV.excA 1

noncomputable def CSD.CV.zOp : Matrix HopConfig HopConfig ℂ

The imbalance Z = n_B − n_A.

Equations

• CSD.CV.zOp = CSD.CV.occB - CSD.CV.occA

theorem CSD.CV.oneExc_eq_occA_add_occB : oneExc = occA + occB

theorem CSD.CV.occB_conjTranspose : occB.conjTranspose = occB

theorem CSD.CV.occA_conjTranspose : occA.conjTranspose = occA

theorem CSD.CV.zOp_conjTranspose : zOp.conjTranspose = zOp

theorem CSD.CV.single_mul_single_hop (i : HopConfig) {j k l : HopConfig} (h : j ≠ k) : Matrix.single i j 1 * Matrix.single k l 1 = 0

Two matrix units whose inner indices differ multiply to zero.

theorem CSD.CV.zOp_mul_zOp : zOp * zOp = oneExc

theorem CSD.CV.hopX_mul_zOp : hopX * zOp = Matrix.single excA excB 1 - Matrix.single excB excA 1

theorem CSD.CV.zOp_mul_hopX : zOp * hopX = Matrix.single excB excA 1 - Matrix.single excA excB 1

theorem CSD.CV.oneExc_mul_oneExc : oneExc * oneExc = oneExc

theorem CSD.CV.oneExc_mul_hopX : oneExc * hopX = hopX

theorem CSD.CV.oneExc_mul_zOp : oneExc * zOp = zOp

theorem CSD.CV.zOp_mul_oneExc : zOp * oneExc = zOp

The Rabi frequency and the rescaled traceless part

noncomputable def CSD.CV.rabiFreq (J Δ : ℝ) : ℝ

The Rabi energy of the detuned hop: Ω = √(J² + (Δ/2)²).

Equations

• CSD.CV.rabiFreq J Δ = √(J ^ 2 + (Δ / 2) ^ 2)

theorem CSD.CV.rabiFreq_sq (J Δ : ℝ) : rabiFreq J Δ ^ 2 = J ^ 2 + (Δ / 2) ^ 2

theorem CSD.CV.rabiFreq_pos {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : 0 < rabiFreq J Δ

theorem CSD.CV.le_rabiFreq {J : ℝ} (hJ : 0 ≤ J) (Δ : ℝ) : J ≤ rabiFreq J Δ

theorem CSD.CV.rabiFreq_zero {J : ℝ} (hJ : 0 ≤ J) : rabiFreq J 0 = J

theorem CSD.CV.div_rabiFreq_sq_le_one {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : (J / rabiFreq J Δ) ^ 2 ≤ 1

The peak transfer (J/Ω)² is at most 1.

theorem CSD.CV.div_rabiFreq_sq_pos {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : 0 < (J / rabiFreq J Δ) ^ 2

theorem CSD.CV.one_sub_div_rabiFreq_sq {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : 1 - (J / rabiFreq J Δ) ^ 2 = (Δ / 2) ^ 2 / rabiFreq J Δ ^ 2

★ The detuning loss: 1 − (J/Ω)² = (Δ/2)²/Ω².

theorem CSD.CV.div_rabiFreq_sq_lt_one {J : ℝ} (hJ : 0 < J) {Δ : ℝ} (hΔ : Δ ≠ 0) : (J / rabiFreq J Δ) ^ 2 < 1

The detuning loss is strictly positive whenever Δ ≠ 0.

noncomputable def CSD.CV.rabiY (J Δ : ℝ) : Matrix HopConfig HopConfig ℂ

The rescaled traceless part Y = (J X + (Δ/2) Z)/Ω, with Y² = P and Y P = Y.

Equations

• CSD.CV.rabiY J Δ = ↑(CSD.CV.rabiFreq J Δ)⁻¹ • (↑J • CSD.CV.hopX + ↑(Δ / 2) • CSD.CV.zOp)

theorem CSD.CV.rabiY_mul_oneExc (J Δ : ℝ) : rabiY J Δ * oneExc = rabiY J Δ

theorem CSD.CV.oneExc_mul_rabiY (J Δ : ℝ) : oneExc * rabiY J Δ = rabiY J Δ

theorem CSD.CV.rabiY_mul_rabiY {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : rabiY J Δ * rabiY J Δ = oneExc

The detuned Hamiltonian, its generator and its flow

noncomputable def CSD.CV.detunedH (J Δ : ℝ) : Matrix HopConfig HopConfig ℂ

The detuned Hamiltonian H(Δ) = J X + Δ n_B.

Equations

• CSD.CV.detunedH J Δ = ↑J • CSD.CV.hopX + ↑Δ • CSD.CV.occB

theorem CSD.CV.detunedH_conjTranspose (J Δ : ℝ) : (detunedH J Δ).conjTranspose = detunedH J Δ

theorem CSD.CV.detunedH_eq {J : ℝ} (hJ : 0 < J) (Δ : ℝ) : detunedH J Δ = ↑(Δ / 2) • oneExc + ↑(rabiFreq J Δ) • rabiY J Δ

H(Δ) = (Δ/2) P + Ω Y.

noncomputable def CSD.CV.detunedGen (J ħ Δ : ℝ) : Matrix HopConfig HopConfig ℂ

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

Equations

• CSD.CV.detunedGen J ħ Δ = -(Complex.I * ↑(1 / ħ)) • CSD.CV.detunedH J Δ

theorem CSD.CV.detunedGen_skew (J ħ Δ : ℝ) : (detunedGen J ħ Δ).conjTranspose = -detunedGen J ħ Δ

theorem CSD.CV.detunedGen_zero (J ħ : ℝ) : detunedGen J ħ 0 = hopGen J ħ

At zero detuning the generator is the hop's.

theorem CSD.CV.continuous_detunedGen (J ħ : ℝ) : Continuous fun (Δ : ℝ) => detunedGen J ħ Δ

noncomputable def CSD.CV.detunedFlow (J ħ Δ : ℝ) : FieldStructuredFlow 2 2

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

Equations

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

theorem CSD.CV.detunedFlow_val (J ħ Δ t : ℝ) : ↑((detunedFlow J ħ Δ).flow t) = NormedSpace.exp (t • detunedGen J ħ Δ)

theorem CSD.CV.detunedFlow_val_zero_detuning (J ħ t : ℝ) : ↑((detunedFlow J ħ 0).flow t) = ↑((hopFlow J ħ).flow t)

At zero detuning the flow is the hop's flow.

theorem CSD.CV.continuous_detunedFlowVal_prod (J ħ : ℝ) : Continuous fun (x : ℝ × ℝ) => ↑((detunedFlow J ħ x.1).flow x.2)

The flow is continuous jointly in the detuning and the time.

theorem CSD.CV.continuous_detunedFlowVal (J ħ Δ : ℝ) : Continuous fun (t : ℝ) => ↑((detunedFlow J ħ Δ).flow t)

theorem CSD.CV.continuous_detunedFlow_prod (J ħ : ℝ) : Continuous fun (x : ℝ × ℝ) => (detunedFlow J ħ x.1).flow x.2

The unitary itself, as a continuous family in the detuning and the time.

theorem CSD.CV.continuous_detunedFlow (J ħ Δ : ℝ) : Continuous fun (t : ℝ) => (detunedFlow J ħ Δ).flow t

theorem CSD.CV.hasDerivAt_detunedFlowVal (J ħ Δ t : ℝ) : HasDerivAt (fun (t : ℝ) => ↑((detunedFlow J ħ Δ).flow t)) (detunedGen J ħ Δ * ↑((detunedFlow J ħ Δ).flow t)) t

The Schrödinger equation of the detuned exchange: U' = G U, with the state-dependent generator.

The closed form

noncomputable def CSD.CV.dynPhase (ħ Δ t : ℝ) : ℝ

The dynamical phase Δ t/(2ħ).

Equations

• CSD.CV.dynPhase ħ Δ t = Δ * t / (2 * ħ)

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

The Rabi rate Ω/ħ.

Equations

• CSD.CV.rabiRate J ħ Δ = CSD.CV.rabiFreq J Δ / ħ

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

The Rabi angle Ω t/ħ.

Equations

• CSD.CV.rabiAngle J ħ Δ t = CSD.CV.rabiRate J ħ Δ * t

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

theorem CSD.CV.smul_detunedGen {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : t • detunedGen J ħ Δ = (↑(-dynPhase ħ Δ t) * Complex.I) • oneExc + (↑(-rabiAngle J ħ Δ t) * Complex.I) • rabiY J Δ

theorem CSD.CV.detunedFlow_val_eq {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : ↑((detunedFlow J ħ Δ).flow t) = 1 + (Complex.exp (↑(-dynPhase ħ Δ t) * Complex.I) * ↑(Real.cos (rabiAngle J ħ Δ t)) - 1) • oneExc + -(Complex.I * Complex.exp (↑(-dynPhase ħ Δ t) * Complex.I) * ↑(Real.sin (rabiAngle J ħ Δ t))) • rabiY J Δ

★★ The flow in closed form: U(t) = 1 + (e^{−iΔt/2ħ} cos(Ωt/ħ) − 1) P − i e^{−iΔt/2ħ} sin(Ωt/ħ) Y.

Entries of the closed form

theorem CSD.CV.oneExc_apply_vacC (i : HopConfig) : oneExc i vacC = 0

theorem CSD.CV.rabiY_apply_vacC (J Δ : ℝ) (i : HopConfig) : rabiY J Δ i vacC = 0

theorem CSD.CV.oneExc_apply_excB_excA : oneExc excB excA = 0

theorem CSD.CV.rabiY_apply_excB_excA (J Δ : ℝ) : rabiY J Δ excB excA = ↑(rabiFreq J Δ)⁻¹ * ↑J

theorem CSD.CV.detunedFlow_apply_vacC {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) (i : HopConfig) : ↑((detunedFlow J ħ Δ).flow t) i vacC = if i = vacC then 1 else 0

The vacuum column of the flow is the vacuum: the vacuum is fixed.

theorem CSD.CV.detunedFlow_apply_excB_excA {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : ↑((detunedFlow J ħ Δ).flow t) excB excA = -(Complex.I * Complex.exp (↑(-dynPhase ħ Δ t) * Complex.I)) * ↑(Real.sin (rabiAngle J ħ Δ t) * (J / rabiFreq J Δ))

The transfer amplitude U_{BA}(t) = −i e^{−iΔt/2ħ} · (J/Ω) sin(Ωt/ħ).

theorem CSD.CV.toEuclideanLin_detunedFlow_vacC {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : (Matrix.toEuclideanLin ↑((detunedFlow J ħ Δ).flow t)) (basisVec vacC) = basisVec vacC

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

The vacuum is fixed by the detuned flow: message 0 never reaches the receiver.

theorem CSD.CV.norm_basisVec (c : HopConfig) : ‖basisVec c‖ = 1

theorem CSD.CV.detunedFlow_isom (J ħ Δ t : ℝ) : (↑((detunedFlow J ħ Δ).flow t)).conjTranspose * ↑((detunedFlow J ħ Δ).flow t) = 1

The receiver's readouts under detuning

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

★★ The detuned Rabi formula: the receiver's occupancy for message 1 is (J/Ω)² sin²(Ωt/ħ).

theorem CSD.CV.detuned_readout_zero {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : arenaObs occB ((detunedFlow J ħ Δ).arenaFlow t (msgPoint 0)) = 0

The receiver's occupancy for message 0 is 0.

theorem CSD.CV.detuned_readout_one_le {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : arenaObs occB ((detunedFlow J ħ Δ).arenaFlow t (msgPoint 1)) ≤ (J / rabiFreq J Δ) ^ 2

★ The detuning loss: the readout never exceeds (J/Ω)².

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

The detuned hop time π ħ/(2Ω).

Equations

• CSD.CV.detunedHopTime J ħ Δ = Real.pi * ħ / (2 * CSD.CV.rabiFreq J Δ)

theorem CSD.CV.rabiAngle_detunedHopTime {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : rabiAngle J ħ Δ (detunedHopTime J ħ Δ) = Real.pi / 2

theorem CSD.CV.detuned_readout_one_peak {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) : arenaObs occB ((detunedFlow J ħ Δ).arenaFlow (detunedHopTime J ħ Δ) (msgPoint 1)) = (J / rabiFreq J Δ) ^ 2

★ The loss is attained: at the detuned hop time the readout is exactly (J/Ω)².

theorem CSD.CV.detuned_readout_one_lt_one {J : ℝ} (hJ : 0 < J) (ħ : ℝ) {Δ : ℝ} (hΔ : Δ ≠ 0) (t : ℝ) : arenaObs occB ((detunedFlow J ħ Δ).arenaFlow t (msgPoint 1)) < 1

With a nonzero detuning the transfer is never complete.

The carrier's energy is conserved

theorem CSD.CV.detunedH_commute_flow (J ħ Δ t : ℝ) : Commute (detunedH J Δ) ↑((detunedFlow J ħ Δ).flow t)

theorem CSD.CV.arenaObs_detunedH_arenaFlow (J ħ Δ t : ℝ) (p : FieldArena 2 2) : arenaObs (detunedH J Δ) ((detunedFlow J ħ Δ).arenaFlow t p) = arenaObs (detunedH J Δ) p

★ Energy conservation on the carrier: ⟨H(Δ)⟩ is constant along the detuned flow.

theorem CSD.CV.arenaObs_detunedH (J Δ : ℝ) (p : FieldArena 2 2) : arenaObs (detunedH J Δ) p = J * arenaObs hopX p + Δ * Projectivization.momentMap p excB

The energy of the detuned Hamiltonian at a ray: J⟨X⟩ + Δ n_B.

The occupancy history and its time integral

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

The receiver's occupancy history along the detuned exchange from p.

Equations

• CSD.CV.occHist J ħ Δ p s = CSD.CV.arenaObs CSD.CV.occB ((CSD.CV.detunedFlow J ħ Δ).arenaFlow s p)

theorem CSD.CV.occHist_eq_momentMap (J ħ Δ : ℝ) (p : FieldArena 2 2) (s : ℝ) : occHist J ħ Δ p s = Projectivization.momentMap ((detunedFlow J ħ Δ).arenaFlow s p) excB

theorem CSD.CV.occHist_nonneg (J ħ Δ : ℝ) (p : FieldArena 2 2) (s : ℝ) : 0 ≤ occHist J ħ Δ p s

theorem CSD.CV.occHist_le_one (J ħ Δ : ℝ) (p : FieldArena 2 2) (s : ℝ) : occHist J ħ Δ p s ≤ 1

theorem CSD.CV.occHist_eq_heis (J ħ Δ : ℝ) (p : FieldArena 2 2) (s : ℝ) : occHist J ħ Δ p s = arenaObs (star ↑((detunedFlow J ħ Δ).flow s) * occB * ↑((detunedFlow J ħ Δ).flow s)) p

The history in Heisenberg form: the occupancy of the evolved ray is the expectation of the evolved occupancy.

theorem CSD.CV.continuous_occHist_prod (J ħ : ℝ) : Continuous (Function.uncurry fun (x : FieldArena 2 2 × ℝ) (s : ℝ) => occHist J ħ x.2 x.1 s)

The history is continuous jointly in the ray, the detuning and the time, stated in the uncurried form the parametric-integral lemma consumes.

theorem CSD.CV.continuous_occHist (J ħ Δ : ℝ) (p : FieldArena 2 2) : Continuous fun (s : ℝ) => occHist J ħ Δ p s

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

The accumulated receiver occupancy ∫₀ᵗ n_B(p(s)) ds.

Equations

• CSD.CV.occAccum J ħ Δ p t = ∫ (s : ℝ) in 0..t, CSD.CV.occHist J ħ Δ p s

theorem CSD.CV.occAccum_zero (J ħ Δ : ℝ) (p : FieldArena 2 2) : occAccum J ħ Δ p 0 = 0

theorem CSD.CV.occAccum_nonneg (J ħ Δ : ℝ) (p : FieldArena 2 2) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ occAccum J ħ Δ p t

theorem CSD.CV.occAccum_le (J ħ Δ : ℝ) (p : FieldArena 2 2) {t : ℝ} (ht : 0 ≤ t) : occAccum J ħ Δ p t ≤ t

theorem CSD.CV.occHist_arenaFlow (J ħ Δ : ℝ) (p : FieldArena 2 2) (s u : ℝ) : occHist J ħ Δ ((detunedFlow J ħ Δ).arenaFlow s p) u = occHist J ħ Δ p (u + s)

The history from the evolved ray is the shifted history.

theorem CSD.CV.occAccum_add (J ħ Δ : ℝ) (p : FieldArena 2 2) (s t : ℝ) : occAccum J ħ Δ p (s + t) = occAccum J ħ Δ p s + occAccum J ħ Δ ((detunedFlow J ħ Δ).arenaFlow s p) t

★ The group law of the accumulated occupancy: A(p, s + t) = A(p, s) + A(U(s)p, t).

theorem CSD.CV.hasDerivAt_occAccum (J ħ Δ : ℝ) (p : FieldArena 2 2) (t : ℝ) : HasDerivAt (fun (t : ℝ) => occAccum J ħ Δ p t) (occHist J ħ Δ p t) t

★ The pointer's rate: the accumulated occupancy has derivative the occupancy.

theorem CSD.CV.continuous_occAccum (J ħ Δ : ℝ) (p : FieldArena 2 2) : Continuous fun (t : ℝ) => occAccum J ħ Δ p t

theorem CSD.CV.continuous_occAccum_prod (J ħ t : ℝ) : Continuous fun (x : FieldArena 2 2 × ℝ) => occAccum J ħ x.2 x.1 t

The accumulated occupancy is continuous jointly in the ray and the detuning, at every fixed time — the measurability #194's skew product needs.

The two messages

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

theorem CSD.CV.occHist_msgPoint_zero {J : ℝ} (hJ : 0 < J) (ħ Δ s : ℝ) : occHist J ħ Δ (msgPoint 0) s = 0

theorem CSD.CV.occHist_msgPoint_one_zero {J : ℝ} (hJ : 0 < J) (ħ Δ : ℝ) : occHist J ħ Δ (msgPoint 1) 0 = 0

The pointer starts at rest: at t = 0 nothing has arrived at the receiver.

theorem CSD.CV.occHist_msgPoint_one_pos {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ : ℝ) {s : ℝ} (hs : 0 < s) (hs' : s < Real.pi / rabiRate J ħ Δ) : 0 < occHist J ħ Δ (msgPoint 1) s

The activation is the arriving carrier: on (0, πħ/Ω) the occupancy is strictly positive.

theorem CSD.CV.occAccum_msgPoint_zero {J : ℝ} (hJ : 0 < J) (ħ Δ t : ℝ) : occAccum J ħ Δ (msgPoint 0) t = 0

theorem CSD.CV.occAccum_msgPoint_one {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (Δ t : ℝ) : occAccum J ħ Δ (msgPoint 1) t = (J / rabiFreq J Δ) ^ 2 * (rabiAngle J ħ Δ t - Real.sin (rabiAngle J ħ Δ t) * Real.cos (rabiAngle J ħ Δ t)) / (2 * rabiRate J ħ Δ)

★★ The accumulated occupancy for message 1 in closed form: (J/Ω)² (Ωt/ħ − sin(Ωt/ħ) cos(Ωt/ħ)) / (2Ω/ħ).