The activated write: one pointer set in motion by the arriving carrier

Category: 7-SigmaLayer (the record layer). BACKLOG #194 (out of #39; the research gate of the author's second operational-geometry brief, #191–#197).

Every write in the corpus so far was triggered by a schedule: a readout time indexed by t_Σ (RecordedExchange.lean, ChainClocks.lean). This file replaces one of them by an internal activation. The arena is the two-site exchange of #183 with one pointer torus,

ActiveArena = FieldArena 2 2 × T², θ = (θ₁, θ₂),

and the dynamics is the one the time-independent joint Hamiltonian

𝓗(p, θ) = ⟨p, J X p⟩ + g · n_B(p) · f(θ₂), f periodic and C¹,

prescribes on the product: at fixed θ₂ the ray evolves by the detuned exchange H(Δ) = J X + Δ n_B with Δ = g f(θ₂) (CV/DetunedExchange.lean), the pointer θ₁ moves at the rate −(2g/ħ) f'(θ₂) · n_B(p) (the factor is the arena form's normalisation, fixed by #195), and θ₂ is conserved. The pointer therefore moves only while the carrier occupies the receiver: the activation is the arriving carrier, and no test of t_Σ appears anywhere — the evolution is autonomous (activeEvolve_shift).

• detuningAt, rateAt — g f(θ₂) and −(2g/ħ) f'(θ₂) on the circle (Function.Periodic.lift); Function.Periodic.deriv_periodic (AddCirclePeriodicLift.lean); ★ pointerAmount, ★ activeFlow — the dynamics as data;
• activeFlow_zero, ★★ activeFlow_add — a one-parameter group, by the group law of the accumulated occupancy; activeEvolve, activeEvolve_self, activeEvolve_comp — the two-time law; ★ activeEvolve_shift — autonomy: only t − s enters;
• continuous_activeFlow; ★★ activeFlow_measurePreserving — Liouville: the skew product of the Fubini–Study-preserving unitary at fixed θ₂ with a translation of θ₁ by a function of (p, θ₂), over the conserved θ₂;
• ★★ activeEnergy_activeFlow — the joint energy J⟨X⟩ + g f(θ₂) n_B is conserved; activeFlow_angle — θ₂ is conserved;
• ★★ hasDerivAt_pointerAmount — the pointer's equation of motion: the lifted angle moves at the rate −(2g/ħ) f'(θ₂) · n_B(p(t)); occHist_msgPoint_one_zero, occHist_msgPoint_one_pos (in DetunedExchange.lean) — the pointer starts at rest and is set in motion by the carrier;
• ★★★ pointerAmount_msgPoint_one, activeFlow_msgPoint_zero — the message-dependent pointer displacement: for message 1 the pointer has turned by κ (ωt − sin ωt cos ωt)/(2ω) with κ = −(2g/ħ) f'(θ₂) (J/Ω)², ω = Ω/ħ; for message 0 the whole arena point is fixed;
• displayArc, displayed, writeStart, writeEnd, retention; ★★ message_one_not_displayed, ★★ message_one_displayed — the write interval and the retention window, under the explicit hypotheses 0 < κ and 3κ ≤ 2ω (the pointer gains at most two thirds of a turn per Rabi radian); ★★★ activatedRegister — the write as an ActualOccurrence (#191), site {B}, from the start 0, value true, with its write interval [1/(6κ), 2/(3κ) + 1/(2ω)] and window 2/(3κ) − 1/ω;
• ★★ records_distinguish — the two messages leave the pointer in disjoint arcs throughout the window; the detuning loss (J/Ω)² < 1 is paid in the rate, not in the record;
• ★★ message_one_returns — the retention is finite: the carrier oscillates on, the pointer keeps turning, and at an explicit later time it is back where message 0 left it;
• ★★ transition_region — the obstruction half: for every horizon T the set of θ₂ at which the message-1 write has not been displayed by T is open and of positive Haar measure. It contains the zero of f' that Rolle's theorem forces on every periodic C¹ coupling (exists_rateAt_eq_zero). The write is continuous in the preparation, so it is exact only off a transition region — the trilemma's price, which the brief allows;
• ★★★ activated_write — the package.

What is and is not claimed

• ⚠️ Hamiltonian generation is #195. This file builds the dynamics the Hamiltonian prescribes and proves it is a two-time, measure-preserving, energy-conserving flow whose pointer obeys the stated equation of motion (hasDerivAt_pointerAmount) and whose ray obeys Schrödinger's equation with the state-dependent generator (hasDerivAt_detunedFlowVal). That activeFlow is the Hamiltonian flow of 𝓗 for the arena form of LF4/ArenaSymplectic.lean is not proved here.
• The pointer coordinate that moves is θ₁; the record is read off it. Its symplectic partner θ₂ is a conserved parameter that sets both the detuning and the rate; nothing is claimed about a global translation on the torus (θ̇₂ = 0).
• The write is exact for the preparations stated: ready pointer, 0 < κ, 3κ ≤ 2ω. Angles with f'(θ₂) < 0 turn the pointer the other way and are not treated; angles with small |f'| are the transition region of transition_region, and that region has positive measure for every finite horizon. This is the honest form of "exact only off a transition region".
• No clock is in this arena; the forgetful map to CV.RecordEvent needs one and is not taken.

References: specs/BACKLOG.md #194, #191, #195, #39; CV/DetunedExchange.lean, RecordLayer/RecordOccurrence.lean (ActualOccurrence, IsRecordWrite), RecordLayer/ShearWitness.lean (pshift, readyArc, rep_pshift_of_mem), RecordLayer/RecordedExchange.lean (the scheduled writes this replaces one of), SigmaLayer/UntriggeredFlow.lean (the chart-level one-stroke witness), SigmaLayer/FrozenBase.lean.

The arena

@[reducible, inline]

abbrev CSD.RecordLayer.ActiveArena : Type

The arena of the activated write: the two-site exchange and one pointer torus.

Equations

• CSD.RecordLayer.ActiveArena = (CSD.CV.FieldArena 2 2 × CSD.LF4.KTorus)

The coupling function on the conserved angle

noncomputable def CSD.RecordLayer.detuningAt {f : ℝ → ℝ} (g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) : ℝ

The detuning g f(θ₂).

Equations

• CSD.RecordLayer.detuningAt g hf φ = g * hf.lift φ

noncomputable def CSD.RecordLayer.rateAt {f : ℝ → ℝ} (g ħ : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) : ℝ

The pointer rate −(2g/ħ) f'(θ₂): the rate Hamilton's equations prescribe for the arena form, whose Fubini–Study normalisation makes the Schrödinger unitary of H the flow of −2⟨H⟩ (LF4/ArenaCoupledFlow.lean, #195).

Equations

• CSD.RecordLayer.rateAt g ħ hf φ = -(2 * g / ħ) * ⋯.lift φ

theorem CSD.RecordLayer.detuningAt_coe {f : ℝ → ℝ} (g : ℝ) (hf : Function.Periodic f 1) (x : ℝ) : detuningAt g hf ↑x = g * f x

theorem CSD.RecordLayer.rateAt_coe {f : ℝ → ℝ} (g ħ : ℝ) (hf : Function.Periodic f 1) (x : ℝ) : rateAt g ħ hf ↑x = -(2 * g / ħ) * deriv f x

theorem CSD.RecordLayer.continuous_periodicLift {f : ℝ → ℝ} (hf : Function.Periodic f 1) (hc : Continuous f) : Continuous hf.lift

theorem CSD.RecordLayer.continuous_detuningAt {f : ℝ → ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hc : Continuous f) : Continuous (detuningAt g hf)

theorem CSD.RecordLayer.continuous_rateAt {f : ℝ → ℝ} (g ħ : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) : Continuous (rateAt g ħ hf)

theorem CSD.RecordLayer.exists_rateAt_eq_zero {f : ℝ → ℝ} (g ħ : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) : ∃ (φ : AddCircle 1), rateAt g ħ hf φ = 0

Rolle: a periodic C¹ coupling has a stationary angle, at which the pointer rate vanishes.

The dynamics

noncomputable def CSD.RecordLayer.pointerAmount {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) (x : ActiveArena) : ℝ

The lifted pointer displacement after time t: −(2g/ħ) f'(θ₂) ∫₀ᵗ n_B(p(s)) ds.

Equations

• CSD.RecordLayer.pointerAmount J ħ g hf t x = CSD.RecordLayer.rateAt g ħ hf x.2.2 * CSD.CV.occAccum J ħ (CSD.RecordLayer.detuningAt g hf x.2.2) x.1 t

noncomputable def CSD.RecordLayer.activeFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) : ActiveArena → ActiveArena

★ The activated flow: at fixed θ₂ the ray evolves by the detuned exchange with Δ = g f(θ₂), and the pointer θ₁ is translated by the lifted displacement.

Equations

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

theorem CSD.RecordLayer.activeFlow_fst {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) (x : ActiveArena) : (activeFlow J ħ g hf t x).1 = (CV.detunedFlow J ħ (detuningAt g hf x.2.2)).arenaFlow t x.1

theorem CSD.RecordLayer.activeFlow_snd {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) (x : ActiveArena) : (activeFlow J ħ g hf t x).2 = pshift (pointerAmount J ħ g hf t x) x.2

theorem CSD.RecordLayer.activeFlow_angle {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) (x : ActiveArena) : (activeFlow J ħ g hf t x).2.2 = x.2.2

θ₂ is conserved.

theorem CSD.RecordLayer.occupancy_activeFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) (x : ActiveArena) : CV.arenaObs CV.occB (activeFlow J ħ g hf t x).1 = CV.occHist J ħ (detuningAt g hf x.2.2) x.1 t

The receiver's occupancy along the flow is the occupancy history of the detuned exchange.

theorem CSD.RecordLayer.activeFlow_zero {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) : activeFlow J ħ g hf 0 = id

theorem CSD.RecordLayer.pointerAmount_add {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (s t : ℝ) (x : ActiveArena) : pointerAmount J ħ g hf (s + t) x = pointerAmount J ħ g hf s x + pointerAmount J ħ g hf t (activeFlow J ħ g hf s x)

theorem CSD.RecordLayer.activeFlow_add {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (s t : ℝ) : activeFlow J ħ g hf (s + t) = activeFlow J ħ g hf t ∘ activeFlow J ħ g hf s

★★ The group law: the flow is a one-parameter group, because the accumulated occupancy obeys the group law of the detuned exchange (occAccum_add).

noncomputable def CSD.RecordLayer.activeEvolve {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (s t : SigmaLayer.OnticTime) : ActiveArena → ActiveArena

The two-time propagator: autonomous, so only the elapsed time enters.

Equations

• CSD.RecordLayer.activeEvolve J ħ g hf s t = CSD.RecordLayer.activeFlow J ħ g hf (t - s)

theorem CSD.RecordLayer.activeEvolve_self {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : SigmaLayer.OnticTime) : activeEvolve J ħ g hf t t = id

theorem CSD.RecordLayer.activeEvolve_comp {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (s t u : SigmaLayer.OnticTime) : activeEvolve J ħ g hf t u ∘ activeEvolve J ħ g hf s t = activeEvolve J ħ g hf s u

The two-time law.

theorem CSD.RecordLayer.activeEvolve_shift {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (s t a : SigmaLayer.OnticTime) : activeEvolve J ħ g hf (s + a) (t + a) = activeEvolve J ħ g hf s t

★ Autonomy: shifting both times leaves the propagator unchanged — no test of t_Σ appears. Compare the scheduled hopOn/arrived of RecordedExchange.lean.

Continuity and Liouville

theorem CSD.RecordLayer.continuous_pointerAmount {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) (t : ℝ) : Continuous (pointerAmount J ħ g hf t)

theorem CSD.RecordLayer.continuous_activeFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) (t : ℝ) : Continuous (activeFlow J ħ g hf t)

theorem CSD.RecordLayer.measurable_activeEvolve {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) (s t : SigmaLayer.OnticTime) : Measurable (activeEvolve J ħ g hf s t)

noncomputable def CSD.RecordLayer.cshift (a : ℝ) (θ : AddCircle 1) : AddCircle 1

Translation of one circle coordinate, written as pshift writes it.

Equations

• CSD.RecordLayer.cshift a θ = θ + ↑a

theorem CSD.RecordLayer.continuous_cshift_uncurry : Continuous fun (aθ : ℝ × AddCircle 1) => cshift aθ.1 aθ.2

theorem CSD.RecordLayer.measurePreserving_cshift (a : ℝ) : MeasureTheory.MeasurePreserving (cshift a) MeasureTheory.volume MeasureTheory.volume

theorem CSD.RecordLayer.activeFlow_measurePreserving {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) (t : ℝ) (p₀ : CV.FieldArena 2 2) : MeasureTheory.MeasurePreserving (activeFlow J ħ g hf t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)

★★ Liouville: the activated flow preserves Fubini–Study × Haar × Haar. The proof is the skew product over the conserved θ₂: at fixed θ₂ the ray moves by a unitary (Fubini–Study preserving) and θ₁ by a translation depending on (p, θ₂) (Haar preserving).

theorem CSD.RecordLayer.activeEvolve_measurePreserving {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena 2 2) : MeasureTheory.MeasurePreserving (activeEvolve J ħ g hf s t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)

Energy and the equations of motion

noncomputable def CSD.RecordLayer.activeEnergy {f : ℝ → ℝ} (J g : ℝ) (hf : Function.Periodic f 1) (x : ActiveArena) : ℝ

The joint energy J⟨X⟩ + g f(θ₂) n_B: the Hamiltonian function of #194 read at an arena point.

Equations

• CSD.RecordLayer.activeEnergy J g hf x = J * CSD.CV.arenaObs CSD.CV.hopX x.1 + CSD.RecordLayer.detuningAt g hf x.2.2 * Projectivization.momentMap x.1 CSD.CV.excB

theorem CSD.RecordLayer.activeEnergy_eq {f : ℝ → ℝ} (J g : ℝ) (hf : Function.Periodic f 1) (x : ActiveArena) : activeEnergy J g hf x = CV.arenaObs (CV.detunedH J (detuningAt g hf x.2.2)) x.1

theorem CSD.RecordLayer.activeEnergy_activeFlow {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (t : ℝ) (x : ActiveArena) : activeEnergy J g hf (activeFlow J ħ g hf t x) = activeEnergy J g hf x

★★ Energy conservation: the joint energy is constant along the activated flow.

theorem CSD.RecordLayer.hasDerivAt_pointerAmount {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (x : ActiveArena) (t : ℝ) : HasDerivAt (fun (t : ℝ) => pointerAmount J ħ g hf t x) (rateAt g ħ hf x.2.2 * CV.arenaObs CV.occB (activeFlow J ħ g hf t x).1) t

★★ The pointer's equation of motion: the lifted displacement moves at the rate −(2g/ħ) f'(θ₂) · n_B(p(t)) — only while the carrier occupies the receiver.

The two messages

theorem CSD.RecordLayer.activeFlow_msgPoint_zero {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (q : LF4.KTorus) (t : ℝ) : activeFlow J ħ g hf t (CV.msgPoint 0, q) = (CV.msgPoint 0, q)

Message 0 is fixed: the vacuum never reaches the receiver, so the pointer never moves.

noncomputable def CSD.RecordLayer.pointerDrift (κ ω t : ℝ) : ℝ

The pointer drift κ (ωt − sin ωt cos ωt)/(2ω) as a function of time.

Equations

• CSD.RecordLayer.pointerDrift κ ω t = κ * (ω * t - Real.sin (ω * t) * Real.cos (ω * t)) / (2 * ω)

noncomputable def CSD.RecordLayer.driftRate {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (φ : AddCircle 1) : ℝ

The mean pointer rate over a Rabi cycle: κ = −(2g/ħ) f'(θ₂) (J/Ω)².

Equations

• CSD.RecordLayer.driftRate J ħ g hf φ = CSD.RecordLayer.rateAt g ħ hf φ * (J / CSD.CV.rabiFreq J (CSD.RecordLayer.detuningAt g hf φ)) ^ 2

theorem CSD.RecordLayer.pointerAmount_msgPoint_one {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (q : LF4.KTorus) (t : ℝ) : pointerAmount J ħ g hf t (CV.msgPoint 1, q) = pointerDrift (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) t

★★★ The message-dependent pointer displacement: for message 1 the lifted pointer has turned by pointerDrift κ ω t with κ = −(2g/ħ) f'(θ₂) (J/Ω)² and ω = Ω/ħ.

theorem CSD.RecordLayer.activeFlow_msgPoint_one_snd {f : ℝ → ℝ} (J ħ g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (q : LF4.KTorus) (t : ℝ) : (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 = pshift (pointerDrift (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) t) q

Bounds on the drift

theorem CSD.RecordLayer.abs_sin_mul_cos_le_half (x : ℝ) : |Real.sin x * Real.cos x| ≤ 1 / 2

theorem CSD.RecordLayer.sub_sin_mul_cos_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ x - Real.sin x * Real.cos x

theorem CSD.RecordLayer.sub_sin_mul_cos_le_two_mul {x : ℝ} (hx : 0 ≤ x) : x - Real.sin x * Real.cos x ≤ 2 * x

theorem CSD.RecordLayer.pointerDrift_nonneg {κ ω : ℝ} (hκ : 0 ≤ κ) (hω : 0 < ω) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ pointerDrift κ ω t

theorem CSD.RecordLayer.pointerDrift_le {κ ω : ℝ} (hκ : 0 ≤ κ) (hω : 0 < ω) {t : ℝ} (ht : 0 ≤ t) : pointerDrift κ ω t ≤ κ * t

theorem CSD.RecordLayer.pointerDrift_lower {κ ω : ℝ} (hκ : 0 ≤ κ) (hω : 0 < ω) (t : ℝ) : κ * (t / 2 - 1 / (4 * ω)) ≤ pointerDrift κ ω t

theorem CSD.RecordLayer.pointerDrift_upper {κ ω : ℝ} (hκ : 0 ≤ κ) (hω : 0 < ω) (t : ℝ) : pointerDrift κ ω t ≤ κ * (t / 2 + 1 / (4 * ω))

theorem CSD.RecordLayer.continuous_pointerDrift (κ ω : ℝ) : Continuous (pointerDrift κ ω)

The display arc, the readout and the write interval

noncomputable def CSD.RecordLayer.displayArc : Set LF4.KTorus

The displayed arc (1/3, 5/6]: two ready widths past the ready arc, one width short of the turn.

Equations

• CSD.RecordLayer.displayArc = {q : CSD.LF4.KTorus | CSD.RecordLayer.rep q.1 ∈ Set.Ioc (2 * CSD.RecordLayer.shearWidth 2) (1 - CSD.RecordLayer.shearWidth 2)}

theorem CSD.RecordLayer.measurableSet_displayArc : MeasurableSet displayArc

theorem CSD.RecordLayer.shearWidth_two : shearWidth 2 = 1 / 6

theorem CSD.RecordLayer.readyArc_disjoint_displayArc : Disjoint (readyArc 2) displayArc

noncomputable def CSD.RecordLayer.displayed (x : ActiveArena) : Bool

The Boolean readout: is the pointer in the displayed arc?

Equations

• CSD.RecordLayer.displayed x = if x.2 ∈ CSD.RecordLayer.displayArc then true else false

theorem CSD.RecordLayer.measurable_displayed : Measurable displayed

theorem CSD.RecordLayer.displayed_eq_true {x : ActiveArena} (hx : x.2 ∈ displayArc) : displayed x = true

theorem CSD.RecordLayer.displayed_eq_false {x : ActiveArena} (hx : x.2 ∉ displayArc) : displayed x = false

noncomputable def CSD.RecordLayer.displayObservation : Observation ActiveArena Bool

The readout as an Observation (#191, kind 2).

Equations

• CSD.RecordLayer.displayObservation = { obs := CSD.RecordLayer.displayed, measurable_obs := CSD.RecordLayer.measurable_displayed }

noncomputable def CSD.RecordLayer.writeStart (κ : ℝ) : ℝ

The write interval begins: 1/(6κ).

Equations

• CSD.RecordLayer.writeStart κ = 1 / (6 * κ)

noncomputable def CSD.RecordLayer.writeEnd (κ ω : ℝ) : ℝ

The write interval ends: 2/(3κ) + 1/(2ω).

Equations

• CSD.RecordLayer.writeEnd κ ω = 2 / (3 * κ) + 1 / (2 * ω)

noncomputable def CSD.RecordLayer.retention (κ ω : ℝ) : ℝ

The retention window: 2/(3κ) − 1/ω.

Equations

• CSD.RecordLayer.retention κ ω = 2 / (3 * κ) - 1 / ω

theorem CSD.RecordLayer.writeStart_nonneg {κ : ℝ} (hκ : 0 < κ) : 0 ≤ writeStart κ

theorem CSD.RecordLayer.writeStart_le_writeEnd {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) : writeStart κ ≤ writeEnd κ ω

theorem CSD.RecordLayer.retention_nonneg {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) (hslow : 3 * κ ≤ 2 * ω) : 0 ≤ retention κ ω

The window is a window exactly when the pointer gains at most two thirds of a turn per Rabi radian: 3κ ≤ 2ω.

theorem CSD.RecordLayer.mul_writeStart {κ : ℝ} (hκ : 0 < κ) : κ * writeStart κ = 1 / 6

theorem CSD.RecordLayer.drift_at_writeEnd {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) : κ * (writeEnd κ ω / 2 - 1 / (4 * ω)) = 1 / 3

theorem CSD.RecordLayer.drift_at_window_end {κ ω : ℝ} (hκ : 0 < κ) (hω : 0 < ω) : κ * ((writeEnd κ ω + retention κ ω) / 2 + 1 / (4 * ω)) = 2 / 3

theorem CSD.RecordLayer.message_one_not_displayed {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) {t : ℝ} (ht0 : 0 ≤ t) (ht : t < writeStart (driftRate J ħ g hf q.2)) : (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 ∉ displayArc

★★ Before the write interval the register is not displayed: the pointer has turned by less than κ t < 1/6.

theorem CSD.RecordLayer.message_one_displayed {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) {t : ℝ} (ht₁ : writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) ≤ t) (ht₂ : t ≤ writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) + retention (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2))) : (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 ∈ displayArc

★★ Through the window the register is displayed: the pointer has turned by between 1/3 and 2/3 of a turn.

noncomputable def CSD.RecordLayer.activatedRegister {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) : ActualOccurrence ActiveArena Bool 2

★★★ The activated write as an actual occurrence (#191): the carrier at B (site {1}), history from 0, value true, write interval [1/(6κ), 2/(3κ) + 1/(2ω)], window 2/(3κ) − 1/ω. The hypotheses are the ready pointer, a positive mean rate κ = −(2g/ħ) f'(θ₂) (J/Ω)², and the slowness 3κ ≤ 2ω.

Equations

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

theorem CSD.RecordLayer.activatedRegister_prep {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) : (activatedRegister g hf hJ hħ hf1 hq hκ hslow).prep = (CV.msgPoint 1, q)

theorem CSD.RecordLayer.activatedRegister_site {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) : (activatedRegister g hf hJ hħ hf1 hq hκ hslow).site = {1}

theorem CSD.RecordLayer.records_distinguish {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) {t : ℝ} (ht₁ : writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) ≤ t) (ht₂ : t ≤ writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) + retention (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2))) : (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 ∈ displayArc ∧ (activeFlow J ħ g hf t (CV.msgPoint 0, q)).2 ∈ readyArc 2 ∧ (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 ≠ (activeFlow J ħ g hf t (CV.msgPoint 0, q)).2

★★ The two messages are distinguishable throughout the window: message 1 displays, message 0 leaves the pointer ready, and the two pointer positions differ.

theorem CSD.RecordLayer.message_one_returns {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (q : LF4.KTorus) (hκ : 0 < driftRate J ħ g hf q.2) : ∃ (t : ℝ), writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) + retention (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) < t ∧ (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 = q

★★ The retention is finite: after the window there is a time at which the message-1 pointer is back exactly where message 0 left it — the carrier oscillates on and the pointer completes a turn.

The transition region

theorem CSD.RecordLayer.rep_pshift_of_mem_neg (q : LF4.KTorus) {a : ℝ} (h : rep q.1 + a ∈ Set.Ioc (-1) 0) : rep (pshift a q).1 = rep q.1 + a + 1

A translation that wraps once drops the representative by a turn.

theorem CSD.RecordLayer.transition_region {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hf1 : ContDiff ℝ 1 f) {T : ℝ} (hT : 0 < T) : IsOpen {φ : AddCircle 1 | |rateAt g ħ hf φ| * T < shearWidth 2} ∧ 0 < MeasureTheory.volume {φ : AddCircle 1 | |rateAt g ħ hf φ| * T < shearWidth 2} ∧ ∀ φ ∈ {φ : AddCircle 1 | |rateAt g ħ hf φ| * T < shearWidth 2}, ∀ q ∈ readyArc 2, q.2 = φ → (activeFlow J ħ g hf T (CV.msgPoint 1, q)).2 ∉ displayArc

★★ The transition region has positive measure for every horizon. For every T > 0 the set of angles θ₂ with |2g f'(θ₂)/ħ| T < 1/6 is open and nonempty (it contains Rolle's zero of f'), hence of positive Haar measure, and from every ready pointer at such an angle the message-1 write is not displayed at time T. The write is exact only off this region.

The package

theorem CSD.RecordLayer.activated_write {f : ℝ → ℝ} {J ħ : ℝ} (g : ℝ) (hf : Function.Periodic f 1) (hJ : 0 < J) (hħ : 0 < ħ) (hf1 : ContDiff ℝ 1 f) {q : LF4.KTorus} (hq : q ∈ readyArc 2) (hκ : 0 < driftRate J ħ g hf q.2) (hslow : 3 * driftRate J ħ g hf q.2 ≤ 2 * CV.rabiRate J ħ (detuningAt g hf q.2)) : (∀ (s t u : SigmaLayer.OnticTime), activeEvolve J ħ g hf t u ∘ activeEvolve J ħ g hf s t = activeEvolve J ħ g hf s u) ∧ (∀ (s t a : SigmaLayer.OnticTime), activeEvolve J ħ g hf (s + a) (t + a) = activeEvolve J ħ g hf s t) ∧ (∀ (s t : SigmaLayer.OnticTime) (p₀ : CV.FieldArena 2 2), MeasureTheory.MeasurePreserving (activeEvolve J ħ g hf s t) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume) ((Matrix.UnitaryGroup.fsMeasure p₀).prod MeasureTheory.volume)) ∧ (∀ (t : ℝ) (x : ActiveArena), activeEnergy J g hf (activeFlow J ħ g hf t x) = activeEnergy J g hf x) ∧ (∀ (t : ℝ) (x : ActiveArena), (activeFlow J ħ g hf t x).2.2 = x.2.2) ∧ (∀ (x : ActiveArena) (t : ℝ), HasDerivAt (fun (t : ℝ) => pointerAmount J ħ g hf t x) (rateAt g ħ hf x.2.2 * CV.arenaObs CV.occB (activeFlow J ħ g hf t x).1) t) ∧ (∀ (t : ℝ), activeFlow J ħ g hf t (CV.msgPoint 0, q) = (CV.msgPoint 0, q)) ∧ (∀ (t : ℝ), writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) ≤ t → t ≤ writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) + retention (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) → (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 ∈ displayArc ∧ (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 ≠ (activeFlow J ħ g hf t (CV.msgPoint 0, q)).2) ∧ (∃ (t : ℝ), writeEnd (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) + retention (driftRate J ħ g hf q.2) (CV.rabiRate J ħ (detuningAt g hf q.2)) < t ∧ (activeFlow J ħ g hf t (CV.msgPoint 1, q)).2 = q) ∧ (activatedRegister g hf hJ hħ hf1 hq hκ hslow).prep = (CV.msgPoint 1, q) ∧ (activatedRegister g hf hJ hħ hf1 hq hκ hslow).site = {1}

★★★ The activated write. On FieldArena 2 2 × T² with the dynamics of the time-independent joint Hamiltonian ⟨p, J X p⟩ + g n_B(p) f(θ₂): the two-time law holds and the propagator is autonomous; Liouville measure is preserved; the joint energy and θ₂ are conserved; the pointer's lifted angle moves at the rate −(2g/ħ) f'(θ₂) n_B(p(t)); message 0 leaves the whole arena point fixed; through the window message 1 displays and the two pointer positions differ; the retention is finite; and the write is registered as an ActualOccurrence at site {B}.