SigmaLayer/RotatedSwap: the first measurement in any basis — the unitary-covariance law

Category: 7-SigmaLayer (dynamical measurement — the covariance extension).

What this closes

RotatedContext.lean built the rotated context field and extended the sequential layer's follow-up reads to arbitrary bases; the first measurement stayed hardwired to the computational basis (selector basinIndex (momentContext N), bank calibrated on the computational vertices). That asymmetry — the reason BB84Sequential had to run the dual round — ends here:

• ★ sector_born_ctx / prep_outcome_pos_ctx / readyBankPrep_selReadyBank — the swap-arena Born and conditioning-positivity lemmas, generic in the context field and the bank calibration. The momentContext instances in SwapClosure.lean predate these and stand; the generic forms subsume them.
• ★ rotated_swap_luders_born — the Lüders update for a first measurement in any orthonormal basis bON: selector basinIndex (basisContext bON), bank calibrated on the rotated vertices [bONᵢ]; conditioned on outcome i, follow-up statistics for any context are the collapsed state's rates c'.rate [bONᵢ]. Pure instantiation: swap_luders_marginal was always selector- and calibration-generic — the missing pieces were only the rotated Born accounting.
• ★★ measurement_covariance — the unitary-covariance law, in closure form: for every orthonormal basis and every state, the full six-fact measurement closure (RotatedSwapClosure: ready ⇒ no record, record created, exclusivity, persistence, dynamical Born ‖⟨bONᵢ, ψ⟩‖², Lüders to [bONᵢ]) holds on the swap arena. The apparatus basis is a parameter of the context field, not a preferred structure of Σ.

What this retires

The BB84Sequential dual-round caveat (the primal round Alice-Z/Eve-X is now directly formalisable — see the corollary there), and the "arbitrary bases by unitary covariance" item of the extension list. Remaining extension items (mixed preparations in the dynamical model, POVM/instrument dynamics) stay recorded in specs/BACKLOG.md.

References

SigmaLayer/SwapClosure.lean (readyPrep, selReadyBank machinery, the momentContext instance); SigmaLayer/SwapLuders.lean (swap_luders_marginal — the generic engine); SigmaLayer/RotatedContext.lean (basisContext, basisContext_rate_mk); specs/BACKLOG.md.

The rotated vertices and bank

noncomputable def CSD.RecordLayer.basisPoint {N : ℕ} (bON : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : LF4.CPN N

The i-th rotated vertex: the basis ray [bONᵢ].

Equations

• CSD.RecordLayer.basisPoint bON i = Projectivization.mk ℂ (bON i) ⋯

noncomputable def CSD.RecordLayer.rotatedBank {N : ℕ} (bON : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : MeasureTheory.Measure (Fin N → LF4.KSigma N)

The rotated calibrated bank: slot k prepared at [bONₖ].

Equations

• CSD.RecordLayer.rotatedBank bON = MeasureTheory.Measure.pi fun (k : Fin N) => CSD.RecordLayer.epistemicMeasure (CSD.RecordLayer.basisPoint bON k)

instance CSD.RecordLayer.instIsProbabilityMeasureForallFinKSigmaRotatedBank {N : ℕ} (bON : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : MeasureTheory.IsProbabilityMeasure (rotatedBank bON)

The context-generic swap-arena accounting

theorem CSD.RecordLayer.readyBankPrep_selReadyBank {N : ℕ} [NeZero N] (c : ContextField N) (ν : Fin N → MeasureTheory.Measure (LF4.KSigma N)) [∀ (k : Fin N), MeasureTheory.IsProbabilityMeasure (ν k)] (p : LF4.CPN N) (i : Fin N) : ((readyPrep p).prod (MeasureTheory.Measure.pi ν)) (selReadyBank (basinIndex c) i) = ENNReal.ofReal (c.rate p i)

The ready preparation weights the selector-and-ready-and-bank set with the context's rate — for any context field and any probability bank. Generalises swapPrep_selReadyBank.

theorem CSD.RecordLayer.readyBankPrep_cover {N : ℕ} [NeZero N] (c : ContextField N) (ν : Fin N → MeasureTheory.Measure (LF4.KSigma N)) [∀ (k : Fin N), MeasureTheory.IsProbabilityMeasure (ν k)] (p : LF4.CPN N) : ∑ i : Fin N, ((readyPrep p).prod (MeasureTheory.Measure.pi ν)) (selReadyBank (basinIndex c) i) = 1

theorem CSD.RecordLayer.sector_born_ctx {N : ℕ} [NeZero N] (c : ContextField N) (ν : Fin N → MeasureTheory.Measure (LF4.KSigma N)) [∀ (k : Fin N), MeasureTheory.IsProbabilityMeasure (ν k)] (p : LF4.CPN N) (i : Fin N) : ((readyPrep p).prod (MeasureTheory.Measure.pi ν)) ((swapProtocol (basinIndex c) ⋯).outcomeSector i) = ENNReal.ofReal (c.rate p i)

★ The context-generic dynamical Born: the outcome sector's measure is the context's rate at the preparation, for any context field and bank.

theorem CSD.RecordLayer.prep_outcome_pos_ctx {N : ℕ} [NeZero N] (c : ContextField N) (p : LF4.CPN N) (i : Fin N) (hpos : c.rate p i ≠ 0) : (readyPrep p) ((shearProtocol (basinIndex c) ⋯).outcomeSector i) ≠ 0

The context-generic conditioning positivity: the outcome sector has nonzero measure whenever the context's rate does. Generalises prep_outcome_pos.

★ Lüders for a first measurement in any basis

theorem CSD.RecordLayer.rotated_swap_luders_born {N : ℕ} [NeZero N] (bON : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) (hpos : ‖inner ℂ (bON i) ψ‖ ^ 2 ≠ 0) (c' : ContextField N) (j : Fin N) : ((swapProtocol (basinIndex (basisContext bON)) ⋯).postMeasure ((readyPrep (Projectivization.mk ℂ ψ hψ0)).prod (rotatedBank bON)) i) ((fun (y : SwapArena (LF4.KSigma N) N) => y.1.1) ⁻¹' globalBasin c' j) = ENNReal.ofReal (c'.rate (basisPoint bON i) j)

★ The rotated Lüders update. First measurement in the basis bON (selector = the rotated context's basins, bank calibrated on the rotated vertices), conditioned on outcome i: the follow-up outcome-j probability for any context field c' is the collapsed state's rate c'.rate [bONᵢ] j.

★★ The covariance law, in closure form

structure CSD.RecordLayer.RotatedSwapClosure {N : ℕ} [NeZero N] (bON : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) : Prop

The rotated measurement closure: the six dynamical facts for a first measurement in the orthonormal basis bON.

• ready_no_record (x : SwapArena (LF4.KSigma N) N) : x.1.2 ∈ readyArc N → (swapProtocol (basinIndex (basisContext bON)) ⋯).readout x = none

  Ready ⇒ no record.

• record_created (i : Fin N) (x : SwapArena (LF4.KSigma N) N) : x ∈ selReadyBank (basinIndex (basisContext bON)) i → (swapProtocol (basinIndex (basisContext bON)) ⋯).readout ((swapProtocol (basinIndex (basisContext bON)) ⋯).evolve 0 1 x) = some i

  A record is created, and it is the rotated-basin outcome the selector fixed.

• outcomes_exclusive : Pairwise (Function.onFun Disjoint (swapProtocol (basinIndex (basisContext bON)) ⋯).outcomeSector)

  Distinct outcomes are exclusive.

• record_persists (i : Fin N) (x : SwapArena (LF4.KSigma N) N) (t : SigmaLayer.OnticTime) : x ∈ (swapProtocol (basinIndex (basisContext bON)) ⋯).outcomeSector i → 1 ≤ t → t ≤ 1 + 1 → (swapProtocol (basinIndex (basisContext bON)) ⋯).readout ((swapProtocol (basinIndex (basisContext bON)) ⋯).evolve 0 t x) = some i

  The record persists across the operational window.

• sector_born (hψ0 : ψ ≠ 0) : ‖ψ‖ = 1 → ∀ (i : Fin N), ((readyPrep (Projectivization.mk ℂ ψ hψ0)).prod (rotatedBank bON)) ((swapProtocol (basinIndex (basisContext bON)) ⋯).outcomeSector i) = ENNReal.ofReal (‖inner ℂ (bON i) ψ‖ ^ 2)

  The dynamical Born in the rotated basis: the outcome sector's measure is ‖⟨bONᵢ, ψ⟩‖².

• luders_followup (hψ0 : ψ ≠ 0) : ‖ψ‖ = 1 → ∀ (i : Fin N), ‖inner ℂ (bON i) ψ‖ ^ 2 ≠ 0 → ∀ (c' : ContextField N) (j : Fin N), ((swapProtocol (basinIndex (basisContext bON)) ⋯).postMeasure ((readyPrep (Projectivization.mk ℂ ψ hψ0)).prod (rotatedBank bON)) i) ((fun (y : SwapArena (LF4.KSigma N) N) => y.1.1) ⁻¹' globalBasin c' j) = ENNReal.ofReal (c'.rate (basisPoint bON i) j)

  The rotated Lüders update, conditioning licensed by the rotated Born weight.

theorem CSD.RecordLayer.measurement_covariance {N : ℕ} [NeZero N] (bON : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) : RotatedSwapClosure bON ψ

★★ The unitary-covariance law: the measurement closure holds for every orthonormal basis and every state — the apparatus basis is a parameter of the context field, not a preferred structure of Σ.