RecordLayer/DrivenTwoTime: measure, DRIVE, measure — the two-time law with a flow between the readouts

Category: 7-SigmaLayer (the record layer — Q25's two-stage arena with a sector flow inserted between the two measurements, and the first measurement in an arbitrary orthonormal basis; the record-layer engine TH5d consumes, specs/BACKLOG.md ▶ OPEN QUEUE #4).

What was missing

RecordLayer/TwoTimeLuders.lean composes two measurements on one arena, but nothing happens to the system BETWEEN them: the second apparatus reads the relocated state [eᵢ] as it was left. Every "measure, evolve, measure" statement — a two-point-measurement protocol, a Ramsey sequence, an echo — needs a flow in the gap. This module inserts one, and lets the first measurement read an arbitrary orthonormal basis (the two-stage arena's first context was the computational basis), with a MIXED preparation.

The construction

driveStage Φ moves the system coordinate by Φ : Xsel → Xsel and touches nothing else; drivenTwoStage idx₁ Φ idx₂ = stageTwo idx₂ ∘ driveStage Φ ∘ stageOne idx₁. The first register and bank ride through the drive (driveStage_register₁, driveStage_bank₁), so the t₁ record still persists structurally.

★ The reindexing identity (drivenJointRecordSector_eq): the joint record sector of the driven propagator is the joint record sector of the UNDRIVEN propagator at the reindexed second context idx₂ ∘ Φ. The second register's reading depends on the system only through idx₂, and the system it sees is Φ of the relocated one (swapEvolve_register_comp). So the drive is, at the level of records, a change of the second context — and Q25's generic engine two_stage_joint applies verbatim.

Main results

• Generic (Xsel): driveStage, drivenTwoStage, drivenJointRecordSector; ★ drivenJointRecordSector_eq; ★★ driven_two_stage_joint — the joint law factors as (stage-1 sector) × (stage-2 sector at idx₂ ∘ Φ).

• On Σ = ℂℙ^{N−1} × T²: baseLift Φ' (a base map lifted to the sector, the fibre untouched — baseLift_unitary_smul: for a unitary it is the corpus's U(N) action on KSigma); ContextField.pullback (the context "measure after the flow"), with ★ basinIndex_pullback (basinIndex (c.pullback Φ') = basinIndex c ∘ baseLift Φ').

• The mixed first stage in a rotated basis: mixedReadyPrep_prod_sector (the mixed preparation's sector weight under ANY context and ANY bank is the eigenvalue mixture of the context's rates), mixed_outcome_pos_ctx (positivity licenses conditioning), ★ spectral_born_ctx_eq_traceForm (that mixture, in an orthonormal basis b, is Tr(ρ ∣bᵢ⟩⟨bᵢ∣) — spectral_born_eq_traceForm at a general basis).

• ★★ driven_mixed_two_time_born — the two-time law with a drive: for a density operator ρ, first readout in the orthonormal basis b, a measurable base map Φ' between the readouts, and an arbitrary second context c₂,

  P(record i at t₁ ∧ record j at t₂) = Tr(ρ ∣bᵢ⟩⟨bᵢ∣) · c₂.rate (Φ' [bᵢ]) j;

  driven_mixed_two_time_first_record — the drive and the second apparatus cannot retro-act on the first record.

⚠️ Honest scope

• The drive acts on the BASE and leaves the pointer fibre alone (baseLift): between the two readouts the system is isolated from both apparatus, and its ontic base point moves by the flow. A drive that also stirs the fibre is not modelled.
• The drive sits between the two crossings as a composed map, exactly as the two stages do; the clock-glued single-propagator form remains two-time-luders-scoping.md's gated presentation item.
• Φ' is an arbitrary measurable map. Invertibility, a flow law and Hamiltonian generation are not hypotheses of the joint-law theorem. The second context is an arbitrary normalized rate field; it becomes a quantum Born readout when specialized to a basis context.
• Rank-one readouts, one bank per measurement, the vertex-calibrated bank for the second apparatus (any probability bank would do — sector_born_ctx is bank-generic).

References

specs/BACKLOG.md (▶ OPEN QUEUE #4 = TH5d, the consumer; Q25); specs/two-time-luders-scoping.md; RecordLayer/TwoTimeLuders.lean (stageOne, stageTwo, regroup, two_stage_joint, two_stage_first_record); RecordLayer/SwapWitness.lean (swapEvolve_fwd, swapG_register); RecordLayer/RotatedSwap.lean (basisPoint, sector_born_ctx, prep_outcome_pos_ctx); RecordLayer/RotatedContext.lean (basisContext, basisContext_rate_mk); RecordLayer/MixedLuders.lean (mixedReadyPrep, mixed_outcome_pos); RecordLayer/MixedSwap.lean (eigRay, spectral_born_eq_traceForm); LF4/KahlerInstance.lean (instSMulKSigma); specs/future-work.md.

The drive between the two measurements

def CSD.RecordLayer.driveStage {Xsel : Type u_1} {K : ℕ} (Φ : Xsel → Xsel) (x : TwoStageArena Xsel K) : TwoStageArena Xsel K

The drive: move the system coordinate by Φ; both registers and both banks ride.

Equations

• CSD.RecordLayer.driveStage Φ x = (((Φ x.1.1.1, x.1.1.2), x.1.2), x.2)

theorem CSD.RecordLayer.driveStage_register₁ {Xsel : Type u_1} {K : ℕ} (Φ : Xsel → Xsel) (x : TwoStageArena Xsel K) : (driveStage Φ x).1.1.2 = x.1.1.2

theorem CSD.RecordLayer.driveStage_bank₁ {Xsel : Type u_1} {K : ℕ} (Φ : Xsel → Xsel) (x : TwoStageArena Xsel K) : (driveStage Φ x).1.2 = x.1.2

theorem CSD.RecordLayer.measurable_driveStage {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} {Φ : Xsel → Xsel} (hΦ : Measurable Φ) : Measurable (driveStage Φ)

noncomputable def CSD.RecordLayer.drivenTwoStage {Xsel : Type u_1} {K : ℕ} (idx₁ : Xsel → Fin K) (Φ : Xsel → Xsel) (idx₂ : Xsel → Fin K) : TwoStageArena Xsel K → TwoStageArena Xsel K

The driven two-time propagator: stage 1, the drive, stage 2.

Equations

• CSD.RecordLayer.drivenTwoStage idx₁ Φ idx₂ = CSD.RecordLayer.stageTwo idx₂ ∘ CSD.RecordLayer.driveStage Φ ∘ CSD.RecordLayer.stageOne idx₁

theorem CSD.RecordLayer.measurable_drivenTwoStage {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₁ : Xsel → Fin K) {Φ : Xsel → Xsel} (idx₂ : Xsel → Fin K) (h₁ : Measurable idx₁) (hΦ : Measurable Φ) (h₂ : Measurable idx₂) : Measurable (drivenTwoStage idx₁ Φ idx₂)

def CSD.RecordLayer.drivenJointRecordSector {Xsel : Type u_1} {K : ℕ} (idx₁ : Xsel → Fin K) (Φ : Xsel → Xsel) (idx₂ : Xsel → Fin K) (i j : Fin K) : Set (TwoStageArena Xsel K)

The driven joint record sector: the initial states destined to display record i at t₁ and, after the drive, record j at t₂.

Equations

• CSD.RecordLayer.drivenJointRecordSector idx₁ Φ idx₂ i j = CSD.RecordLayer.drivenTwoStage idx₁ Φ idx₂ ⁻¹' (CSD.RecordLayer.recordOneEvent i ∩ CSD.RecordLayer.recordTwoEvent j)

★ The drive is a reindexing of the second context

theorem CSD.RecordLayer.swapEvolve_register_comp {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (Φ : Xsel → Xsel) (x : SwapArena Xsel K) : (swapEvolve idx 0 1 ((Φ x.1.1, x.1.2), x.2)).1.2 = (swapEvolve (idx ∘ Φ) 0 1 x).1.2

The register after the crossing depends on the system only through the index: driving the system by Φ before a swap protocol at idx reads as the swap protocol at idx ∘ Φ.

theorem CSD.RecordLayer.stageTwo_driveStage_register₂ {Xsel : Type u_1} {K : ℕ} (idx₂ : Xsel → Fin K) (Φ : Xsel → Xsel) (y : TwoStageArena Xsel K) : (stageTwo idx₂ (driveStage Φ y)).2.1 = (stageTwo (idx₂ ∘ Φ) y).2.1

The second register after the driven stage 2 is the second register after the undriven stage 2 at the reindexed context.

theorem CSD.RecordLayer.drivenJointRecordSector_eq {Xsel : Type u_1} {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) (Φ : Xsel → Xsel) (i j : Fin K) : drivenJointRecordSector idx₁ Φ idx₂ i j = jointRecordSector idx₁ (idx₂ ∘ Φ) i j

★ The drive is a reindexing of the second context, at the level of record sectors: the driven joint sector at (idx₁, Φ, idx₂) IS the undriven joint sector at (idx₁, idx₂ ∘ Φ). The first record never sees the drive; the second register's reading depends on the system only through the index, and the system it reads is Φ of the relocated one.

theorem CSD.RecordLayer.drivenTwoStage_preimage_recordOne {Xsel : Type u_1} {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) (Φ : Xsel → Xsel) (i : Fin K) : drivenTwoStage idx₁ Φ idx₂ ⁻¹' recordOneEvent i = twoStage idx₁ (idx₂ ∘ Φ) ⁻¹' recordOneEvent i

The drive does not move the first-record event.

theorem CSD.RecordLayer.driven_two_stage_joint {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) {Φ : Xsel → Xsel} (h₁ : Measurable idx₁) (hΦ : Measurable Φ) (h₂ : Measurable idx₂) (μ12 : MeasureTheory.Measure (Xsel × LF4.KTorus)) [MeasureTheory.IsProbabilityMeasure μ12] (ν₁ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₁ j)] (μR₂ : MeasureTheory.Measure LF4.KTorus) [MeasureTheory.IsProbabilityMeasure μR₂] (ν₂ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₂ j)] (i j : Fin K) (hpos : μ12 ((shearProtocol idx₁ h₁).outcomeSector i) ≠ 0) : (twoStagePrep μ12 ν₁ μR₂ ν₂) (drivenJointRecordSector idx₁ Φ idx₂ i j) = (μ12.prod (MeasureTheory.Measure.pi ν₁)) ((swapProtocol idx₁ h₁).outcomeSector i) * (((ν₁ i).prod μR₂).prod (MeasureTheory.Measure.pi ν₂)) ((swapProtocol (idx₂ ∘ Φ) ⋯).outcomeSector j)

★★ The generic driven two-stage composition: the joint two-record probability with a drive Φ between the readouts factors as (stage-1 sector measure) × (stage-2 sector measure at the relocated state, for the reindexed context idx₂ ∘ Φ). two_stage_joint through the reindexing identity.

The sector flow of a base map, and the pulled-back context

def CSD.RecordLayer.baseLift {N : ℕ} (Φ' : LF4.CPN N → LF4.CPN N) : LF4.KSigma N → LF4.KSigma N

A base map lifted to the sector: the ontic base point moves, the pointer fibre rides.

Equations

• CSD.RecordLayer.baseLift Φ' = Prod.map Φ' id

@[simp]

theorem CSD.RecordLayer.baseLift_apply {N : ℕ} (Φ' : LF4.CPN N → LF4.CPN N) (x : LF4.KSigma N) : baseLift Φ' x = (Φ' x.1, x.2)

theorem CSD.RecordLayer.measurable_baseLift {N : ℕ} {Φ' : LF4.CPN N → LF4.CPN N} (hΦ' : Measurable Φ') : Measurable (baseLift Φ')

theorem CSD.RecordLayer.baseLift_unitary_smul {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : (baseLift fun (p : LF4.CPN N) => U • p) = fun (x : LF4.KSigma N) => U • x

For a unitary, the lifted base action IS the corpus's U(N) action on Σ (LF4/KahlerInstance.lean, instSMulKSigma).

noncomputable def CSD.RecordLayer.ContextField.pullback {N : ℕ} (c : ContextField N) (Φ' : LF4.CPN N → LF4.CPN N) (hΦ' : Measurable Φ') : ContextField N

The pulled-back context: the apparatus c read AFTER the base flow Φ' — its rate at p is c's rate at Φ' p.

Equations

• c.pullback Φ' hΦ' = { rate := fun (p : CSD.LF4.CPN N) (i : Fin N) => c.rate (Φ' p) i, measurable_rate := ⋯, nonneg := ⋯, sum_one := ⋯ }

@[simp]

theorem CSD.RecordLayer.ContextField.pullback_rate {N : ℕ} (c : ContextField N) (Φ' : LF4.CPN N → LF4.CPN N) (hΦ' : Measurable Φ') (p : LF4.CPN N) (i : Fin N) : (c.pullback Φ' hΦ').rate p i = c.rate (Φ' p) i

theorem CSD.RecordLayer.globalBasin_pullback {N : ℕ} (c : ContextField N) (Φ' : LF4.CPN N → LF4.CPN N) (hΦ' : Measurable Φ') (i : Fin N) : globalBasin (c.pullback Φ' hΦ') i = baseLift Φ' ⁻¹' globalBasin c i

The basins of the pulled-back context are the pulled-back basins.

theorem CSD.RecordLayer.basinIndex_pullback {N : ℕ} [NeZero N] (c : ContextField N) (Φ' : LF4.CPN N → LF4.CPN N) (hΦ' : Measurable Φ') : basinIndex (c.pullback Φ' hΦ') = basinIndex c ∘ baseLift Φ'

★ The pulled-back selector is the selector after the flow: reading the basin index of c after moving the base by Φ' is reading the basin index of c.pullback Φ'.

The mixed preparation under an arbitrary context and bank

theorem CSD.RecordLayer.mixedReadyPrep_prod_sector {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (c : ContextField N) (ν : Fin N → MeasureTheory.Measure (LF4.KSigma N)) [∀ (k : Fin N), MeasureTheory.IsProbabilityMeasure (ν k)] (i : Fin N) : ((mixedReadyPrep ρ).prod (MeasureTheory.Measure.pi ν)) ((swapProtocol (basinIndex c) ⋯).outcomeSector i) = ENNReal.ofReal (∑ j : Fin N, ⋯.eigenvalues j * c.rate (eigRay ρ j) i)

The mixed preparation's sector weight, for any context and any bank: the eigenvalue mixture of the context's rates at the spectral eigenrays.

theorem CSD.RecordLayer.mixed_outcome_pos_ctx {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (c : ContextField N) (i : Fin N) (hpos : ∑ j : Fin N, ⋯.eigenvalues j * c.rate (eigRay ρ j) i ≠ 0) : (mixedReadyPrep ρ) ((shearProtocol (basinIndex c) ⋯).outcomeSector i) ≠ 0

Positivity licenses the conditioning, for any context: a nonzero mixed rate gives the outcome sector nonzero mixed measure. mixed_outcome_pos at a general context field.

theorem CSD.RecordLayer.spectral_born_ctx_eq_traceForm {N : ℕ} (ρ : LF2.DensityOperator N) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : ∑ j : Fin N, ⋯.eigenvalues j * (basisContext b).rate (eigRay ρ j) i = LF2.traceForm ρ (LF2.rankOneEffect (b i) ⋯)

★ The spectral bridge in an arbitrary orthonormal basis: the eigenvalue mixture of the basis-b rates at the eigenrays is the density-operator Born probability Tr(ρ ∣bᵢ⟩⟨bᵢ∣). spectral_born_eq_traceForm with the standard basis replaced by b.

★★ The two-time law with a drive, for a mixed preparation in a rotated basis

noncomputable def CSD.RecordLayer.rotatedMixedTwoPrep {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ρ : LF2.DensityOperator N) : MeasureTheory.Measure (TwoStageArena (LF4.KSigma N) N)

The two-stage preparation of a mixed system whose first readout is in the orthonormal basis b: mixedReadyPrep ρ with the bank calibrated to the rotated vertices [bₖ] (rotatedBank b), and a fresh ready register with the vertex-calibrated bank for the second apparatus.

Equations

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

instance CSD.RecordLayer.instIsProbabilityMeasureTwoStageArenaKSigmaRotatedMixedTwoPrep {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ρ : LF2.DensityOperator N) : MeasureTheory.IsProbabilityMeasure (rotatedMixedTwoPrep b ρ)

theorem CSD.RecordLayer.driven_mixed_two_time_born_of_ne_zero {N : ℕ} [NeZero N] (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ρ : LF2.DensityOperator N) {Φ' : LF4.CPN N → LF4.CPN N} (hΦ' : Measurable Φ') (c₂ : ContextField N) (i j : Fin N) (hpos : LF2.traceForm ρ (LF2.rankOneEffect (b i) ⋯) ≠ 0) : (rotatedMixedTwoPrep b ρ) (drivenJointRecordSector (basinIndex (basisContext b)) (baseLift Φ') (basinIndex c₂) i j) = ENNReal.ofReal (LF2.traceForm ρ (LF2.rankOneEffect (b i) ⋯)) * ENNReal.ofReal (c₂.rate (Φ' (basisPoint b i)) j)

★★ Measure, drive, measure — the two-time law with a flow between the readouts. For a density operator ρ, a first readout in the orthonormal basis b, a measurable base map Φ' applied between the readouts, and an ARBITRARY second context c₂:

P(record i at t₁ ∧ record j at t₂) = Tr(ρ ∣bᵢ⟩⟨bᵢ∣) · c₂.rate (Φ' [bᵢ]) j.

This conditional helper uses a nonzero first-outcome weight to invoke the conditioned law. The first factor is the Born weight in basis b; the second is the supplied context rate at Φ' [bᵢ]. For a basis context the latter is a Born weight. The final theorem driven_mixed_two_time_born also covers zero first-outcome weight.

theorem CSD.RecordLayer.driven_mixed_two_time_first_record {N : ℕ} [NeZero N] (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ρ : LF2.DensityOperator N) (Φ' : LF4.CPN N → LF4.CPN N) (c₂ : ContextField N) (i : Fin N) : (rotatedMixedTwoPrep b ρ) (drivenTwoStage (basinIndex (basisContext b)) (baseLift Φ') (basinIndex c₂) ⁻¹' recordOneEvent i) = ENNReal.ofReal (LF2.traceForm ρ (LF2.rankOneEffect (b i) ⋯))

No retro-action: neither the drive nor the second apparatus disturbs the first record's mixed Born law in the basis b.

theorem CSD.RecordLayer.driven_mixed_two_time_born {N : ℕ} [NeZero N] (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ρ : LF2.DensityOperator N) {Φ' : LF4.CPN N → LF4.CPN N} (hΦ' : Measurable Φ') (c₂ : ContextField N) (i j : Fin N) : (rotatedMixedTwoPrep b ρ) (drivenJointRecordSector (basinIndex (basisContext b)) (baseLift Φ') (basinIndex c₂) i j) = ENNReal.ofReal (LF2.traceForm ρ (LF2.rankOneEffect (b i) ⋯)) * ENNReal.ofReal (c₂.rate (Φ' (basisPoint b i)) j)

The driven joint law for every first outcome, including zero-probability outcomes. The first bank is calibrated to the basis rays and both apparatus are independently prepared. The second factor is the supplied context rate; for a basis context it is a Born weight.