LF5's measurement flow produces the de-isolation channel

Category: 3-Local (W6′ of specs/qit-chain-scoping.md; the joint-index instance that closes the loop from LF5's ontic flow to the channel of LF6/DecoherenceChannel.lean).

LF2/FlowChannel.lean proves that a flow lifting a unitary produces the Stinespring channel of that unitary, with the lift hypothesis a theorem for the projective unitary action at index Fin N (isUnitaryLift_of_smul). LF5's measurement flow (LF5/MeasurementFlow.lean) is such an action, but on the dilated space reindexed along e : Fin N × Fin N ≃ Fin m, because the Fubini-Study infrastructure is Fin m-indexed. This module carries the lift back across the reindexing and instantiates the W6/W7 theorems on LF5's flow:

• isUnitaryLift_measurementFlow — an ontic sector over the dilated projective space whose flow projects to measurementFlow N e, with any unit section of the ray map, lifts vnUnitary N on the joint index through the representative transported back along e (isUnitaryLift_of_reindex, LF2/FlowChannel.lean);
• ★★ measurementFlow_traceRight_barycenter — for a preparation on that sector, product with the apparatus ready in a₀, the reduced density operator of the flowed preparation is deisolationChannel N applied to the system's density operator: the de-isolation channel is the environment marginal of LF5's flow;
• ★ measurementFlow_vonNeumannEntropy_le — the second law under LF5's flow: the system's reduced entropy after the flow is at least its entropy before (TH2's full-support hypothesis).

Honest scope

The unit section. The general theorems take a unit-norm measurable section rep' of the ray map (mk (rep' p) = p), as fromPreparation does; Projectivization.unitSection (Mathlib/LinearAlgebra/Projectivization/UnitSection.lean, W6″) is one, canonical and Borel measurable, and measurementFlow_traceRight_barycenter_unitSection is the theorem with it supplied, so no section hypothesis remains.

⚠️ The product form is a hypothesis. That the joint preparation is the system preparation tensored with the ready apparatus, at the projector level and almost everywhere, is what "the apparatus starts in a₀" means for a preparation; it is not derived from the sector.

References: specs/qit-chain-scoping.md (W6′); LF2/FlowChannel.lean (W6); LF6/DecoherenceChannel.lean (W5 witness); Thermo/SigmaSecondLaw.lean (W7); LF5/MeasurementFlow.lean (measurementFlow, vnUnitaryReindexed).

LF5's measurement flow lifts the von Neumann coupling

theorem CSD.LF6.isUnitaryLift_measurementFlow {N : ℕ} [NeZero N] {m : ℕ} {SigmaSpace : Type u_1} {G : Type u_2} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [Group G] [MulAction G SigmaSpace] [MulAction G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] [MulAction.IsPretransitive G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] (e : Fin N × Fin N ≃ Fin m) (D : LF2.SectorData SigmaSpace (Projectivization ℂ (EuclideanSpace ℂ (Fin m))) G) (Φ : SigmaSpace → SigmaSpace) (hproj : ∀ (x : SigmaSpace), D.π (Φ x) = LF5.measurementFlow N e (D.π x)) (rep' : Projectivization ℂ (EuclideanSpace ℂ (Fin m)) → EuclideanSpace ℂ (Fin m)) (hrep_unit : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), ‖rep' p‖ = 1) (hrep_ne : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), rep' p ≠ 0) (hsec : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), Projectivization.mk ℂ (rep' p) ⋯ = p) : LF2.IsUnitaryLift D Φ (fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))) => (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e).symm (rep' p)) (LF5.vnUnitary N)

The joint-index instance (W6′). An ontic sector over the dilated projective space whose flow projects to LF5's measurementFlow N e (the projective action of the reindexed von Neumann coupling), with any unit section rep' of the ray map, lifts vnUnitary N on the joint index Fin N × Fin N, through the representative transported back along e.

The de-isolation channel is the environment marginal of that flow

theorem CSD.LF6.measurementFlow_traceRight_barycenter {N : ℕ} [NeZero N] {m : ℕ} {SigmaSpace : Type u_1} {G : Type u_2} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [Group G] [MulAction G SigmaSpace] [MulAction G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] [MulAction.IsPretransitive G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] (e : Fin N × Fin N ≃ Fin m) (D : LF2.SectorData SigmaSpace (Projectivization ℂ (EuclideanSpace ℂ (Fin m))) G) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (Φ : SigmaSpace → SigmaSpace) (hΦ : Measurable Φ) (hproj : ∀ (x : SigmaSpace), D.π (Φ x) = LF5.measurementFlow N e (D.π x)) (rep' : Projectivization ℂ (EuclideanSpace ℂ (Fin m)) → EuclideanSpace ℂ (Fin m)) (hrep_unit : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), ‖rep' p‖ = 1) (hrep_ne : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), rep' p ≠ 0) (hsec : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), Projectivization.mk ℂ (rep' p) ⋯ = p) (hrep_meas : Measurable rep') (repS : Projectivization ℂ (EuclideanSpace ℂ (Fin m)) → EuclideanSpace ℂ (Fin N)) (hrepS_meas : Measurable repS) (hprod : ∀ᵐ (x : SigmaSpace) ∂μprep, LF2.outerProduct ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e).symm (rep' (D.π x))) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS (D.π x))) (LF2.outerProduct (EuclideanSpace.single 0 1))) : (LF2.barycenterMatrix (fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))) => (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e).symm (rep' p)) (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ μprep))).traceRight = (deisolationChannel N).apply (LF2.barycenterMatrix repS (MeasureTheory.Measure.map D.π μprep))

★★ LF5's measurement flow produces the de-isolation channel. For a preparation on a sector over the dilated projective space whose flow projects to measurementFlow N e, with a unit section of the ray map and the preparation a product with the apparatus ready in a₀ (a.e., at the projector level, in the representative transported back to Fin N × Fin N), the reduced density operator of the flowed preparation is deisolationChannel N applied to the system's density operator. The loop from the ontic flow of LF5 to the channel of LF6/DecoherenceChannel closes: the de-isolation channel is the environment marginal of that flow.

theorem CSD.LF6.measurementFlow_vonNeumannEntropy_le {N : ℕ} [NeZero N] {m : ℕ} {SigmaSpace : Type u_1} {G : Type u_2} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [Group G] [MulAction G SigmaSpace] [MulAction G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] [MulAction.IsPretransitive G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] (e : Fin N × Fin N ≃ Fin m) (D : LF2.SectorData SigmaSpace (Projectivization ℂ (EuclideanSpace ℂ (Fin m))) G) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (Φ : SigmaSpace → SigmaSpace) (hΦ : Measurable Φ) (hproj : ∀ (x : SigmaSpace), D.π (Φ x) = LF5.measurementFlow N e (D.π x)) (rep' : Projectivization ℂ (EuclideanSpace ℂ (Fin m)) → EuclideanSpace ℂ (Fin m)) (hrep_unit : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), ‖rep' p‖ = 1) (hrep_ne : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), rep' p ≠ 0) (hsec : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), Projectivization.mk ℂ (rep' p) ⋯ = p) (hrep_meas : Measurable rep') (repS : Projectivization ℂ (EuclideanSpace ℂ (Fin m)) → EuclideanSpace ℂ (Fin N)) (hrepS_unit : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))), ‖repS p‖ = 1) (hrepS_meas : Measurable repS) (hprod : ∀ᵐ (x : SigmaSpace) ∂μprep, LF2.outerProduct ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e).symm (rep' (D.π x))) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS (D.π x))) (LF2.outerProduct (EuclideanSpace.single 0 1))) (hpos : ∀ (i : Fin N), 0 < (LF2.barycenterMatrix repS (MeasureTheory.Measure.map D.π μprep) i i).re) : QuantumInfo.vonNeumannEntropy ⋯ ≤ QuantumInfo.vonNeumannEntropy ⋯

★ The second law under LF5's measurement flow: the entropy of the system's reduced density operator after the flow is at least its entropy before (full support of the system state assumed, TH2's hypothesis).

theorem CSD.LF6.measurementFlow_traceRight_barycenter_unitSection {N : ℕ} [NeZero N] {m : ℕ} {SigmaSpace : Type u_1} {G : Type u_2} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [Group G] [MulAction G SigmaSpace] [MulAction G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] [MulAction.IsPretransitive G (Projectivization ℂ (EuclideanSpace ℂ (Fin m)))] (e : Fin N × Fin N ≃ Fin m) (D : LF2.SectorData SigmaSpace (Projectivization ℂ (EuclideanSpace ℂ (Fin m))) G) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (Φ : SigmaSpace → SigmaSpace) (hΦ : Measurable Φ) (hproj : ∀ (x : SigmaSpace), D.π (Φ x) = LF5.measurementFlow N e (D.π x)) (repS : Projectivization ℂ (EuclideanSpace ℂ (Fin m)) → EuclideanSpace ℂ (Fin N)) (hrepS_meas : Measurable repS) (hprod : ∀ᵐ (x : SigmaSpace) ∂μprep, LF2.outerProduct ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e).symm (D.π x).unitSection) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS (D.π x))) (LF2.outerProduct (EuclideanSpace.single 0 1))) : (LF2.barycenterMatrix (fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin m))) => (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e).symm p.unitSection) (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ μprep))).traceRight = (deisolationChannel N).apply (LF2.barycenterMatrix repS (MeasureTheory.Measure.map D.π μprep))

★★ Unconditional form: with the canonical measurable unit section as representative, the section hypotheses disappear. The reduced density operator of the flowed preparation is the de-isolation channel applied to the system's density operator, for every preparation on a sector whose flow projects to LF5's measurement flow and is a product with the apparatus ready.