The signal exchange: a two-site hop, exact transfer with its phase, and the Rabi return

Category: 3-Local (CV; the smallest physical signal of the clock-and-echo programme). BACKLOG #183 (out of #39; the first of #183–#189).

Two sites A = 0 and B = 1, each holding 0 or 1 excitation (FieldConfig 2 2). The hop X = |10⟩⟨01| + |01⟩⟨10| exchanges the one-excitation configurations and does nothing else, so X² = P (the one-excitation projector) and X P = X, and the Schrödinger generator −(i J/ħ) X of the Hamiltonian H = J X has the flow

U(t) = 1 + (cos θ − 1) P − i sin θ · X, θ = J t / ħ,

by the ODE uniqueness of ExpUnique.lean, not by a series. The sender's message is the occupancy of A (0 or 1); the receiver reads the occupancy of B.

• hopX, oneExc, hopGen, ★ hopFlow J ħ : FieldStructuredFlow 2 2 — the exchange is an instance of the CSD field-structured dynamics, so FieldStructuredFlow.lightcone applies to it with no further hypothesis;
• ★★ hopFlow_val_eq — the flow in closed form;
• hopTime J ħ = π ħ / (2 J), ★★ transfer_at_hopTime — the excitation at A becomes −i times the excitation at B: the transfer is exact and the phase is a theorem;
• roundTrip J ħ = 2 · hopTime, ★★ return_at_roundTrip — the echo is the Rabi return: at 2 τ_hop the excitation is back at A with phase −1, and the arena point is the message point again (arenaFlow_roundTrip); the round trip is nonzero (roundTrip_pos);
• receiver_readout_one, receiver_readout_zero — the receiver's readout arenaObs occB is sin² θ for message 1 and 0 for message 0;
• ★★★ receiver_distinguishes — at τ_hop the readout is 1 versus 0;
• ★ partial_transfer_before_hopTime — complete transfer at τ_hop does not mean silence before it: on (0, τ_hop) the readout is strictly between 0 and 1;
• influence_of_message — the two preparations differ only in the occupancy of A (msgConfig_siteB) and give different receiver readouts: causal influence by comparison of preparations, not inferred from a correlation;
• ★★★ signal_exchange — the package.

Drift check

The hop is quantum mechanics — the isolated item's Hamiltonian flow on the arena (R-016′), the calculation engine. The records of emission at A and reception at B are ontic writes in Σ and belong to #186; nothing here is a record. Successful transmission is a readout at a stated time, not a propagation bound; the Lieb–Robinson cone of FieldStructuredFlow.lightcone bounds what can happen, it does not say what does.

Honest scope

• Two sites and one excitation; the "message" is a one-bit occupancy. Longer chains need a sequentially activated coupling schedule to transfer exactly, which this file does not claim.
• J and ħ are positive reals in consistent units (J an energy, ħ an action, J/ħ a rate); no numerical value is derived from either.
• Zero processing delay at B: the echo is the free Rabi return, not a reflection protocol.

References: specs/BACKLOG.md #183, #39, #186; specs/records-to-spacetime-scoping.md §4; CV/FieldStructuredFlow.lean (FieldStructuredFlow, lightcone), CV/ArenaBridge.lean (arenaKick_mk, arenaObs, dmVec), Mathlib/Analysis/Normed/Algebra/ExpUnique.lean.

Configurations: two sites, one bit each

@[reducible, inline]

abbrev CSD.CV.HopConfig : Type

Two sites, occupancy 0 or 1.

Equations

• CSD.CV.HopConfig = CSD.CV.FieldConfig 2 2

def CSD.CV.vacC : HopConfig

The vacuum.

Equations

• CSD.CV.vacC = ![0, 0]

def CSD.CV.excA : HopConfig

One excitation at A.

Equations

• CSD.CV.excA = ![1, 0]

def CSD.CV.excB : HopConfig

One excitation at B.

Equations

• CSD.CV.excB = ![0, 1]

theorem CSD.CV.excA_ne_excB : excA ≠ excB

theorem CSD.CV.vacC_ne_excA : vacC ≠ excA

theorem CSD.CV.vacC_ne_excB : vacC ≠ excB

def CSD.CV.msgConfig (b : Fin 2) : HopConfig

The sender's message b is the occupancy of A; B is empty in both preparations.

Equations

• CSD.CV.msgConfig b = ![b, 0]

theorem CSD.CV.msgConfig_zero : msgConfig 0 = vacC

theorem CSD.CV.msgConfig_one : msgConfig 1 = excA

theorem CSD.CV.msgConfig_siteB (b : Fin 2) : msgConfig b 1 = 0

The two preparations agree at the receiver's site.

The hop and the one-excitation projector

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

The hop |10⟩⟨01| + |01⟩⟨10|.

Equations

• CSD.CV.hopX = Matrix.single CSD.CV.excA CSD.CV.excB 1 + Matrix.single CSD.CV.excB CSD.CV.excA 1

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

The projector on the one-excitation configurations.

Equations

• CSD.CV.oneExc = Matrix.single CSD.CV.excA CSD.CV.excA 1 + Matrix.single CSD.CV.excB CSD.CV.excB 1

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

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

theorem CSD.CV.single_conjTranspose {ι : Type u_1} [DecidableEq ι] (i j : ι) (a : ℂ) : (Matrix.single i j a).conjTranspose = Matrix.single j i (star a)

theorem CSD.CV.hopX_conjTranspose : hopX.conjTranspose = hopX

The generator and the field-structured flow

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

The Schrödinger generator −(i J/ħ) X of the Hamiltonian H = J X.

Equations

• CSD.CV.hopGen J ħ = -(Complex.I * ↑(J / ħ)) • CSD.CV.hopX

theorem CSD.CV.hopGen_skew (J ħ : ℝ) : (hopGen J ħ).conjTranspose = -hopGen J ħ

theorem CSD.CV.supportedOn_pair (M : Matrix HopConfig HopConfig ℂ) : SupportedOn {0, 1} M

On two sites every operator is supported on {A, B}.

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

★ The exchange as a field-structured flow: one coupling edge (A, B) carrying the hop.

Equations

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

theorem CSD.CV.hopFlow_val (J ħ t : ℝ) : ↑((hopFlow J ħ).flow t) = NormedSpace.exp (t • hopGen J ħ)

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

The phase angle θ = J t / ħ.

Equations

• CSD.CV.hopAngle J ħ t = J / ħ * t

theorem CSD.CV.smul_hopGen (J ħ t : ℝ) : t • hopGen J ħ = (↑(-hopAngle J ħ t) * Complex.I) • hopX

theorem CSD.CV.hopFlow_val_eq (J ħ t : ℝ) : ↑((hopFlow J ħ).flow t) = 1 + ↑(Real.cos (hopAngle J ħ t) - 1) • oneExc + -(Complex.I * ↑(Real.sin (hopAngle J ħ t))) • hopX

★★ The flow in closed form: U(t) = 1 + (cos θ − 1) P − i sin θ · X.

The column of the flow at a basis configuration

theorem CSD.CV.hopFlow_mulVec_excA (J ħ t : ℝ) : (↑((hopFlow J ħ).flow t)).mulVec (Pi.single excA 1) = ↑(Real.cos (hopAngle J ħ t)) • Pi.single excA 1 + -(Complex.I * ↑(Real.sin (hopAngle J ħ t))) • Pi.single excB 1

The flow applied to the excitation at A: cos θ · e_A − i sin θ · e_B.

theorem CSD.CV.hopFlow_mulVec_vacC (J ħ t : ℝ) : (↑((hopFlow J ħ).flow t)).mulVec (Pi.single vacC 1) = Pi.single vacC 1

The flow fixes the vacuum.

Arena points and the receiver's readout

noncomputable def CSD.CV.basisVec (c : HopConfig) : EuclideanSpace ℂ HopConfig

The basis vector of a configuration.

Equations

• CSD.CV.basisVec c = PiLp.single 2 c 1

theorem CSD.CV.basisVec_apply (c c' : HopConfig) : (basisVec c).ofLp c' = Pi.single c 1 c'

theorem CSD.CV.basisVec_ne_zero (c : HopConfig) : basisVec c ≠ 0

noncomputable def CSD.CV.msgPoint (b : Fin 2) : FieldArena 2 2

The arena point of message b: excitation b at A, nothing at B.

Equations

• CSD.CV.msgPoint b = Projectivization.mk ℂ (CSD.CV.basisVec (CSD.CV.msgConfig b)) ⋯

theorem CSD.CV.msgPoint_zero : msgPoint 0 = Projectivization.mk ℂ (basisVec vacC) ⋯

theorem CSD.CV.msgPoint_one : msgPoint 1 = Projectivization.mk ℂ (basisVec excA) ⋯

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

The receiver's observable: "the excitation sits at B".

Equations

• CSD.CV.occB = Matrix.single CSD.CV.excB CSD.CV.excB 1

theorem CSD.CV.arenaObs_single_mk {ι : Type u_1} [Fintype ι] [DecidableEq ι] {v : EuclideanSpace ℂ ι} (hv : v ≠ 0) (j : ι) : arenaObs (Matrix.single j j 1) (Projectivization.mk ℂ v hv) = ‖v.ofLp j‖ ^ 2 / ‖v‖ ^ 2

The Born weight of a basis projector at a ray: ‖v j‖² / ‖v‖².

theorem CSD.CV.toEuclideanLin_hopFlow_excA (J ħ t : ℝ) : (Matrix.toEuclideanLin ↑((hopFlow J ħ).flow t)) (basisVec excA) = ↑(Real.cos (hopAngle J ħ t)) • basisVec excA + -(Complex.I * ↑(Real.sin (hopAngle J ħ t))) • basisVec excB

The vector the flow produces from message 1, in Euclidean form.

theorem CSD.CV.toEuclideanLin_hopFlow_vacC (J ħ t : ℝ) : (Matrix.toEuclideanLin ↑((hopFlow J ħ).flow t)) (basisVec vacC) = basisVec vacC

theorem CSD.CV.norm_transferred (J ħ t : ℝ) : ‖↑(Real.cos (hopAngle J ħ t)) • basisVec excA + -(Complex.I * ↑(Real.sin (hopAngle J ħ t))) • basisVec excB‖ = 1

The transferred vector has unit norm: cos² θ + sin² θ = 1.

theorem CSD.CV.receiver_readout_one (J ħ t : ℝ) : arenaObs occB ((hopFlow J ħ).arenaFlow t (msgPoint 1)) = Real.sin (hopAngle J ħ t) ^ 2

The receiver's readout for message 1 is sin² θ.

theorem CSD.CV.receiver_readout_zero (J ħ t : ℝ) : arenaObs occB ((hopFlow J ħ).arenaFlow t (msgPoint 0)) = 0

The receiver's readout for message 0 is 0: the vacuum does not move.

The hop time, the transfer, the return

noncomputable def CSD.CV.hopTime (J ħ : ℝ) : ℝ

τ_hop = π ħ / (2 J): the time of complete transfer.

Equations

• CSD.CV.hopTime J ħ = Real.pi * ħ / (2 * J)

noncomputable def CSD.CV.roundTrip (J ħ : ℝ) : ℝ

The round trip 2 τ_hop.

Equations

• CSD.CV.roundTrip J ħ = 2 * CSD.CV.hopTime J ħ

theorem CSD.CV.hopTime_pos {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : 0 < hopTime J ħ

theorem CSD.CV.roundTrip_pos {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : 0 < roundTrip J ħ

The round trip is nonzero.

theorem CSD.CV.hopAngle_hopTime {J ħ : ℝ} (hJ : J ≠ 0) (hħ : ħ ≠ 0) : hopAngle J ħ (hopTime J ħ) = Real.pi / 2

theorem CSD.CV.hopAngle_roundTrip {J ħ : ℝ} (hJ : J ≠ 0) (hħ : ħ ≠ 0) : hopAngle J ħ (roundTrip J ħ) = Real.pi

theorem CSD.CV.transfer_at_hopTime {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (Matrix.toEuclideanLin ↑((hopFlow J ħ).flow (hopTime J ħ))) (basisVec excA) = -Complex.I • basisVec excB

★★ Exact transfer with its phase: at τ_hop the excitation at A is −i times the excitation at B.

theorem CSD.CV.return_at_roundTrip {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (Matrix.toEuclideanLin ↑((hopFlow J ħ).flow (roundTrip J ħ))) (basisVec excA) = -1 • basisVec excA

★★ The echo is the Rabi return: at 2 τ_hop the excitation is back at A with phase −1.

theorem CSD.CV.arenaFlow_hopTime {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (hopFlow J ħ).arenaFlow (hopTime J ħ) (msgPoint 1) = Projectivization.mk ℂ (basisVec excB) ⋯

At τ_hop the arena point of message 1 is the ray of the excitation at B.

theorem CSD.CV.arenaFlow_roundTrip {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (hopFlow J ħ).arenaFlow (roundTrip J ħ) (msgPoint 1) = msgPoint 1

At 2 τ_hop the arena point of message 1 is the message point again.

Distinguishing the messages, partial transfer, influence

theorem CSD.CV.receiver_distinguishes {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : arenaObs occB ((hopFlow J ħ).arenaFlow (hopTime J ħ) (msgPoint 1)) = 1 ∧ arenaObs occB ((hopFlow J ħ).arenaFlow (hopTime J ħ) (msgPoint 0)) = 0

★★★ At τ_hop the receiver's readout is 1 for message 1 and 0 for message 0.

theorem CSD.CV.partial_transfer_before_hopTime {J ħ t : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (ht : 0 < t) (ht' : t < hopTime J ħ) : 0 < arenaObs occB ((hopFlow J ħ).arenaFlow t (msgPoint 1)) ∧ arenaObs occB ((hopFlow J ħ).arenaFlow t (msgPoint 1)) < 1

★ Partial transfer before τ_hop: for 0 < t < τ_hop the readout is strictly between 0 and 1 — complete transfer at τ_hop does not mean silence at earlier times.

theorem CSD.CV.influence_of_message {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : arenaObs occB ((hopFlow J ħ).arenaFlow (hopTime J ħ) (msgPoint 1)) ≠ arenaObs occB ((hopFlow J ħ).arenaFlow (hopTime J ħ) (msgPoint 0))

Causal influence by comparison of preparations: the two message points differ only in the occupancy of A (msgConfig_siteB), and at τ_hop their receiver readouts differ.

The package

theorem CSD.CV.signal_exchange {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (hopFlow J ħ).edges = {(0, 1)} ∧ (Matrix.toEuclideanLin ↑((hopFlow J ħ).flow (hopTime J ħ))) (basisVec excA) = -Complex.I • basisVec excB ∧ arenaObs occB ((hopFlow J ħ).arenaFlow (hopTime J ħ) (msgPoint 1)) = 1 ∧ arenaObs occB ((hopFlow J ħ).arenaFlow (hopTime J ħ) (msgPoint 0)) = 0 ∧ (∀ (t : ℝ), 0 < t → t < hopTime J ħ → 0 < arenaObs occB ((hopFlow J ħ).arenaFlow t (msgPoint 1)) ∧ arenaObs occB ((hopFlow J ħ).arenaFlow t (msgPoint 1)) < 1) ∧ 0 < roundTrip J ħ ∧ (hopFlow J ħ).arenaFlow (roundTrip J ħ) (msgPoint 1) = msgPoint 1

★★★ The signal exchange. The hop is a field-structured flow; at τ_hop = πħ/2J the excitation at A has become −i times the excitation at B and the receiver's readout is 1 for message 1 and 0 for message 0; before τ_hop the transfer is partial; at the nonzero round trip 2 τ_hop the arena point is the message point again.