Channels from Σ-flows: the density operator of a flowed preparation #
Category: 3-Local (W6 of specs/qit-chain-scoping.md; the CSD origin of the channels the
QIT layer reasons about).
W3 (LF2/PreparationBarycenter.lean) made the density operator of a preparation the barycentre
∫ |rep ψ⟩⟨rep ψ| d(π_* μprep) of rank-one projectors along its projective law. This module
follows that object along an ontic flow. If the flow Φ : Σ → Σ lifts a unitary U through
the projection and the representative — |rep (π (Φ x))⟩⟨…| = U |rep (π x)⟩⟨…| Uᴴ — then:
- ★★
barycenter_flow— closed system: the density operator of the flowed preparationΦ_* μprepisU ρ Uᴴ(unitaryChannel_apply_barycenter: the unitary channel ofUmaps the density operator of the preparation to that of the flowed preparation); - ★★
traceRight_barycenter_flow— open system: for a joint sectorsystem ⊗ environment, a preparation that is a product with the environment in a ready vectore₀, and a flow lifting the joint unitaryU, the reduced density operator of the flowed preparation is the Stinespring channelρ ↦ Tr_env (U (ρ ⊗ |e₀⟩⟨e₀|) Uᴴ)applied to the system's density operator. The channel (stinespringChannel, aQuantumInfo.Channelwith Kraus operators the environment blocks of the isometryU · embedEnv e₀) is produced by theΣ-flow.
The matrix-level inputs: barycenterMatrix_map (barycentre along a pushforward),
barycenterMatrix_conj (covariance under a projector-level conjugation),
barycenterMatrix_kronecker_of_ae (product preparations have Kronecker barycentres),
embedEnv with embedEnv_conjTranspose_mul (isometry) and embedEnv_mul_mul_conjTranspose
(E ρ Eᴴ = ρ ⊗ |e₀⟩⟨e₀|), outerProduct_toEuclideanLin (|U v⟩⟨U v| = U |v⟩⟨v| Uᴴ).
The lift hypothesis, and why it is not vacuous #
IsUnitaryLift D Φ rep U is stated at the projector level, so it is phase-free: rep is a
choice of unit representative and two representatives of one ray differ by a phase the projector
does not see. It follows from the vector-level lift (isUnitaryLift_of_vector) and — the
corpus's actual shape — from π (Φ x) = U • π x for the projective action of a unitary, for
any unit section rep (isUnitaryLift_of_smul). That is the projectable field of every
KahlerOnticSetup (LF4/NonTrivialSetup.lean, unitaryFlowSetup) and the form of LF5's
measurementFlow.
Honest scope #
⚠️ The survey row misdescribed the corpus. specs/qit-chain-scoping.md W6 called
RecordLayer.IsJointLift "the lift of a unitary U_t on ℂᴺ ⊗ ℂᴱ". It is not: it is the
pointer-arena stroke predicate (pointer agreement plus conserved rates and register). The corpus's
flows-lifting-unitaries are the projective actions above; this module builds W6 on those and on
the abstract SectorData interface, at the QM theorem's level of generality.
Mixed environments. traceRight_barycenter_flow takes the environment in a fixed unit
vector e₀ (the LF5 apparatus ground state a₀). For a mixed environment state σ,
stinespringChannelMixed is the finite Kraus family √λₖ · (env-blocks of U · embedEnv vₖ) over a
spectral decomposition σ = ∑ₖ λₖ |vₖ⟩⟨vₖ| (isHermitian_eq_sum_eigenvalues_smul_outerProduct),
with action ρ ↦ Tr_env (U (ρ ⊗ σ) Uᴴ) (stinespringChannelMixed_apply); and ★★
traceRight_barycenter_flow_prod is the CSD theorem for a product preparation μS ⊗ μE on a
product sector: the environment state is then the barycentre of the environment preparation
(barycenterMatrix_prod, Fubini), and the reduced flowed system state is that channel applied to
the system's density operator.
The lift hypothesis, discharged for projective actions. IsUnitaryLift says the ontic flow
projects to a unitary action through rep; for the corpus's KahlerOnticSetup flows it is a
theorem for any unit section (isUnitaryLift_of_smul) and unconditional with the canonical
measurable unit section Projectivization.unitSection (isUnitaryLift_unitSection,
Mathlib/LinearAlgebra/Projectivization/UnitSection.lean); for an abstract SectorData it is
what "the flow is the lift of U" means. Which unitary a given de-isolation flow lifts is the physics (LF5's vnUnitary for the
von Neumann coupling; LF6/DecoherenceChannel.lean instantiates it).
Index generality. The theorems are over any finite index; the projective-action instance
isUnitaryLift_of_smul is at Fin N because the corpus's projective unitary action
(Mathlib/LinearAlgebra/Projectivization/Unitary.lean) is. A joint Fin N × Fin E sector is fed
through it by reindexing (Fin N × Fin E ≃ Fin m, LF5's device): isUnitaryLift_of_reindex
transports the lift along piLpCongrLeft, and LF6/MeasurementFlowChannel.lean applies it to
LF5's measurementFlow (W6′).
References: specs/qit-chain-scoping.md (W6, W5); LF2/PreparationBarycenter.lean (W3);
Mathlib/QuantumInfo/Stinespring.lean (Channel.ofIsometry, ofIsometry_apply);
Mathlib/QuantumInfo/CanonicalChannels.lean (unitaryChannel);
LF5/DilationFromFlow.lean (embedGround, vnDilationV); LF6/Decoherence.lean
(decohereReduced, the instance in LF6/DecoherenceChannel.lean).
The entry function is the entry of the projector |rep p⟩⟨rep p|.
|U v⟩⟨U v| = U |v⟩⟨v| Uᴴ.
The barycentre under pushforward and under a lifted unitary #
The barycentre along a pushforward is the barycentre of the composed representative.
Covariance of the barycentre. If rep' is rep conjugated by U at the projector level
(|rep' p⟩⟨rep' p| = U |rep p⟩⟨rep p| Uᴴ for every p), the barycentres are conjugate too.
Product form. If the projector of rep is a.e. the Kronecker product of the projector
of repS with a fixed projector σ, the barycentre is the Kronecker product B_S ⊗ σ.
The barycentre only sees the representative almost everywhere.
A preparation living in a subspace has its barycentre there. If the representative is a.e.
fixed by a Hermitian projector-like matrix P (P (rep p) = rep p), the barycentre satisfies
P B Pᴴ = B.
The ready-environment embedding and the Stinespring channel of a unitary #
The embedding ψ ↦ ψ ⊗ e₀ of the system into system ⊗ environment with the environment
in the ready vector e₀, as a matrix: (embedEnv n e₀) (a, i) j = δ_{a j} · e₀ i.
Equations
Instances For
The embedding is an isometry when e₀ is a unit vector.
Conjugating by the embedding tensors on the ready projector: E ρ Eᴴ = ρ ⊗ |e₀⟩⟨e₀|.
The Stinespring channel of a unitary with a ready environment: couple the system to the
environment in e₀, evolve the joint by U, trace the environment out. Its Kraus operators are
the environment blocks of the isometry U · embedEnv e₀ (Channel.ofIsometry).
Equations
- CSD.LF2.stinespringChannel U hU e₀ he₀ = QuantumInfo.Channel.ofIsometry (U * CSD.LF2.embedEnv n e₀) ⋯
Instances For
The channel's action is ρ ↦ Tr_env (U (ρ ⊗ |e₀⟩⟨e₀|) Uᴴ).
Embedding the system vector with the ready environment tensors the projectors:
|ψ ⊗ e₀⟩⟨ψ ⊗ e₀| = |ψ⟩⟨ψ| ⊗ |e₀⟩⟨e₀|.
Channels from Σ-flows #
A Σ-flow lifts a unitary through the representative, at the projector level: along the
ontic flow Φ, the projector |rep (π x)⟩⟨rep (π x)| of the projected point is conjugated by
U. Phase-free by construction (projectors do not see the phase of rep), and implied by the
vector-level lift rep (π (Φ x)) = U (rep (π x)) (isUnitaryLift_of_vector) and by the
projective form π (Φ x) = U • π x for a section rep (isUnitaryLift_of_smul).
Equations
- CSD.LF2.IsUnitaryLift D Φ rep U = ∀ (x : SigmaSpace), CSD.LF2.outerProduct (rep (D.π (Φ x))) = U * CSD.LF2.outerProduct (rep (D.π x)) * U.conjTranspose
Instances For
The vector-level lift implies the projector-level lift.
The lift of an iterate is the power. If the ontic flow Φ lifts U then k applications
of Φ lift U ^ k: a circuit of k identical gates is the flow iterated k times.
★★ Closed system: the density operator of the flowed preparation is U ρ Uᴴ. If the
ontic flow Φ lifts U, the barycentre of the flowed preparation Φ_* μprep is the barycentre
of μprep conjugated by U — the Schrödinger-picture evolution of the density operator, derived
from the ontic flow.
The closed-system statement as a channel: the unitary channel of U maps the density
operator of the preparation to the density operator of the flowed preparation.
★★ The channel of a Σ-flow (open system). Let the joint sector carry a representative
rep : P → ℂⁿ ⊗ ℂᵉ, let the preparation be a product with the environment in the ready vector
e₀ (a.e., at the projector level, with system representative repS), and let the ontic flow Φ
lift the unitary U. Then the reduced density operator of the flowed preparation is the
Stinespring channel of U with ready environment e₀ applied to the density operator of the
system preparation: Tr_env ρ(Φ_* μprep) = Φ_U(ρ_S(μprep)). The channel is produced by the
Σ-flow; nothing about it is posited.
The product hypothesis in vector form: the joint representative is the system representative
embedded with the ready environment, rep (π x) = repS (π x) ⊗ e₀, a.e. along the preparation.
The projective unitary action lifts, for any unit section #
Non-vacuity of the lift hypothesis. If the flow projects to the projective action of a
unitary U (π (Φ x) = U • π x, the projectable shape of every KahlerOnticSetup) and rep
is a unit section of the projectivisation (mk (rep p) = p), then Φ lifts U at the projector
level: two unit representatives of one ray differ by a phase, which the projector does not see.
★ The lift hypothesis is unconditional for the projective action. With the canonical
measurable unit section Projectivization.unitSection as representative, every ontic flow that
projects to the action of a unitary lifts it.
A mixed environment: the Stinespring channel over a spectral decomposition #
A Hermitian matrix is the sum of its eigenvalues times the projectors onto an orthonormal eigenbasis (the spectral theorem in projector form).
The Stinespring channel of a unitary with a mixed environment state σ. Couple the system
to the environment in σ, evolve the joint by U, trace out the environment:
ρ ↦ Tr_env (U (ρ ⊗ σ) Uᴴ). Its Kraus operators are √λₖ · (env-block i of U · embedEnv vₖ) over
a spectral decomposition σ = ∑ₖ λₖ |vₖ⟩⟨vₖ|; the trace-preserving constraint is ∑ₖ λₖ = Tr σ = 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The mixed-environment channel's action is ρ ↦ Tr_env (U (ρ ⊗ σ) Uᴴ).
Product preparations: the environment state is the barycentre of the environment #
Fubini for barycentres. If the joint projector is pointwise the Kronecker product of the system and environment projectors, the barycentre along a product measure is the Kronecker product of the two barycentres.
★★ The channel of a Σ-flow with a mixed environment. The joint sector is a product
Σ_sys × Σ_env → P_sys × P_env; the preparation is the product μS ⊗ μE of a system preparation
and an environment preparation; the joint representative is the tensor of the two (projector
level); the ontic flow Φ lifts the joint unitary U. Then the reduced density operator of the
flowed preparation is the mixed-environment Stinespring channel — with environment state the
barycentre of the environment preparation — applied to the density operator of the system
preparation.
Reindexing the lift #
Transporting a vector along piLpCongrLeft e transports its projector along reindex e e.
reindex e e is multiplicative and commutes with ᴴ, so it respects conjugation.
The lift transports along a reindexing. If the representative on the reindexed space is
the transport of rep, a lift of the reindexed unitary is a lift of the unitary.