The recorded exchange: clock, signal and three records on one arena, with one evolution

Category: 7-SigmaLayer (the record layer — the common arena of the clock-and-echo programme). BACKLOG #186 (out of #39; the fourth of #183–#189, the price driver).

#183 built the signal (a two-site hop on FieldArena 2 2), #185 the clock (ClockArena K). This file puts them on one arena with one evolution and adds the three record registers the experiment needs — emission at A, reception at B, return at A — each written by the record mechanism of ShearWitness.lean: a pointer translated by shearAmt 2 b from the ready arc into the pointer arc of the bit b it reads. A register is written on the crossing of its readout time, by the bit read off the exchange state at that time; the hop is switched on at t = 0, the apparatus is prepared at t = −1.

• XArena K = FieldArena 2 2 × ClockArena K × (Fin 3 → KTorus); hopOn, arrived, readTime, readSite, readBit (the occupancy weight of a site, thresholded at 1/2, measurable by measurable_momentMap); xEvolve J ħ T s t — the joint two-time propagator;
• xEvolve_self, ★★ xEvolve_comp — the two-time law holds on the common arena: the bit a register reads is the exchange state at its readout time, which the group law of the hop makes independent of where the propagator is cut; measurable_xEvolve; ★ xEvolve_measurePreserving — Liouville (Fubini–Study × Haar × Haar) is preserved: it is a dynamics;
• XReady, xPrep b c r — the ready preparation with message b; register_before, ★★ register_written — each register is written with the message, emission at 0, reception at τ_hop, return at 2 τ_hop, from the actual transfer (arenaFlow_hopTime, arenaFlow_roundTrip) and nothing else; register_frozen;
• recordProtocol i — each register is a MeasurementProtocol, recordProtocol_pointerInvariant, ★ record_persists through the corpus's record_persists_on_interval;
• ★★ reception_depends_on_message, return_depends_on_message — demonstrated influence: two preparations differing only in the message (msgConfig_siteB) leave the reception register, and the return register, in disjoint pointer arcs;
• Occurrence, emission, reception, returnOcc, eventOf — occurrences with their register, site, time and message, and the forgetful map to CV.RecordEvent, whose period label is the tick count of the physical clock in the arena at the occurrence time (eventOf_emission, eventOf_reception, eventOf_return under the stated calibration T = τ_hop);
• ★★ causal_chain — emission ⪯ reception ⪯ return under CausalPrecedes on the coupling graph {(A, B)}, and emission ⪯ return by the corpus's transitivity;
• recordEvents, recordPattern, ★ factorsThrough_recordEvents — the record predicates factor through a macroscopic projection, the pattern projection of MacroProjection.lean;
• ★★★ recorded_exchange — the package.

The two clocks, identified explicitly

RecordEvent.time is a period index; the clock reads a tick count. They coincide here by a stated modelling choice: the clock period is the hop time, T = τ_hop, so emission, reception and return fall at ticks 0, 1, 2 (tickCount_at_period). With another period the same occurrences carry other labels; nothing identifies the two clocks dynamically.

Honest scope

• ⚠️ The readout times and the switch-on are a schedule, a modelling input indexed by t_Σ, as in #185. The writes are triggered by the schedule reading the exchange state; a dynamical trigger is not built.
• ⚠️ CausalPrecedes is permitted influence on an assumed graph; the demonstrated influence is reception_depends_on_message. Both are proved; neither is inferred from the other.
• The bit is read by thresholding an occupancy weight at 1/2. At the readout times the exchange state is a basis ray, so the weight is 0 or 1 and the threshold is never close; between them it is not read.
• No metric, no volume element on the event order, no universal c: the scoping note's §8 stands.

References: specs/BACKLOG.md #186, #183, #185, #187, #39; CV/SignalExchange.lean, RecordLayer/RecordClock.lean, CV/RecordCausalOrder.lean (RecordEvent, CausalPrecedes), RecordLayer/MacroProjection.lean (patternProjection, factorsThrough_patternMap), RecordLayer/ShearWitness.lean (the arcs and shearAmt), RecordLayer/RecordPersistence.lean.

The common arena

@[reducible, inline]

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

The experiment's arena: the exchange, the clock, and three record registers (0 emission at A, 1 reception at B, 2 return at A).

Equations

• CSD.RecordLayer.XArena K = (CSD.CV.FieldArena 2 2 × CSD.RecordLayer.ClockArena K × (Fin 3 → CSD.LF4.KTorus))

noncomputable def CSD.RecordLayer.hopOn (u : ℝ) : ℝ

The hop coupling is switched on at t = 0: the exchange has run for hopOn u by time u.

Equations

• CSD.RecordLayer.hopOn u = max u 0

theorem CSD.RecordLayer.hopOn_of_nonneg {u : ℝ} (hu : 0 ≤ u) : hopOn u = u

theorem CSD.RecordLayer.hopOn_of_nonpos {u : ℝ} (hu : u ≤ 0) : hopOn u = 0

noncomputable def CSD.RecordLayer.arrived (τ t : ℝ) : ℝ

1 once the readout time τ has arrived, 0 before.

Equations

• CSD.RecordLayer.arrived τ t = if τ ≤ t then 1 else 0

theorem CSD.RecordLayer.arrived_of_le {τ t : ℝ} (h : τ ≤ t) : arrived τ t = 1

theorem CSD.RecordLayer.arrived_of_lt {τ t : ℝ} (h : t < τ) : arrived τ t = 0

noncomputable def CSD.RecordLayer.readTime (J ħ : ℝ) : Fin 3 → ℝ

The readout times: emission at 0, reception at τ_hop, return at 2 τ_hop.

Equations

• CSD.RecordLayer.readTime J ħ = ![0, CSD.CV.hopTime J ħ, CSD.CV.roundTrip J ħ]

def CSD.RecordLayer.readSite : Fin 3 → Fin 2

The site each register reads: A, B, A.

Equations

• CSD.RecordLayer.readSite = ![0, 1, 0]

def CSD.RecordLayer.siteConfig : Fin 2 → CV.HopConfig

The one-excitation configuration of a site.

Equations

• CSD.RecordLayer.siteConfig = ![CSD.CV.excA, CSD.CV.excB]

theorem CSD.RecordLayer.readTime_zero (J ħ : ℝ) : readTime J ħ 0 = 0

theorem CSD.RecordLayer.readTime_one (J ħ : ℝ) : readTime J ħ 1 = CV.hopTime J ħ

theorem CSD.RecordLayer.readTime_two (J ħ : ℝ) : readTime J ħ 2 = CV.roundTrip J ħ

theorem CSD.RecordLayer.readTime_nonneg {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (i : Fin 3) : 0 ≤ readTime J ħ i

noncomputable def CSD.RecordLayer.readBit (c : CV.HopConfig) (p : CV.FieldArena 2 2) : Fin 2

The bit read off a ray at a configuration: its occupancy weight thresholded at 1/2.

Equations

• CSD.RecordLayer.readBit c p = if 1 / 2 ≤ Projectivization.momentMap p c then 1 else 0

theorem CSD.RecordLayer.measurable_readBit (c : CV.HopConfig) : Measurable (readBit c)

The arena kick is the unitary action

theorem CSD.RecordLayer.arenaKick_eq_smul (U : ↥(Matrix.unitaryGroup CV.HopConfig ℂ)) (p : CV.FieldArena 2 2) : CV.arenaKick U p = U • p

theorem CSD.RecordLayer.measurable_arenaKick (U : ↥(Matrix.unitaryGroup CV.HopConfig ℂ)) : Measurable (CV.arenaKick U)

theorem CSD.RecordLayer.hopFlow_zero (J ħ : ℝ) : (CV.hopFlow J ħ).flow 0 = 1

theorem CSD.RecordLayer.arenaFlow_zero (J ħ : ℝ) (p : CV.FieldArena 2 2) : (CV.hopFlow J ħ).arenaFlow 0 p = p

theorem CSD.RecordLayer.measurable_arenaFlow (J ħ t : ℝ) : Measurable ((CV.hopFlow J ħ).arenaFlow t)

The joint propagator

noncomputable def CSD.RecordLayer.readAt (J ħ : ℝ) (i : Fin 3) (s : SigmaLayer.OnticTime) (p : CV.FieldArena 2 2) : Fin 2

The bit register i reads: the occupancy of its site in the exchange state at its readout time, when the propagator starts at s.

Equations

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

noncomputable def CSD.RecordLayer.xEvolve {K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) : XArena K → XArena K

The joint two-time propagator: the hop runs from switch-on, the clock runs on its schedule, and register i is translated by shearAmt 2 (bit) on the crossing of its readout time, the bit being read off the exchange state at that time.

Equations

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

theorem CSD.RecordLayer.xEvolve_exchange {K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (x : XArena K) : (xEvolve J ħ T s t x).1 = (CV.hopFlow J ħ).arenaFlow (hopOn t - hopOn s) x.1

theorem CSD.RecordLayer.xEvolve_clock {K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (x : XArena K) : (xEvolve J ħ T s t x).2.1 = clockEvolve T s t x.2.1

theorem CSD.RecordLayer.xEvolve_register {K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (x : XArena K) (i : Fin 3) : (xEvolve J ħ T s t x).2.2 i = pshift ((arrived (readTime J ħ i) t - arrived (readTime J ħ i) s) * shearAmt 2 (readAt J ħ i s x.1)) (x.2.2 i)

theorem CSD.RecordLayer.xEvolve_self {K : ℕ} (J ħ T : ℝ) (t : SigmaLayer.OnticTime) : xEvolve J ħ T t t = id

theorem CSD.RecordLayer.readAt_arenaFlow (J ħ : ℝ) (i : Fin 3) (s t : SigmaLayer.OnticTime) (p : CV.FieldArena 2 2) : readAt J ħ i t ((CV.hopFlow J ħ).arenaFlow (hopOn t - hopOn s) p) = readAt J ħ i s p

The bit read at the readout time does not depend on where the propagator is cut.

theorem CSD.RecordLayer.xEvolve_comp {K : ℕ} (J ħ T : ℝ) (s t u : SigmaLayer.OnticTime) : xEvolve J ħ T t u ∘ xEvolve J ħ T s t = xEvolve J ħ T s u

★★ The two-time composition law on the common arena.

theorem CSD.RecordLayer.measurable_xEvolve {K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) : Measurable (xEvolve J ħ T s t)

theorem CSD.RecordLayer.arenaFlow_measurePreserving (J ħ t : ℝ) (p₀ : CV.FieldArena 2 2) : MeasureTheory.MeasurePreserving ((CV.hopFlow J ħ).arenaFlow t) (Matrix.UnitaryGroup.fsMeasure p₀) (Matrix.UnitaryGroup.fsMeasure p₀)

The exchange factor preserves the Fubini–Study measure at every reference point.

theorem CSD.RecordLayer.xEvolve_measurePreserving {K : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena 2 2) : MeasureTheory.MeasurePreserving (xEvolve J ħ T s t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)

★ The joint propagator preserves Liouville measure — Fubini–Study on the exchange, Haar on the clock and the registers — for every reference point of the Fubini–Study measure: it is a dynamics. The register shifts depend on the exchange state, so this is a skew product.

The ready preparation and what the registers read

def CSD.RecordLayer.XReady (K : ℕ) : Set (XArena K)

The ready preparation: clock ready, all three registers in the ready arc.

Equations

• CSD.RecordLayer.XReady K = {x : CSD.RecordLayer.XArena K | x.2.1 ∈ CSD.RecordLayer.ClockReady K ∧ ∀ (i : Fin 3), x.2.2 i ∈ CSD.RecordLayer.readyArc 2}

noncomputable def CSD.RecordLayer.xPrep {K : ℕ} (b : Fin 2) (c : ClockArena K) (r : Fin 3 → LF4.KTorus) : XArena K

The preparation with message b: the exchange at the message point, clock and registers as given.

Equations

• CSD.RecordLayer.xPrep b c r = (CSD.CV.msgPoint b, c, r)

theorem CSD.RecordLayer.momentMap_msgPoint (b : Fin 2) (c : CV.HopConfig) : Projectivization.momentMap (CV.msgPoint b) c = if c = CV.msgConfig b then 1 else 0

The occupancy weight of a configuration at a message point is 1 at the message's configuration and 0 elsewhere.

theorem CSD.RecordLayer.momentMap_mk_basisVec (c c' : CV.HopConfig) : (Projectivization.mk ℂ (CV.basisVec c) ⋯).momentMap c' = if c' = c then 1 else 0

theorem CSD.RecordLayer.arenaFlow_msgPoint_zero (J ħ t : ℝ) : (CV.hopFlow J ħ).arenaFlow t (CV.msgPoint 0) = CV.msgPoint 0

The vacuum does not move: message 0's exchange point is fixed by the hop.

theorem CSD.RecordLayer.readBit_msgPoint_excA (b : Fin 2) : readBit CV.excA (CV.msgPoint b) = b

At A, the message point reads its message.

theorem CSD.RecordLayer.readAt_xPrep_zero (J ħ : ℝ) (b : Fin 2) : readAt J ħ 0 (-1) (CV.msgPoint b) = b

theorem CSD.RecordLayer.readAt_xPrep_one {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) : readAt J ħ 1 (-1) (CV.msgPoint b) = b

theorem CSD.RecordLayer.readAt_xPrep_two {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) : readAt J ħ 2 (-1) (CV.msgPoint b) = b

theorem CSD.RecordLayer.readAt_xPrep {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (i : Fin 3) (b : Fin 2) : readAt J ħ i (-1) (CV.msgPoint b) = b

★ Each register reads the message at its readout time: emission reads A at 0, reception reads B at τ_hop (the transfer), return reads A at 2 τ_hop (the Rabi return).

The records

theorem CSD.RecordLayer.pshift_shearAmt_mem_pointerArc {K' : ℕ} (i : Fin K') {q : LF4.KTorus} (hq : q ∈ readyArc K') : pshift (shearAmt K' i) q ∈ pointerArc K' i

A ready pointer shifted by shearAmt K i displays outcome i.

theorem CSD.RecordLayer.readyArc_disjoint_pointerArc {K' : ℕ} (i : Fin K') : Disjoint (readyArc K') (pointerArc K' i)

theorem CSD.RecordLayer.register_before {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {x : XArena K} (hx : x ∈ XReady K) (i : Fin 3) {t : SigmaLayer.OnticTime} (ht : t < readTime J ħ i) : (xEvolve J ħ T (-1) t x).2.2 i ∈ readyArc 2

Before its readout time a register is still ready.

theorem CSD.RecordLayer.register_written {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {c : ClockArena K} {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) (i : Fin 3) {t : SigmaLayer.OnticTime} (ht : readTime J ħ i ≤ t) : (xEvolve J ħ T (-1) t (xPrep b c r)).2.2 i ∈ pointerArc 2 b

★★ Each register is written with the message from its readout time on: emission at 0, reception at τ_hop, return at 2 τ_hop.

theorem CSD.RecordLayer.register_frozen {K : ℕ} (J ħ T : ℝ) {s t : SigmaLayer.OnticTime} (i : Fin 3) (hs : readTime J ħ i ≤ s) (hst : s ≤ t) (x : XArena K) : (xEvolve J ħ T s t x).2.2 i = x.2.2 i

After its readout time a register is frozen.

Each register is a measurement protocol; the records persist

noncomputable def CSD.RecordLayer.recordProtocol {K : ℕ} (J ħ T : ℝ) (i : Fin 3) (τR : ℝ) : MeasurementProtocol (XArena K) 2

Register i as a MeasurementProtocol with two outcomes (the bit), prepared at −1, read out at its readout time, with record lifetime τR.

Equations

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

theorem CSD.RecordLayer.recordProtocol_pointerInvariant {K : ℕ} (J ħ T : ℝ) (i : Fin 3) (τR : ℝ) : (recordProtocol J ħ T i τR).PointerInvariantOn

theorem CSD.RecordLayer.record_persists {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {c : ClockArena K} {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) (i : Fin 3) {τR t : ℝ} (ht₁ : readTime J ħ i ≤ t) (ht₂ : t ≤ readTime J ħ i + τR) : (xEvolve J ħ T (-1) t (xPrep b c r)).2.2 i ∈ pointerArc 2 b

★ The records persist from the readout time through the record lifetime — by the corpus's record_persists_on_interval, applied to recordProtocol i.

Demonstrated influence: the records depend on the message

theorem CSD.RecordLayer.reception_depends_on_message {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {c : ClockArena K} {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) {t : SigmaLayer.OnticTime} (ht : CV.hopTime J ħ ≤ t) : (xEvolve J ħ T (-1) t (xPrep 1 c r)).2.2 1 ∈ pointerArc 2 1 ∧ (xEvolve J ħ T (-1) t (xPrep 0 c r)).2.2 1 ∈ pointerArc 2 0 ∧ (xEvolve J ħ T (-1) t (xPrep 1 c r)).2.2 1 ≠ (xEvolve J ħ T (-1) t (xPrep 0 c r)).2.2 1

★★ The reception record depends on the message: two preparations identical except for the occupancy of A (msgConfig_siteB) leave the reception register in disjoint pointer arcs.

theorem CSD.RecordLayer.return_depends_on_message {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) {c : ClockArena K} {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) {t : SigmaLayer.OnticTime} (ht : CV.roundTrip J ħ ≤ t) : (xEvolve J ħ T (-1) t (xPrep 1 c r)).2.2 2 ≠ (xEvolve J ħ T (-1) t (xPrep 0 c r)).2.2 2

The return record depends on the message in the same way.

Occurrences and the forgetful map to record events

structure CSD.RecordLayer.Occurrence : Type

An occurrence along the constructed evolution: which register writes, at which site, at which time, recording which message. Richer than CV.RecordEvent, which keeps region and period only.

• register : Fin 3

  The register that writes.

• site : Fin 2

  The site of the write.

• time : ℝ

  The ontic time of the write.

• message : Fin 2

  The message the write records.

def CSD.RecordLayer.emission (b : Fin 2) : Occurrence

The emission of message b at A, time 0.

Equations

• CSD.RecordLayer.emission b = { register := 0, site := 0, time := 0, message := b }

noncomputable def CSD.RecordLayer.reception (J ħ : ℝ) (b : Fin 2) : Occurrence

The reception of message b at B, time τ_hop.

Equations

• CSD.RecordLayer.reception J ħ b = { register := 1, site := 1, time := CSD.CV.hopTime J ħ, message := b }

noncomputable def CSD.RecordLayer.returnOcc (J ħ : ℝ) (b : Fin 2) : Occurrence

The return of message b at A, time 2 τ_hop.

Equations

• CSD.RecordLayer.returnOcc J ħ b = { register := 2, site := 0, time := CSD.CV.roundTrip J ħ, message := b }

noncomputable def CSD.RecordLayer.eventOf {K : ℕ} (J ħ T : ℝ) (x : XArena K) (o : Occurrence) : CV.RecordEvent 2

The forgetful map to CV.RecordEvent: the region is the site, and the period label is the tick count of the physical clock in the arena at the occurrence time.

Equations

• CSD.RecordLayer.eventOf J ħ T x o = { region := {o.site}, time := CSD.RecordLayer.tickCount (CSD.RecordLayer.xEvolve J ħ T (-1) o.time x).2.1 }

theorem CSD.RecordLayer.tickCount_clock_neg_one {K : ℕ} {T : ℝ} (hT : 0 < T) (t : SigmaLayer.OnticTime) (c : ClockArena K) : tickCount (clockEvolve T (-1) t c) = tickCount (clockEvolve T 0 t c)

The clock in the arena, run from −1, has the slots of the clock run from 0.

theorem CSD.RecordLayer.eventOf_emission {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) {x : XArena K} (hx : x ∈ XReady K) (b : Fin 2) : eventOf J ħ T x (emission b) = { region := {0}, time := 0 }

Under the calibration T = τ_hop, emission is at period 0.

theorem CSD.RecordLayer.eventOf_reception {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 1 ≤ K) {x : XArena K} (hx : x ∈ XReady K) (b : Fin 2) : eventOf J ħ T x (reception J ħ b) = { region := {1}, time := 1 }

Under the calibration T = τ_hop, reception is at period 1.

theorem CSD.RecordLayer.eventOf_return {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 2 ≤ K) {x : XArena K} (hx : x ∈ XReady K) (b : Fin 2) : eventOf J ħ T x (returnOcc J ħ b) = { region := {0}, time := 2 }

Under the calibration T = τ_hop, the return is at period 2.

def CSD.RecordLayer.hopGraph : Finset (Fin 2 × Fin 2)

The coupling graph of the experiment: the one hop edge (A, B).

Equations

• CSD.RecordLayer.hopGraph = {(0, 1)}

theorem CSD.RecordLayer.causal_chain {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 2 ≤ K) {x : XArena K} (hx : x ∈ XReady K) (b : Fin 2) : CV.CausalPrecedes hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (reception J ħ b)) ∧ CV.CausalPrecedes hopGraph (eventOf J ħ T x (reception J ħ b)) (eventOf J ħ T x (returnOcc J ħ b)) ∧ CV.CausalPrecedes hopGraph (eventOf J ħ T x (emission b)) (eventOf J ħ T x (returnOcc J ħ b))

★★ The causal chain: emission ⪯ reception ⪯ return under CausalPrecedes on the hop graph, and emission ⪯ return by the corpus's transitivity.

The record predicates factor through a macroscopic projection

def CSD.RecordLayer.recordEvents {K : ℕ} (j : Fin 2) : Fin 3 → Set (XArena K)

The record events: register i displays bit j.

Equations

• CSD.RecordLayer.recordEvents j i = {x : CSD.RecordLayer.XArena K | x.2.2 i ∈ CSD.RecordLayer.pointerArc 2 j}

theorem CSD.RecordLayer.measurableSet_recordEvents {K : ℕ} (j : Fin 2) (i : Fin 3) : MeasurableSet (recordEvents j i)

noncomputable def CSD.RecordLayer.recordPattern {K : ℕ} (j : Fin 2) : MacroProjection (XArena K) (Fin 3 → Bool)

The macroscopic coordinate of the experiment's records: the pattern projection of the three "register i displays j" events.

Equations

• CSD.RecordLayer.recordPattern j = CSD.RecordLayer.patternProjection (CSD.RecordLayer.recordEvents j) ⋯

theorem CSD.RecordLayer.factorsThrough_recordEvents {K : ℕ} (j : Fin 2) (i : Fin 3) : FactorsThrough (recordPattern j).toFun (recordEvents j i)

★ Every record predicate factors through the macroscopic projection.

The package

theorem CSD.RecordLayer.recorded_exchange {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 2 ≤ K) {c : ClockArena K} (hc : c ∈ ClockReady K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) (b : Fin 2) : (∀ (s t u : SigmaLayer.OnticTime), xEvolve J ħ T t u ∘ xEvolve J ħ T s t = xEvolve J ħ T s u) ∧ (∀ (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena 2 2), MeasureTheory.MeasurePreserving (xEvolve J ħ T s t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)) ∧ (∀ (i : Fin 3) (t : SigmaLayer.OnticTime), readTime J ħ i ≤ t → (xEvolve J ħ T (-1) t (xPrep b c r)).2.2 i ∈ pointerArc 2 b) ∧ (∀ (t : SigmaLayer.OnticTime), CV.hopTime J ħ ≤ t → (xEvolve J ħ T (-1) t (xPrep 1 c r)).2.2 1 ≠ (xEvolve J ħ T (-1) t (xPrep 0 c r)).2.2 1) ∧ eventOf J ħ T (xPrep b c r) (emission b) = { region := {0}, time := 0 } ∧ eventOf J ħ T (xPrep b c r) (reception J ħ b) = { region := {1}, time := 1 } ∧ eventOf J ħ T (xPrep b c r) (returnOcc J ħ b) = { region := {0}, time := 2 } ∧ CV.CausalPrecedes hopGraph (eventOf J ħ T (xPrep b c r) (emission b)) (eventOf J ħ T (xPrep b c r) (reception J ħ b)) ∧ CV.CausalPrecedes hopGraph (eventOf J ħ T (xPrep b c r) (reception J ħ b)) (eventOf J ħ T (xPrep b c r) (returnOcc J ħ b)) ∧ ∀ (j : Fin 2) (i : Fin 3), FactorsThrough (recordPattern j).toFun (recordEvents j i)

★★★ The recorded exchange. On the common arena with its one two-time, measure-preserving evolution: from the ready preparation with message b, the three registers are written with b at 0, τ_hop, 2 τ_hop and persist; the reception register distinguishes the two messages; under the calibration T = τ_hop the occurrences map to record events at periods 0, 1, 2 that form the chain emission ⪯ reception ⪯ return on the hop graph; and the record predicates factor through the pattern projection.