SigmaLayer/RotatedContext: context fields in an arbitrary orthonormal basis

Category: record layer / dynamical measurement (the first unitary-covariance step).

momentContext N is the context field of an apparatus measuring in the standard basis. This module produces the context field of an apparatus measuring in any orthonormal basis b:

basisContext b — rates are the moment map read in b-coordinates, via the projective coordinate change basisCoord b induced by the isometry ψ ↦ b.repr ψ.

The point (basisContext_rate_mk): at a unit preparation ψ, the rate of outcome i is ‖⟨b i, ψ⟩‖² — the Born weight in the rotated basis. Since csd_sequential_born (Empirical/CSD/SequentialMeasurement.lean) holds for any context field, this immediately extends the sequential-measurement layer to cross-basis follow-ups: measure in the computational basis, then read the collapsed state in any basis b. That is the missing piece for intercept-resend eavesdropping (Empirical/CSD/Crypto/BB84Sequential.lean), where Eve's computational-basis measurement is followed by Bob's conjugate-basis read.

Why this is the unitary-covariance seed

The recorded unitary-covariance extension asks for the full equivariance rate (U • p) = rate p ∘ σ(U) of the measurement layer under the projective unitary group. This module builds the object that extension quantifies over — the rotated context — and proves its ContextField obligations (measurability via Projectivization.mapOfInjective_continuous, the simplex constraints via transport along the isometry). (Addendum 2026-08-02: the equivariance law itself has since landed — SigmaLayer/RotatedSwap.lean, measurement_covariance.)

References

SigmaLayer/GlobalBasin.lean (ContextField, momentContext, globalBasin_prob); Mathlib/LinearAlgebra/Projectivization/Topology.lean (mapOfInjective_continuous — the staged continuity lemma); LF4/MomentMap.lean (momentMap_mk_eq_inner_sq, measurable_momentMap); Empirical/CSD/SequentialMeasurement.lean (the consumer); specs/BACKLOG.md (unitary covariance); specs/future-work.md.

theorem CSD.RecordLayer.repr_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (h : ψ ≠ 0) : b.repr ψ ≠ 0

If ψ ≠ 0 then its basis representation is nonzero — the coordinate isometry has trivial kernel.

noncomputable def CSD.RecordLayer.basisCoord {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : LF4.CPN N → LF4.CPN N

The projective coordinate change induced by an orthonormal basis b: the descent of the isometry ψ ↦ b.repr ψ to ℂℙ^{N−1}.

Equations

• CSD.RecordLayer.basisCoord b = Projectivization.map ↑b.repr.toLinearEquiv ⋯

theorem CSD.RecordLayer.basisCoord_mk {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : basisCoord b (Projectivization.mk ℂ ψ hψ0) = Projectivization.mk ℂ (b.repr ψ) ⋯

theorem CSD.RecordLayer.continuous_basisCoord {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : Continuous (basisCoord b)

noncomputable def CSD.RecordLayer.basisContext {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : ContextField N

The rotated context field: the context of an apparatus measuring in the orthonormal basis b. Rates are the moment map read in b-coordinates; the ContextField obligations transport along the coordinate isometry. basisContext of the standard basis has the same rates as momentContext (basisContext_basisFun_rate, below).

Equations

• CSD.RecordLayer.basisContext b = { rate := fun (p : CSD.LF4.CPN N) (i : Fin N) => CSD.LF4.momentMap (CSD.RecordLayer.basisCoord b p) i, measurable_rate := ⋯, nonneg := ⋯, sum_one := ⋯ }

@[simp]

theorem CSD.RecordLayer.basisContext_rate {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (p : LF4.CPN N) : (basisContext b).rate p = LF4.momentMap (basisCoord b p)

theorem CSD.RecordLayer.basisContext_rate_mk {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) : (basisContext b).rate (Projectivization.mk ℂ ψ hψ0) i = ‖inner ℂ (b i) ψ‖ ^ 2

★ The rotated rate is the rotated Born weight. At a unit preparation ψ, the basis-b context assigns outcome i the weight ‖⟨b i, ψ⟩‖² — the Born rule in the rotated basis, obtained by transport rather than re-derivation.

theorem CSD.RecordLayer.basisContext_basisFun_rate {N : ℕ} (p : LF4.CPN N) (i : Fin N) : (basisContext (EuclideanSpace.basisFun (Fin N) ℂ)).rate p i = (momentContext N).rate p i

The standard basis reproduces momentContext: the rotated construction at EuclideanSpace.basisFun has literally the moment map's rates — the consistency claim, as a theorem rather than prose.