The occurrence registry: actual record writes, with their provenance

Category: 7-SigmaLayer (the record layer — the registry of the clock-and-echo programme). BACKLOG #191 (out of #39; the first of #191–#197, the author's second operational-geometry brief).

Three things have been called "an event" in the programme and they are not the same thing:

1. an actual record occurrence — a carrier whose readout changes, along the constructed dynamics, from a preparation that was ready, to a value it then holds for a stated window;
2. a possible observation of a subsystem — a measurable readout and nothing else, which can be evaluated at any time without anything having been written (the receiver readouts of #190);
3. a region label — CV.RecordEvent, a read region with a period index, which is what the causal order CausalPrecedes is about.

This file keeps the three apart and names the maps between them.

• IsRecordWrite h t₀ τ₀ τ₁ w v — a readout history writes v: not v on [t₀, τ₀), v on [τ₁, τ₁ + w]; the write interval is [τ₀, τ₁] (sharp when τ₀ = τ₁), the window w finite;
• ★ not_isRecordWrite_of_eq, IsRecordWrite.not_within — inside a write's window there is no second write of that carrier, for any value: inspecting an unchanged register is not an occurrence;
• Observation X Ω — kind 2; ActualOccurrence X Ω K — kind 1, carrying the carrier's two-time measurable evolution, its readout, its ready set, the actual preparation, the recorded value, the write interval and the window, and the write itself as a proof field discharged from the dynamics (isWrite); toObservation forgets to kind 2, toRecordEvent clk forgets to kind 3 by labelling the carrier's site with a clock readout at the completion of the write;
• recordSet, measurableSet_recordSet, recordPattern, ★ factorsThrough_recordSet — the record predicate "this occurrence's value is displayed" is measurable and factors through the pattern projection of MacroProjection.lean;
• instances, each discharged from an existing dynamics: exchangeRegister i — the emission, reception and return registers of #186 (sharp writes at the readout times, toRecordEvent is #186's eventOf); clockSlot n — every slot of the record clock of #185 (write interval [nT, (n+1)T]); ★ exchange_no_second_write — after its readout a register of #186 admits no further write;
• the chain of #190 has readouts, not registers: receiverObservation k is kind 2. So ChainXArena n K adds a reception register at every site, chainXEvolve is its two-time (★ chainXEvolve_comp), measurable, ★ measure-preserving skew-product propagator, ★★ chainRegister_written writes register k with the message from the transmitted state at k τ_hop and chainRegister_frozen keeps it, chainRegister k is the actual occurrence, and ★★★ siteEvent_eq_toRecordEvent — the chain's site events are the forgetful images of actual writes on the common arena, their period labels the ticks of the site's own clock, which are writes themselves (clockSlot). That is the brief's §2 acceptance criterion;
• ★★★ record_occurrences — the package.

Honest scope

• ⚠️ The chain registers are written on the crossing of k τ_hop by the bit read off the exchange state at that time: the schedule still triggers the write, exactly as in #186. What is new is that the receptions of the chain are now writes with provenance rather than readouts; a write activated by the arriving carrier itself is #194.
• ⚠️ ActualOccurrence carries its evolve as a field so that one registry serves several arenas; the two-time law and measurability are proof fields, and every instance below supplies the corpus's constructed evolution. Nothing physical is carried by an unproved field.
• The period label of toRecordEvent is whatever clock readout is supplied; under the stated calibration T = τ_hop it is the site index, as in #186 and #190.
• Clock calibration and synchronisation stay hypotheses; the clocks' horizon must cover the chain.

References: specs/BACKLOG.md #191, #185, #186, #190, #39; RecordLayer/RecordedExchange.lean, RecordLayer/RecordClock.lean, RecordLayer/ChainClocks.lean, RecordLayer/MacroProjection.lean, CV/RecordCausalOrder.lean.

Record writes along a readout history

structure CSD.RecordLayer.IsRecordWrite {Ω : Type u_1} (h : ℝ → Ω) (t₀ τ₀ τ₁ w : ℝ) (v : Ω) : Prop

A readout history writes the value v, from the start t₀, with write interval [τ₀, τ₁] and window w: it does not display v on [t₀, τ₀), and displays v on [τ₁, τ₁ + w].

• start_le : t₀ ≤ τ₀

  The write starts after the start.

• interval : τ₀ ≤ τ₁

  The write interval is an interval.

• window_nonneg : 0 ≤ w

  The window is a window.

• before (t : ℝ) : t₀ ≤ t → t < τ₀ → h t ≠ v

  Before the write the value is not displayed.

• holds (t : ℝ) : τ₁ ≤ t → t ≤ τ₁ + w → h t = v

  Through the window the value is displayed.

theorem CSD.RecordLayer.not_isRecordWrite_of_eq {Ω : Type u_1} {h : ℝ → Ω} {t₀ τ₀ τ₁ w : ℝ} {v : Ω} {a b : ℝ} (ha₀ : t₀ ≤ a) (ha₁ : a < τ₀) (hb₀ : τ₁ ≤ b) (hb₁ : b ≤ τ₁ + w) (hab : h a = h b) : ¬IsRecordWrite h t₀ τ₀ τ₁ w v

A history that displays the same value at a time before a candidate write interval and at a time inside the candidate window admits no write there: an unchanged readout is not a write.

theorem CSD.RecordLayer.IsRecordWrite.not_within {Ω : Type u_1} {h : ℝ → Ω} {t₀ τ₀ τ₁ w : ℝ} {v : Ω} (hw : IsRecordWrite h t₀ τ₀ τ₁ w v) {t₀' τ₀' τ₁' w' : ℝ} {v' : Ω} (hstart : t₀' ≤ τ₁) (hlt : τ₁ < τ₀') (hend : τ₁' ≤ τ₁ + w) : ¬IsRecordWrite h t₀' τ₀' τ₁' w' v'

★ No second write inside a write's window. Once h has written v by τ₁ and holds it through τ₁ + w, there is no write — of any value — whose interval starts after τ₁ and completes within the window, from any start at or before τ₁. Repeated inspection of the unchanged register creates no occurrence.

The three kinds

structure CSD.RecordLayer.Observation (X : Type u_1) [MeasurableSpace X] (Ω : Type u_2) [MeasurableSpace Ω] : Type (max u_1 u_2)

A possible observation of the arena: a measurable readout and nothing else. It can be evaluated at any time; nothing need have been written.

• obs : X → Ω

  The readout.

• measurable_obs : Measurable self.obs

  It is measurable.

structure CSD.RecordLayer.ActualOccurrence (X : Type u_1) [MeasurableSpace X] (Ω : Type u_2) [MeasurableSpace Ω] (K : ℕ) : Type (max u_1 u_2)

An actual record occurrence on the arena X, with values in Ω and sites in Fin K: the carrier's evolution (a two-time, measurable dynamics), its readout, its ready set, the actual preparation, the site of the carrier, the start, the recorded value, the write interval [writeStart, writeEnd], the window, and the write itself, as a proof along the history t ↦ readout (evolve start t prep).

• evolve : SigmaLayer.OnticTime → SigmaLayer.OnticTime → X → X

  The evolution producing the write.

• evolve_self (t : SigmaLayer.OnticTime) : self.evolve t t = id

  Nothing happens in no time.

• evolve_comp (s t u : SigmaLayer.OnticTime) : self.evolve t u ∘ self.evolve s t = self.evolve s u

  The two-time law.

• measurable_evolve (s t : SigmaLayer.OnticTime) : Measurable (self.evolve s t)

  Each time-step is measurable.

• readout : X → Ω

  The carrier's readout.

• measurable_readout : Measurable self.readout

  It is measurable.

• ready : Set X

  The ready-state condition.

• measurableSet_ready : MeasurableSet self.ready

  It is measurable.

• prep : X

  The actual preparation.

• prep_mem : self.prep ∈ self.ready

  It is ready.

• site : Finset (Fin K)

  The site of the carrier.

• start : SigmaLayer.OnticTime

  The start of the history.

• value : Ω

  The recorded value.

• writeStart : ℝ

  The write interval begins.

• writeEnd : ℝ

  The write interval ends.

• window : ℝ

  The finite persistence window.

• isWrite : IsRecordWrite (fun (t : ℝ) => self.readout (self.evolve self.start t self.prep)) self.start self.writeStart self.writeEnd self.window self.value

  The write, discharged from the dynamics.

def CSD.RecordLayer.ActualOccurrence.history {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) (t : ℝ) : Ω

The readout history of the occurrence.

Equations

• o.history t = o.readout (o.evolve o.start t o.prep)

theorem CSD.RecordLayer.ActualOccurrence.isRecordWrite_history {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) : IsRecordWrite o.history o.start o.writeStart o.writeEnd o.window o.value

def CSD.RecordLayer.ActualOccurrence.toObservation {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) : Observation X Ω

Forget to kind 2: the readout alone.

Equations

• o.toObservation = { obs := o.readout, measurable_obs := ⋯ }

def CSD.RecordLayer.ActualOccurrence.toRecordEvent {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) (clk : X → ℕ) : CV.RecordEvent K

Forget to kind 3: the region is the carrier's site, the period is the supplied clock readout at the completion of the write.

Equations

• o.toRecordEvent clk = { region := o.site, time := clk (o.evolve o.start o.writeEnd o.prep) }

theorem CSD.RecordLayer.ActualOccurrence.toRecordEvent_region {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) (clk : X → ℕ) : (o.toRecordEvent clk).region = o.site

def CSD.RecordLayer.ActualOccurrence.recordSet {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) : Set X

The record predicate: at the completion of the write, the carrier displays the value.

Equations

• o.recordSet = {x : X | o.readout (o.evolve o.start o.writeEnd x) = o.value}

theorem CSD.RecordLayer.ActualOccurrence.measurableSet_recordSet {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (o : ActualOccurrence X Ω K) : MeasurableSet o.recordSet

theorem CSD.RecordLayer.ActualOccurrence.prep_mem_recordSet {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) : o.prep ∈ o.recordSet

The actual preparation lies in the record predicate: the write happened.

theorem CSD.RecordLayer.ActualOccurrence.history_eq_value {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) {t : ℝ} (h₁ : o.writeEnd ≤ t) (h₂ : t ≤ o.writeEnd + o.window) : o.history t = o.value

The preparation displays the value throughout the window.

theorem CSD.RecordLayer.ActualOccurrence.history_ne_value {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] (o : ActualOccurrence X Ω K) {t : ℝ} (h₁ : o.start ≤ t) (h₂ : t < o.writeStart) : o.history t ≠ o.value

Before the write interval the preparation does not display the value.

noncomputable def CSD.RecordLayer.ActualOccurrence.recordPattern {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {k : ℕ} (os : Fin k → ActualOccurrence X Ω K) : MacroProjection X (Fin k → Bool)

The macroscopic coordinate of a finite family of occurrences: the pattern projection of their record predicates.

Equations

• CSD.RecordLayer.ActualOccurrence.recordPattern os = CSD.RecordLayer.patternProjection (fun (j : Fin k) => (os j).recordSet) ⋯

theorem CSD.RecordLayer.ActualOccurrence.factorsThrough_recordSet {K : ℕ} {X : Type u_1} [MeasurableSpace X] {Ω : Type u_2} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {k : ℕ} (os : Fin k → ActualOccurrence X Ω K) (i : Fin k) : FactorsThrough (recordPattern os).toFun (os i).recordSet

★ Every record predicate of the family factors through the family's pattern projection.

The arc readout of a register

noncomputable def CSD.RecordLayer.arcReadout (q : LF4.KTorus) : Fin 3

The readout of a two-outcome register: 0 or 1 when the pointer sits in that pointer arc, 2 when it displays no record.

Equations

• CSD.RecordLayer.arcReadout q = if q ∈ CSD.RecordLayer.pointerArc 2 0 then 0 else if q ∈ CSD.RecordLayer.pointerArc 2 1 then 1 else 2

theorem CSD.RecordLayer.measurable_arcReadout : Measurable arcReadout

theorem CSD.RecordLayer.arcReadout_of_mem_zero {q : LF4.KTorus} (hq : q ∈ pointerArc 2 0) : arcReadout q = 0

theorem CSD.RecordLayer.arcReadout_of_mem_one {q : LF4.KTorus} (hq : q ∈ pointerArc 2 1) : arcReadout q = 1

theorem CSD.RecordLayer.arcReadout_of_mem {q : LF4.KTorus} {b : Fin 2} (hq : q ∈ pointerArc 2 b) : arcReadout q = b.castSucc

A pointer in the pointer arc of b reads b.

theorem CSD.RecordLayer.arcReadout_of_ready {q : LF4.KTorus} (hq : q ∈ readyArc 2) : arcReadout q = 2

A ready pointer displays no record.

theorem CSD.RecordLayer.castSucc_ne_two (b : Fin 2) : b.castSucc ≠ 2

Instance: the three registers of the recorded exchange (#186)

theorem CSD.RecordLayer.xPrep_register_before {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 : t < readTime J ħ i) : (xEvolve J ħ T (-1) t (xPrep b c r)).2.2 i ∈ readyArc 2

A register of the exchange is still ready before its readout time, from the preparation xPrep b c r with ready registers (no condition on the clock is needed).

noncomputable def CSD.RecordLayer.exchangeRegister {K : ℕ} {J ħ : ℝ} (T : ℝ) (hJ : 0 < J) (hħ : 0 < ħ) (i : Fin 3) (b : Fin 2) (c : ClockArena K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) {w : ℝ} (hw : 0 ≤ w) : ActualOccurrence (XArena K) (Fin 3) 2

Register i of the recorded exchange as an actual occurrence: carrier the register, readout its arc, ready set its ready arc, preparation xPrep b c r, site readSite i, a sharp write at the readout time with any window w ≥ 0 — the write discharged from register_written.

Equations

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

theorem CSD.RecordLayer.toRecordEvent_exchangeRegister_zero {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) (c : ClockArena K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) {w : ℝ} (hw : 0 ≤ w) : ((exchangeRegister T hJ hħ 0 b c hr hw).toRecordEvent fun (x : XArena K) => tickCount x.2.1) = eventOf J ħ T (xPrep b c r) (emission b)

The forgetful image of the emission register is #186's eventOf of the emission.

theorem CSD.RecordLayer.toRecordEvent_exchangeRegister_one {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) (c : ClockArena K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) {w : ℝ} (hw : 0 ≤ w) : ((exchangeRegister T hJ hħ 1 b c hr hw).toRecordEvent fun (x : XArena K) => tickCount x.2.1) = eventOf J ħ T (xPrep b c r) (reception J ħ b)

The forgetful image of the reception register is #186's eventOf of the reception.

theorem CSD.RecordLayer.toRecordEvent_exchangeRegister_two {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) (c : ClockArena K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) {w : ℝ} (hw : 0 ≤ w) : ((exchangeRegister T hJ hħ 2 b c hr hw).toRecordEvent fun (x : XArena K) => tickCount x.2.1) = eventOf J ħ T (xPrep b c r) (returnOcc J ħ b)

The forgetful image of the return register is #186's eventOf of the return.

theorem CSD.RecordLayer.exchange_no_second_write {K : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (i : Fin 3) (b : Fin 2) (c : ClockArena K) {r : Fin 3 → LF4.KTorus} (hr : ∀ (i : Fin 3), r i ∈ readyArc 2) {t₀' τ₀' τ₁' w' : ℝ} {v' : Fin 3} (hstart : t₀' ≤ readTime J ħ i) (hlt : readTime J ħ i < τ₀') : ¬IsRecordWrite (fun (t : ℝ) => arcReadout ((xEvolve J ħ T (-1) t (xPrep b c r)).2.2 i)) t₀' τ₀' τ₁' w' v'

★ After its readout a register of the exchange admits no further write: for every candidate write interval starting after the readout time, from any start at or before it, the register's history is not a write of any value. Reading the register again is not an occurrence.

Instance: the slots of the record clock (#185)

noncomputable def CSD.RecordLayer.slotReadout {K : ℕ} (n : Fin K) (x : ClockArena K) : Bool

The readout of slot n: whether it has been written.

Equations

• CSD.RecordLayer.slotReadout n x = if x.2 n ∈ CSD.RecordLayer.writtenArc K then true else false

theorem CSD.RecordLayer.measurable_slotReadout {K : ℕ} (n : Fin K) : Measurable (slotReadout n)

noncomputable def CSD.RecordLayer.clockSlot {K : ℕ} (hK : 0 < K) {T : ℝ} (hT : 0 < T) (n : Fin K) {c : ClockArena K} (hc : c ∈ ClockReady K) {w : ℝ} (hw : 0 ≤ w) {L : ℕ} (site : Finset (Fin L)) : ActualOccurrence (ClockArena K) Bool L

Slot n of the record clock as an actual occurrence: the write interval is the window [nT, (n+1)T] of #185, the value true, any window w ≥ 0; the site is the supplied label.

Equations

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

The chain of #190: readouts at the sites, then registers at the sites

noncomputable def CSD.RecordLayer.chainReadBit {n : ℕ} (k : Fin (n + 1)) (p : CV.FieldArena (n + 1) 2) : Fin 2

The bit read off a chain state at site k: its occupancy weight, thresholded at 1/2.

Equations

• CSD.RecordLayer.chainReadBit k p = if 1 / 2 ≤ Projectivization.momentMap p (CSD.CV.excAt k) then 1 else 0

theorem CSD.RecordLayer.measurable_chainReadBit {n : ℕ} (k : Fin (n + 1)) : Measurable (chainReadBit k)

noncomputable def CSD.RecordLayer.receiverObservation {K n : ℕ} (k : Fin (n + 1)) : Observation (ChainArena n K) (Fin 2)

The receiver readout at site k is a possible observation of the chain arena — kind 2, which is all the chain of #190 has at its sites.

Equations

• CSD.RecordLayer.receiverObservation k = { obs := fun (x : CSD.RecordLayer.ChainArena n K) => CSD.RecordLayer.chainReadBit k x.1, measurable_obs := ⋯ }

theorem CSD.RecordLayer.momentMap_eq_arenaObs_occAt {n : ℕ} (k : Fin (n + 1)) (p : CV.FieldArena (n + 1) 2) : Projectivization.momentMap p (CV.excAt k) = CV.arenaObs (CV.occAt k) p

The occupancy weight at site k is the arena observable of occAt k.

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

At k τ_hop the readout at site k of message 1 is 1.

theorem CSD.RecordLayer.chainReadBit_zero {n : ℕ} (J ħ t : ℝ) (k : Fin (n + 1)) : chainReadBit k (CV.chainArenaFlow J ħ t (CV.chainMsg n 0)) = 0

At every time the readout at site k of message 0 is 0.

@[reducible, inline]

abbrev CSD.RecordLayer.ChainXArena (n K : ℕ) : Type

The chain arena with a reception register at every site.

Equations

• CSD.RecordLayer.ChainXArena n K = (CSD.RecordLayer.ChainArena n K × (Fin (n + 1) → CSD.LF4.KTorus))

noncomputable def CSD.RecordLayer.chainReadAt {n : ℕ} (J ħ : ℝ) (k : Fin (n + 1)) (s : SigmaLayer.OnticTime) (p : CV.FieldArena (n + 1) 2) : Fin 2

The bit register k reads: the occupancy of site k in the exchange state at k τ_hop, when the propagator starts at s.

Equations

• CSD.RecordLayer.chainReadAt J ħ k s p = CSD.RecordLayer.chainReadBit k (CSD.CV.arenaKick ((CSD.CV.chainSchedule n J ħ).evolve s (↑↑k * CSD.CV.hopTime J ħ)) p)

theorem CSD.RecordLayer.chainReadAt_evolve {n : ℕ} (J ħ : ℝ) (k : Fin (n + 1)) (s t : SigmaLayer.OnticTime) (p : CV.FieldArena (n + 1) 2) : chainReadAt J ħ k t (CV.arenaKick ((CV.chainSchedule n J ħ).evolve s t) p) = chainReadAt J ħ k s p

The bit read at k τ_hop does not depend on where the propagator is cut.

theorem CSD.RecordLayer.measurable_chainReadAt {n : ℕ} (J ħ : ℝ) (k : Fin (n + 1)) (s : SigmaLayer.OnticTime) : Measurable (chainReadAt J ħ k s)

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

The joint two-time propagator with registers: the chain of #190, and register k translated by shearAmt 2 (bit) on the crossing of k τ_hop, the bit read off the exchange state then.

Equations

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

theorem CSD.RecordLayer.chainXEvolve_fst {K n : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (x : ChainXArena n K) : (chainXEvolve J ħ T s t x).1 = chainEvolve J ħ T s t x.1

theorem CSD.RecordLayer.chainXEvolve_register {K n : ℕ} (J ħ T : ℝ) (s t : SigmaLayer.OnticTime) (x : ChainXArena n K) (k : Fin (n + 1)) : (chainXEvolve J ħ T s t x).2 k = pshift ((arrived (↑↑k * CV.hopTime J ħ) t - arrived (↑↑k * CV.hopTime J ħ) s) * shearAmt 2 (chainReadAt J ħ k s x.1.1)) (x.2 k)

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

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

★ The two-time composition law on the arena with registers.

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

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

★ The joint propagator preserves Liouville measure — the measure of #190 on the chain arena, Haar on every register: a skew product over the chain arena, since the register shifts depend on the exchange state.

What the chain registers read and write

noncomputable def CSD.RecordLayer.chainXPrep {K n : ℕ} (b : Fin 2) (c : Fin (n + 1) → ClockArena K) (r : Fin (n + 1) → LF4.KTorus) : ChainXArena n K

The preparation with message b: the chain preparation and the registers r.

Equations

• CSD.RecordLayer.chainXPrep b c r = (CSD.RecordLayer.chainPrep b c, r)

theorem CSD.RecordLayer.chainReadAt_neg_one {n : ℕ} (J ħ : ℝ) (k : Fin (n + 1)) (p : CV.FieldArena (n + 1) 2) : chainReadAt J ħ k (-1) p = chainReadBit k (CV.chainArenaFlow J ħ (↑↑k * CV.hopTime J ħ) p)

From a start before the switch-on, the exchange factor at k τ_hop is the scheduled arena flow.

theorem CSD.RecordLayer.chainReadAt_chainMsg {n : ℕ} {J ħ : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (k : Fin (n + 1)) (b : Fin 2) : chainReadAt J ħ k (-1) (CV.chainMsg n b) = b

★ Register k reads the message at k τ_hop: 1 for message 1 (the transfer), 0 for message 0 (the vacuum never moves).

theorem CSD.RecordLayer.chainRegister_before {K n : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) (c : Fin (n + 1) → ClockArena K) {r : Fin (n + 1) → LF4.KTorus} (hr : ∀ (k : Fin (n + 1)), r k ∈ readyArc 2) (k : Fin (n + 1)) {t : SigmaLayer.OnticTime} (ht : t < ↑↑k * CV.hopTime J ħ) : (chainXEvolve J ħ T (-1) t (chainXPrep b c r)).2 k ∈ readyArc 2

Before k τ_hop register k is still ready.

theorem CSD.RecordLayer.chainRegister_written {K n : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (b : Fin 2) (c : Fin (n + 1) → ClockArena K) {r : Fin (n + 1) → LF4.KTorus} (hr : ∀ (k : Fin (n + 1)), r k ∈ readyArc 2) (k : Fin (n + 1)) {t : SigmaLayer.OnticTime} (ht : ↑↑k * CV.hopTime J ħ ≤ t) : (chainXEvolve J ħ T (-1) t (chainXPrep b c r)).2 k ∈ pointerArc 2 b

★★ Register k is written with the message from k τ_hop on, from the transmitted state: the reception at site k is now a write with provenance, not a readout.

theorem CSD.RecordLayer.chainRegister_frozen {K n : ℕ} (J ħ T : ℝ) {s t : SigmaLayer.OnticTime} (k : Fin (n + 1)) (hs : ↑↑k * CV.hopTime J ħ ≤ s) (hst : s ≤ t) (x : ChainXArena n K) : (chainXEvolve J ħ T s t x).2 k = x.2 k

After k τ_hop register k is frozen.

noncomputable def CSD.RecordLayer.chainRegister {K n : ℕ} {J ħ : ℝ} (T : ℝ) (hJ : 0 < J) (hħ : 0 < ħ) (k : Fin (n + 1)) (b : Fin 2) (c : Fin (n + 1) → ClockArena K) {r : Fin (n + 1) → LF4.KTorus} (hr : ∀ (k : Fin (n + 1)), r k ∈ readyArc 2) {w : ℝ} (hw : 0 ≤ w) : ActualOccurrence (ChainXArena n K) (Fin 3) (n + 1)

Register k of the chain as an actual occurrence: a sharp write at k τ_hop with the message, from the ready preparation, any window w ≥ 0.

Equations

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

theorem CSD.RecordLayer.siteEvent_eq_toRecordEvent {K n : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) (hnK : n ≤ K) (k : Fin (n + 1)) (b : Fin 2) {c : Fin (n + 1) → ClockArena K} (hc : ∀ (j : Fin (n + 1)), c j ∈ ClockReady K) {r : Fin (n + 1) → LF4.KTorus} (hr : ∀ (k : Fin (n + 1)), r k ∈ readyArc 2) {w : ℝ} (hw : 0 ≤ w) : ((chainRegister T hJ hħ k b c hr hw).toRecordEvent fun (x : ChainXArena n K) => tickCount (x.1.2 k)) = siteEvent k

★★★ The chain's site events are the forgetful images of actual writes on the common arena. Under the calibration T = τ_hop, with the period read off the clock at site k — whose ticks are writes themselves (clockSlot) — the actual occurrence of register k maps to siteEvent k, the event #190's causal chain is built from.

The package

theorem CSD.RecordLayer.record_occurrences {K n : ℕ} {J ħ T : ℝ} (hJ : 0 < J) (hħ : 0 < ħ) (hT : T = CV.hopTime J ħ) (hK : 0 < K) (hnK : n ≤ K) {c : Fin (n + 1) → ClockArena K} (hc : ∀ (j : Fin (n + 1)), c j ∈ ClockReady K) {r : Fin (n + 1) → LF4.KTorus} (hr : ∀ (k : Fin (n + 1)), r k ∈ readyArc 2) {w : ℝ} (hw : 0 ≤ w) : (∀ (Ω : Type) (h : ℝ → Ω) (t₀ τ₀ τ₁ w₁ : ℝ) (v : Ω), IsRecordWrite h t₀ τ₀ τ₁ w₁ v → ∀ (t₀' τ₀' τ₁' w' : ℝ) (v' : Ω), t₀' ≤ τ₁ → τ₁ < τ₀' → τ₁' ≤ τ₁ + w₁ → ¬IsRecordWrite h t₀' τ₀' τ₁' w' v') ∧ (∀ (s t u : SigmaLayer.OnticTime), chainXEvolve J ħ T t u ∘ chainXEvolve J ħ T s t = chainXEvolve J ħ T s u) ∧ (∀ (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena (n + 1) 2), MeasureTheory.MeasurePreserving (chainXEvolve J ħ T s t) (((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume).prod MeasureTheory.volume) (((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume).prod MeasureTheory.volume)) ∧ (∀ (b : Fin 2) (k : Fin (n + 1)) (t : SigmaLayer.OnticTime), ↑↑k * CV.hopTime J ħ ≤ t → (chainXEvolve J ħ T (-1) t (chainXPrep b c r)).2 k ∈ pointerArc 2 b) ∧ (∀ (b : Fin 2) (k : Fin (n + 1)), ((chainRegister T hJ hħ k b c hr hw).toRecordEvent fun (x : ChainXArena n K) => tickCount (x.1.2 k)) = siteEvent k) ∧ ∀ (b : Fin 2) (k : Fin (n + 1)), FactorsThrough (ActualOccurrence.recordPattern fun (j : Fin (n + 1)) => chainRegister T hJ hħ j b c hr hw).toFun (chainRegister T hJ hħ k b c hr hw).recordSet

★★★ The occurrence registry. No carrier is written twice inside a write's window; the three registers of the exchange and every clock slot are actual occurrences discharged from their dynamics, the exchange's forgetful images being #186's events; the chain of #190 carries registers on one two-time measure-preserving dynamics, each written with the message at k τ_hop and frozen after, and the site events of #190's causal chain are the forgetful images of those writes, labelled by the site's own clock.