The scheduled chain: exact transfer along L sites, and clock delay against graph distance

Category: 3-Local (CV; the network witness of the clock-and-echo programme). BACKLOG #190 (out of #39; the residue of #188).

A uniform hopping Hamiltonian on a chain does not carry an excitation perfectly from end to end (dispersion). Exact transmission along L = n + 1 sites needs a sequentially activated coupling schedule: the hop on edge (k, k+1) is switched on for one hop time τ_hop, in order, and nothing else is ever on. This module builds that schedule as a visible modelling input and proves what it transmits.

• swapSites k k', ★ swapHop k k' — the local hop on an arbitrary edge: the exchange σ⁺_k σ⁻_{k'} + σ⁻_k σ⁺_{k'} on every background, i.e. the swap permutation matrix with its diagonal removed. swapHop_mul_swapHop (X² = P, the projector on the configurations the edge moves), swapHop_mul_swapProj, swapHop_conjTranspose, and ★ swapHop_supportedOn — the hop is supported on its edge, which the two-site hop of SignalExchange.lean never had to show;
• edgeFlow J ħ k k' : FieldStructuredFlow L 2 — one coupling edge carrying the hop; ★★ edgeFlow_val_eq — its flow in closed form, 1 + (cos θ − 1) P − i sin θ · X, by the ODE uniqueness of ExpUnique.lean; toEuclideanLin_edgeFlow_single — on a configuration the edge moves, cos θ · e_c − i sin θ · e_{swap c}; on one it does not move, the identity; ★★ edgeFlow_transfer — at τ_hop the excitation at k is −i times the excitation at k';
• Schedule K N — the scheduled generator: a sequence of field-structured flows, one per stage of duration τ; Schedule.completed m (the product of the first m stages, in order), Schedule.propagator t (the completed stages below t and the running one, from switch-on at 0), Schedule.evolve s t = propagator t · (propagator s)⁻¹ with the two-time law (evolve_self, evolve_comp) — a two-parameter dynamics, not a one-parameter group; propagator_at_stage: at m τ the propagator is the completed product;
• chainSchedule n J ħ : Schedule (n+1) 2 — the chain's schedule: stage m < n is the edge flow on (m, m+1), every later stage is off (FieldStructuredFlow.off); its active edges are visible (chainSchedule_edges_of_lt, chainSchedule_edges_of_le) and lie on the path graph;
• ★★★ chain_transfer — exact transfer with the accumulated phase: at m τ_hop the excitation prepared at site 0 is (−i)^m times the excitation at site m, for every m ≤ n; in particular it reaches the far end at n τ_hop = (L − 1) τ_hop with phase (−i)^{L−1} (chain_transfer_last); propagator_vac — the vacuum never moves;
• occAt k, chainMsg n b, ★★ chainReadout_one, chainReadout_zero, ★★★ receiver_distinguishes_chain — at k τ_hop the readout at site k is 1 for message 1 and 0 for message 0, and excitation_position: at m τ_hop the excitation is sharply at site m and nowhere else;
• pathGraph n, ★ mem_graphBall_pathGraph — the path graph's balls about site 0 are the initial segments; graphDist E R k — the graph distance as the least radius whose ball contains k; ★★ graphDist_pathGraph : graphDist (pathGraph n) {0} k = k;
• ★★★ scheduled_chain — the package.

Drift check

The schedule is a modelling input, exactly as the brief warned: the dynamics that transmits is the sequence of edge flows, each a field-structured flow in the sense of FieldStructuredFlow.lean, and the row's own light cone (FieldStructuredFlow.lightcone) applies stage by stage. Nothing here is a record; the clocks at the sites and the comparison of their readings with the graph distance are RecordLayer/ChainClocks.lean. Successful transmission is a readout at a stated time; it is not a propagation bound.

Honest scope

• One excitation; the message is a one-bit occupancy at site 0; the receiver at site k reads "the excitation sits at k", the basis projector of SignalExchange.lean, which coincides with the local occupancy on every state this dynamics reaches from the two preparations.
• The phase (−i)^m is relative to the chosen basis vectors; it is a theorem about this schedule, not an invariant of the chain.
• J and ħ are positive reals in consistent units; no numerical value is derived from either.
• Switch-on is at 0: before it the propagator is the identity (propagator_of_nonpos), the convention of RecordedExchange.lean's hopOn.

References: specs/BACKLOG.md #190, #188, #183, #186, #39; CV/SignalExchange.lean, CV/FieldStructuredFlow.lean, CV/SupportSpreading.lean (graphBall), CV/TwoCones.lean (exists_dist_le_of_mem_graphBall), Mathlib/Analysis/Normed/Algebra/ExpUnique.lean.

Configurations on L sites

@[reducible, inline]

abbrev CSD.CV.ChainConfig (L : ℕ) : Type

L sites, occupancy 0 or 1.

Equations

• CSD.CV.ChainConfig L = CSD.CV.FieldConfig L 2

def CSD.CV.vacL (L : ℕ) : ChainConfig L

The vacuum.

Equations

• CSD.CV.vacL L x✝ = 0

def CSD.CV.excAt {L : ℕ} (k : Fin L) : ChainConfig L

One excitation at site k.

Equations

• CSD.CV.excAt k = Pi.single k 1

theorem CSD.CV.excAt_apply_self {L : ℕ} (k : Fin L) : excAt k k = 1

theorem CSD.CV.excAt_apply_of_ne {L : ℕ} {k j : Fin L} (h : j ≠ k) : excAt k j = 0

theorem CSD.CV.excAt_injective {L : ℕ} : Function.Injective excAt

theorem CSD.CV.vacL_apply {L : ℕ} (k : Fin L) : vacL L k = 0

theorem CSD.CV.excAt_ne_vacL {L : ℕ} (k : Fin L) : excAt k ≠ vacL L

def CSD.CV.swapSites {L : ℕ} (k k' : Fin L) (c : ChainConfig L) : ChainConfig L

The configuration with sites k and k' exchanged.

Equations

• CSD.CV.swapSites k k' c = c ∘ ⇑(Equiv.swap k k')

theorem CSD.CV.swapSites_apply_left {L : ℕ} (k k' : Fin L) (c : ChainConfig L) : swapSites k k' c k = c k'

theorem CSD.CV.swapSites_apply_right {L : ℕ} (k k' : Fin L) (c : ChainConfig L) : swapSites k k' c k' = c k

theorem CSD.CV.swapSites_apply_of_ne {L : ℕ} (k k' : Fin L) (c : ChainConfig L) {j : Fin L} (hj : j ≠ k) (hj' : j ≠ k') : swapSites k k' c j = c j

theorem CSD.CV.swapSites_swapSites {L : ℕ} (k k' : Fin L) (c : ChainConfig L) : swapSites k k' (swapSites k k' c) = c

theorem CSD.CV.swapSites_ne_self {L : ℕ} {k k' : Fin L} {c : ChainConfig L} (hc : c k ≠ c k') : swapSites k k' c ≠ c

theorem CSD.CV.eq_swapSites_iff {L : ℕ} {k k' : Fin L} {c d : ChainConfig L} (hoff : ∀ (j : Fin L), j ≠ k → j ≠ k' → c j = d j) : d = swapSites k k' c ↔ d k = c k' ∧ d k' = c k

The swapped configuration, characterised on the two sites when the spectators agree.

theorem CSD.CV.swap_cond_symm {L : ℕ} {k k' : Fin L} {c d : ChainConfig L} (h : c = swapSites k k' d ∧ d k ≠ d k') : d = swapSites k k' c ∧ c k ≠ c k'

The hop's defining condition is symmetric in its two configurations.

theorem CSD.CV.swapSites_excAt {L : ℕ} (k k' : Fin L) : swapSites k k' (excAt k) = excAt k'

The hop on an edge, and the projector on what it moves

noncomputable def CSD.CV.swapHop {L : ℕ} (k k' : Fin L) : Matrix (ChainConfig L) (ChainConfig L) ℂ

★ The local hop on the edge (k, k'): σ⁺_k σ⁻_{k'} + σ⁻_k σ⁺_{k'} on every background — the swap permutation matrix with its diagonal removed.

Equations

• CSD.CV.swapHop k k' = Matrix.of fun (c d : CSD.CV.ChainConfig L) => if d = CSD.CV.swapSites k k' c ∧ c k ≠ c k' then 1 else 0

noncomputable def CSD.CV.swapProj {L : ℕ} (k k' : Fin L) : Matrix (ChainConfig L) (ChainConfig L) ℂ

The projector on the configurations the edge moves.

Equations

• CSD.CV.swapProj k k' = Matrix.diagonal fun (c : CSD.CV.ChainConfig L) => if c k ≠ c k' then 1 else 0

theorem CSD.CV.swapHop_apply {L : ℕ} (k k' : Fin L) (c d : ChainConfig L) : swapHop k k' c d = if d = swapSites k k' c ∧ c k ≠ c k' then 1 else 0

theorem CSD.CV.swapHop_apply_symm {L : ℕ} (k k' : Fin L) (c d : ChainConfig L) : swapHop k k' d c = if d = swapSites k k' c ∧ c k ≠ c k' then 1 else 0

The hop's entries read the same from either side.

theorem CSD.CV.swapHop_mul_swapHop {L : ℕ} (k k' : Fin L) : swapHop k k' * swapHop k k' = swapProj k k'

theorem CSD.CV.swapHop_mul_swapProj {L : ℕ} (k k' : Fin L) : swapHop k k' * swapProj k k' = swapHop k k'

theorem CSD.CV.swapHop_conjTranspose {L : ℕ} (k k' : Fin L) : (swapHop k k').conjTranspose = swapHop k k'

theorem CSD.CV.swapHop_supportedOn {L : ℕ} (k k' : Fin L) : SupportedOn {k, k'} (swapHop k k')

★ The hop is supported on its edge: it does not move the spectators, and its entries do not depend on them.

The edge flow

noncomputable def CSD.CV.chainGen {L : ℕ} (J ħ : ℝ) (k k' : Fin L) : Matrix (ChainConfig L) (ChainConfig L) ℂ

The Schrödinger generator −(i J/ħ) X of the hop on the edge (k, k').

Equations

• CSD.CV.chainGen J ħ k k' = -(Complex.I * ↑(J / ħ)) • CSD.CV.swapHop k k'

theorem CSD.CV.chainGen_skew {L : ℕ} (J ħ : ℝ) (k k' : Fin L) : (chainGen J ħ k k').conjTranspose = -chainGen J ħ k k'

noncomputable def CSD.CV.edgeFlow {L : ℕ} (J ħ : ℝ) (k k' : Fin L) : FieldStructuredFlow L 2

The field-structured flow with the one coupling edge (k, k') carrying the hop.

Equations

• CSD.CV.edgeFlow J ħ k k' = { edges := {(k, k')}, piece := fun (x : Fin L × Fin L) => CSD.CV.chainGen J ħ k k', piece_supported := ⋯, gen_skew := ⋯ }

theorem CSD.CV.edgeFlow_edges {L : ℕ} (J ħ : ℝ) (k k' : Fin L) : (edgeFlow J ħ k k').edges = {(k, k')}

theorem CSD.CV.edgeFlow_val {L : ℕ} (J ħ : ℝ) (k k' : Fin L) (t : ℝ) : ↑((edgeFlow J ħ k k').flow t) = NormedSpace.exp (t • chainGen J ħ k k')

theorem CSD.CV.smul_chainGen {L : ℕ} (J ħ : ℝ) (k k' : Fin L) (t : ℝ) : t • chainGen J ħ k k' = (↑(-hopAngle J ħ t) * Complex.I) • swapHop k k'

theorem CSD.CV.edgeFlow_val_eq {L : ℕ} (J ħ : ℝ) (k k' : Fin L) (t : ℝ) : ↑((edgeFlow J ħ k k').flow t) = 1 + ↑(Real.cos (hopAngle J ħ t) - 1) • swapProj k k' + -(Complex.I * ↑(Real.sin (hopAngle J ħ t))) • swapHop k k'

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

theorem CSD.CV.edgeFlow_mulVec_single {L : ℕ} (J ħ : ℝ) {k k' : Fin L} {c : ChainConfig L} (hc : c k ≠ c k') (t : ℝ) : (↑((edgeFlow J ħ k k').flow t)).mulVec (Pi.single c 1) = ↑(Real.cos (hopAngle J ħ t)) • Pi.single c 1 + -(Complex.I * ↑(Real.sin (hopAngle J ħ t))) • Pi.single (swapSites k k' c) 1

On a configuration the edge moves, the flow produces cos θ · e_c − i sin θ · e_{swap c}.

theorem CSD.CV.edgeFlow_mulVec_single_of_eq {L : ℕ} (J ħ : ℝ) {k k' : Fin L} {c : ChainConfig L} (hc : c k = c k') (t : ℝ) : (↑((edgeFlow J ħ k k').flow t)).mulVec (Pi.single c 1) = Pi.single c 1

On a configuration the edge does not move, the flow is the identity.

Euclidean form

noncomputable def CSD.CV.eVec {L : ℕ} (c : ChainConfig L) : EuclideanSpace ℂ (ChainConfig L)

The basis vector of a configuration.

Equations

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

theorem CSD.CV.eVec_apply {L : ℕ} (c d : ChainConfig L) : (eVec c).ofLp d = Pi.single c 1 d

theorem CSD.CV.eVec_apply_self {L : ℕ} (c : ChainConfig L) : (eVec c).ofLp c = 1

theorem CSD.CV.eVec_apply_of_ne {L : ℕ} {c d : ChainConfig L} (h : d ≠ c) : (eVec c).ofLp d = 0

theorem CSD.CV.norm_eVec {L : ℕ} (c : ChainConfig L) : ‖eVec c‖ = 1

theorem CSD.CV.eVec_ne_zero {L : ℕ} (c : ChainConfig L) : eVec c ≠ 0

theorem CSD.CV.toEuclideanLin_mul_apply {L : ℕ} (A B : Matrix (ChainConfig L) (ChainConfig L) ℂ) (v : EuclideanSpace ℂ (ChainConfig L)) : (Matrix.toEuclideanLin (A * B)) v = (Matrix.toEuclideanLin A) ((Matrix.toEuclideanLin B) v)

theorem CSD.CV.toEuclideanLin_one_apply {L : ℕ} (v : EuclideanSpace ℂ (ChainConfig L)) : (Matrix.toEuclideanLin 1) v = v

theorem CSD.CV.toEuclideanLin_edgeFlow_single {L : ℕ} (J ħ : ℝ) {k k' : Fin L} {c : ChainConfig L} (hc : c k ≠ c k') (t : ℝ) : (Matrix.toEuclideanLin ↑((edgeFlow J ħ k k').flow t)) (eVec c) = ↑(Real.cos (hopAngle J ħ t)) • eVec c + -(Complex.I * ↑(Real.sin (hopAngle J ħ t))) • eVec (swapSites k k' c)

theorem CSD.CV.toEuclideanLin_edgeFlow_single_of_eq {L : ℕ} (J ħ : ℝ) {k k' : Fin L} {c : ChainConfig L} (hc : c k = c k') (t : ℝ) : (Matrix.toEuclideanLin ↑((edgeFlow J ħ k k').flow t)) (eVec c) = eVec c

theorem CSD.CV.edgeFlow_transfer {L : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {k k' : Fin L} (h : k ≠ k') : (Matrix.toEuclideanLin ↑((edgeFlow J ħ k k').flow (hopTime J ħ))) (eVec (excAt k)) = -Complex.I • eVec (excAt k')

★★ One stage transfers exactly, with phase −i: at τ_hop the excitation at k has become −i times the excitation at k'.

theorem CSD.CV.edgeFlow_vac {L : ℕ} (J ħ : ℝ) (k k' : Fin L) (t : ℝ) : (Matrix.toEuclideanLin ↑((edgeFlow J ħ k k').flow t)) (eVec (vacL L)) = eVec (vacL L)

The scheduled generator

def CSD.CV.FieldStructuredFlow.off (K N : ℕ) : FieldStructuredFlow K N

The flow with nothing switched on.

Equations

• CSD.CV.FieldStructuredFlow.off K N = { edges := ∅, piece := fun (x : Fin K × Fin K) => 0, piece_supported := ⋯, gen_skew := ⋯ }

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

theorem CSD.CV.FieldStructuredFlow.off_flow {K N : ℕ} (t : ℝ) : (off K N).flow t = 1

structure CSD.CV.Schedule (K N : ℕ) : Type

A coupling schedule: a sequence of field-structured flows, stage m switched on for the duration τ after the first m stages. The scheduled generator is piecewise in time — a modelling input, stated as data.

• stage : ℕ → FieldStructuredFlow K N

  The field-structured flow switched on during stage m.

• τ : ℝ

  The duration of each stage.

noncomputable def CSD.CV.Schedule.completed {K N : ℕ} (s : Schedule K N) : ℕ → ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

The product of the first m completed stages, in order: U_{m−1}(τ) ⋯ U_0(τ).

Equations

• s.completed 0 = 1
• s.completed m.succ = (s.stage m).flow s.τ * s.completed m

@[simp]

theorem CSD.CV.Schedule.completed_zero {K N : ℕ} (s : Schedule K N) : s.completed 0 = 1

theorem CSD.CV.Schedule.completed_succ {K N : ℕ} (s : Schedule K N) (m : ℕ) : s.completed (m + 1) = (s.stage m).flow s.τ * s.completed m

noncomputable def CSD.CV.Schedule.propagator {K N : ℕ} (s : Schedule K N) (t : ℝ) : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

The propagator from switch-on at 0: the completed stages below t and the running stage for the remaining time. Before switch-on it is the identity.

Equations

• s.propagator t = (s.stage ⌊max t 0 / s.τ⌋₊).flow (max t 0 - ↑⌊max t 0 / s.τ⌋₊ * s.τ) * s.completed ⌊max t 0 / s.τ⌋₊

noncomputable def CSD.CV.Schedule.evolve {K N : ℕ} (s : Schedule K N) (a b : ℝ) : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

The two-time propagator from a to b.

Equations

• s.evolve a b = s.propagator b * (s.propagator a)⁻¹

theorem CSD.CV.Schedule.evolve_self {K N : ℕ} (s : Schedule K N) (t : ℝ) : s.evolve t t = 1

theorem CSD.CV.Schedule.evolve_comp {K N : ℕ} (s : Schedule K N) (a b c : ℝ) : s.evolve b c * s.evolve a b = s.evolve a c

★ The two-time composition law of the scheduled dynamics.

theorem CSD.CV.Schedule.propagator_of_nonpos {K N : ℕ} (s : Schedule K N) {t : ℝ} (ht : t ≤ 0) : s.propagator t = 1

theorem CSD.CV.Schedule.evolve_zero {K N : ℕ} (s : Schedule K N) (t : ℝ) : s.evolve 0 t = s.propagator t

theorem CSD.CV.Schedule.propagator_at_stage {K N : ℕ} (s : Schedule K N) (hτ : 0 < s.τ) (m : ℕ) : s.propagator (↑m * s.τ) = s.completed m

At the stage boundary m τ the propagator is the completed product.

The chain's schedule

noncomputable def CSD.CV.chainSchedule (n : ℕ) (J ħ : ℝ) : Schedule (n + 1) 2

The chain's schedule on n + 1 sites: stage m < n is the edge flow on (m, m+1); every later stage is off.

Equations

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

theorem CSD.CV.chainSchedule_τ {n : ℕ} (J ħ : ℝ) : (chainSchedule n J ħ).τ = hopTime J ħ

theorem CSD.CV.chainSchedule_stage_of_lt {n : ℕ} (J ħ : ℝ) {m : ℕ} (h : m < n) : (chainSchedule n J ħ).stage m = edgeFlow J ħ ⟨m, h⟩.castSucc ⟨m, h⟩.succ

theorem CSD.CV.chainSchedule_stage_of_le {n : ℕ} (J ħ : ℝ) {m : ℕ} (h : n ≤ m) : (chainSchedule n J ħ).stage m = FieldStructuredFlow.off (n + 1) 2

theorem CSD.CV.chainSchedule_edges_of_lt {n : ℕ} (J ħ : ℝ) {m : ℕ} (h : m < n) : ((chainSchedule n J ħ).stage m).edges = {(⟨m, h⟩.castSucc, ⟨m, h⟩.succ)}

The active edges are visible: during stage m < n exactly the edge (m, m+1) is on.

theorem CSD.CV.chainSchedule_edges_of_le {n : ℕ} (J ħ : ℝ) {m : ℕ} (h : n ≤ m) : ((chainSchedule n J ħ).stage m).edges = ∅

After the last stage nothing is on.

theorem CSD.CV.chain_transfer_completed {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (m : ℕ) (hm : m ≤ n) : (Matrix.toEuclideanLin ↑((chainSchedule n J ħ).completed m)) (eVec (excAt 0)) = (-Complex.I) ^ m • eVec (excAt ⟨m, ⋯⟩)

★★★ Exact transfer with the accumulated phase: after m ≤ n completed stages the excitation prepared at site 0 is (−i)^m times the excitation at site m.

theorem CSD.CV.chain_transfer {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {m : ℕ} (hm : m ≤ n) : (Matrix.toEuclideanLin ↑((chainSchedule n J ħ).propagator (↑m * hopTime J ħ))) (eVec (excAt 0)) = (-Complex.I) ^ m • eVec (excAt ⟨m, ⋯⟩)

★★★ Exact transfer along the chain: at m τ_hop (m ≤ n) the propagator carries the excitation at site 0 to (−i)^m times the excitation at site m.

theorem CSD.CV.chain_transfer_last {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (Matrix.toEuclideanLin ↑((chainSchedule n J ħ).propagator (↑n * hopTime J ħ))) (eVec (excAt 0)) = (-Complex.I) ^ n • eVec (excAt (Fin.last n))

The far end: in n τ_hop = (L − 1) τ_hop the excitation reaches the last site with phase (−i)^{L−1}.

theorem CSD.CV.propagator_vac {n : ℕ} (J ħ t : ℝ) : (Matrix.toEuclideanLin ↑((chainSchedule n J ħ).propagator t)) (eVec (vacL (n + 1))) = eVec (vacL (n + 1))

The vacuum never moves, at any time.

Arena points and the receivers' readouts

noncomputable def CSD.CV.occAt {L : ℕ} (k : Fin L) : Matrix (ChainConfig L) (ChainConfig L) ℂ

The receiver at site k reads "the excitation sits at k".

Equations

• CSD.CV.occAt k = Matrix.single (CSD.CV.excAt k) (CSD.CV.excAt k) 1

def CSD.CV.chainMsgConfig (n : ℕ) : Fin 2 → ChainConfig (n + 1)

The sender's message b is the occupancy of site 0; every other site is empty.

Equations

• CSD.CV.chainMsgConfig n = ![CSD.CV.vacL (n + 1), CSD.CV.excAt 0]

theorem CSD.CV.chainMsgConfig_zero {n : ℕ} : chainMsgConfig n 0 = vacL (n + 1)

theorem CSD.CV.chainMsgConfig_one {n : ℕ} : chainMsgConfig n 1 = excAt 0

theorem CSD.CV.chainMsgConfig_apply_of_ne {n : ℕ} (b : Fin 2) {j : Fin (n + 1)} (hj : j ≠ 0) : chainMsgConfig n b j = 0

The two preparations agree away from site 0.

noncomputable def CSD.CV.chainMsg (n : ℕ) (b : Fin 2) : FieldArena (n + 1) 2

The arena point of message b.

Equations

• CSD.CV.chainMsg n b = Projectivization.mk ℂ (CSD.CV.eVec (CSD.CV.chainMsgConfig n b)) ⋯

theorem CSD.CV.chainMsg_zero {n : ℕ} : chainMsg n 0 = Projectivization.mk ℂ (eVec (vacL (n + 1))) ⋯

theorem CSD.CV.chainMsg_one {n : ℕ} : chainMsg n 1 = Projectivization.mk ℂ (eVec (excAt 0)) ⋯

noncomputable def CSD.CV.chainArenaFlow {n : ℕ} (J ħ t : ℝ) (p : FieldArena (n + 1) 2) : FieldArena (n + 1) 2

The scheduled flow on the arena, from switch-on.

Equations

• CSD.CV.chainArenaFlow J ħ t p = CSD.CV.arenaKick ((CSD.CV.chainSchedule n J ħ).propagator t) p

theorem CSD.CV.norm_pow_neg_I_smul_eVec {L : ℕ} (m : ℕ) (c : ChainConfig L) : ‖(-Complex.I) ^ m • eVec c‖ = 1

theorem CSD.CV.chainReadout_one {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {m : ℕ} (hm : m ≤ n) (k : Fin (n + 1)) : arenaObs (occAt k) (chainArenaFlow J ħ (↑m * hopTime J ħ) (chainMsg n 1)) = if k = ⟨m, ⋯⟩ then 1 else 0

The receiver at k for message 1, at the stage boundary m τ_hop: 1 if k = m, 0 otherwise — the excitation is sharply at site m.

theorem CSD.CV.chainReadout_zero {n : ℕ} (J ħ t : ℝ) (k : Fin (n + 1)) : arenaObs (occAt k) (chainArenaFlow J ħ t (chainMsg n 0)) = 0

The receiver at k for message 0 is 0 at every time: the vacuum does not move.

theorem CSD.CV.receiver_distinguishes_chain {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (k : Fin (n + 1)) : arenaObs (occAt k) (chainArenaFlow J ħ (↑↑k * hopTime J ħ) (chainMsg n 1)) = 1 ∧ arenaObs (occAt k) (chainArenaFlow J ħ (↑↑k * hopTime J ħ) (chainMsg n 0)) = 0

★★★ At k τ_hop the receiver at site k reads 1 for message 1 and 0 for message 0.

theorem CSD.CV.excitation_position {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {m : ℕ} (hm : m ≤ n) {k : Fin (n + 1)} (hk : k ≠ ⟨m, ⋯⟩) : arenaObs (occAt k) (chainArenaFlow J ħ (↑m * hopTime J ħ) (chainMsg n 1)) = 0

The excitation's position: at m τ_hop the readout at any other site is 0.

The path graph and the graph distance

def CSD.CV.pathGraph (n : ℕ) : Finset (Fin (n + 1) × Fin (n + 1))

The path graph on n + 1 sites: the edges (k, k+1).

Equations

• CSD.CV.pathGraph n = Finset.image (fun (k : Fin n) => (k.castSucc, k.succ)) Finset.univ

theorem CSD.CV.mem_pathGraph {n : ℕ} {e : Fin (n + 1) × Fin (n + 1)} : e ∈ pathGraph n ↔ ∃ (k : Fin n), e = (k.castSucc, k.succ)

theorem CSD.CV.chainSchedule_edges_subset {n : ℕ} (J ħ : ℝ) (m : ℕ) : ((chainSchedule n J ħ).stage m).edges ⊆ pathGraph n

The schedule's active edges all lie on the path graph.

theorem CSD.CV.pathGraph_one : pathGraph 1 = {(0, 1)}

The path graph on two sites is the hop graph of the two-site exchange.

theorem CSD.CV.mem_graphBall_pathGraph {n : ℕ} (d : ℕ) (j : Fin (n + 1)) : j ∈ graphBall (pathGraph n) {0} d ↔ ↑j ≤ d

★ The path graph's balls about site 0 are the initial segments.

noncomputable def CSD.CV.graphDist {K : ℕ} (E : Finset (Fin K × Fin K)) (R : Finset (Fin K)) (k : Fin K) : ℕ

The graph distance from a region to a site: the least radius whose graph ball contains it.

Equations

• CSD.CV.graphDist E R k = sInf {d : ℕ | k ∈ CSD.CV.graphBall E R d}

theorem CSD.CV.graphDist_le_of_mem {K : ℕ} {E : Finset (Fin K × Fin K)} {R : Finset (Fin K)} {k : Fin K} {d : ℕ} (h : k ∈ graphBall E R d) : graphDist E R k ≤ d

theorem CSD.CV.le_graphDist {K : ℕ} {E : Finset (Fin K × Fin K)} {R : Finset (Fin K)} {k : Fin K} {d : ℕ} (hne : ∃ (d' : ℕ), k ∈ graphBall E R d') (h : ∀ (d' : ℕ), k ∈ graphBall E R d' → d ≤ d') : d ≤ graphDist E R k

theorem CSD.CV.graphDist_pathGraph {n : ℕ} (k : Fin (n + 1)) : graphDist (pathGraph n) {0} k = ↑k

★★ On the path graph the graph distance from site 0 to site k is k.

The package

theorem CSD.CV.scheduled_chain {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) : (∀ (m : ℕ) (h : m < n), ((chainSchedule n J ħ).stage m).edges = {(⟨m, h⟩.castSucc, ⟨m, h⟩.succ)}) ∧ (∀ (m : ℕ), n ≤ m → ((chainSchedule n J ħ).stage m).edges = ∅) ∧ (∀ (a b c : ℝ), (chainSchedule n J ħ).evolve b c * (chainSchedule n J ħ).evolve a b = (chainSchedule n J ħ).evolve a c) ∧ (∀ (m : ℕ) (hm : m ≤ n), (Matrix.toEuclideanLin ↑((chainSchedule n J ħ).propagator (↑m * hopTime J ħ))) (eVec (excAt 0)) = (-Complex.I) ^ m • eVec (excAt ⟨m, ⋯⟩)) ∧ (∀ (k : Fin (n + 1)), arenaObs (occAt k) (chainArenaFlow J ħ (↑↑k * hopTime J ħ) (chainMsg n 1)) = 1 ∧ arenaObs (occAt k) (chainArenaFlow J ħ (↑↑k * hopTime J ħ) (chainMsg n 0)) = 0) ∧ ∀ (k : Fin (n + 1)), graphDist (pathGraph n) {0} k = ↑k

★★★ The scheduled chain. The schedule's active edges are visible and lie on the path graph; the two-time law holds; at m τ_hop the excitation prepared at site 0 is (−i)^m times the excitation at site m; at k τ_hop the receiver at k reads 1 for message 1 and 0 for message 0; and the graph distance from site 0 to site k is k.