The second law, data processing and Landauer on Σ

Category: 3-Local (W7 of specs/qit-chain-scoping.md; the thermodynamic and information-theoretic theorems of the corpus instantiated on preparations under Σ-flows).

TH2 (Thermo/SecondLaw.lean), the data-processing inequality (Mathlib/QuantumInfo/ DataProcessing.lean) and TH4 (Thermo/Landauer.lean) are theorems about bare density matrices, a unitary U and a coarse-graining map pinch. W3 made the density operator of a preparation on Σ a definite matrix (the barycentre) and W6 made its evolution along an ontic flow lifting U a theorem. This module instantiates the three on that evolution, so each becomes a statement about Σ-regions under de-isolation:

• deisolationChannel_apply_eq_pinch — the coarse-graining of the second law is the de-isolation channel: on a Hermitian input, tracing the pointer out of the von Neumann coupling is exactly the pointer-basis pinching pinch of TH2. The pinch is not an extra postulated coarse-graining; it is the environment marginal of the de-isolation flow;
• ★ vonNeumannEntropy_flow_eq — entropy is conserved along the ontic flow (closed system);
• ★★ vonNeumannEntropy_le_pinching_flow — the second law on Σ: S(ρ(μprep)) = S(ρ(Φ_* μprep)) ≤ S(pinch ρ(Φ_* μprep)), reversible microdynamics on Σ, entropy production from coarse-graining;
• ★★ vonNeumannEntropy_le_deisolation — the second law under de-isolation: the entropy of the system's reduced density operator after a flow lifting the von Neumann coupling is at least its entropy before, because the reduced flowed state is the pinching;
• ★★ traceDist_traceRight_flow_le — data processing on Σ: de-isolation along a flow lifting any joint unitary cannot increase the trace distance of two preparations' reduced density operators;
• ★★ landauer_flow — Landauer on Σ: for a product preparation on a system-plus-bath sector whose bath preparation has the Gibbs state as its density operator, the entropy removed from the system preparation by an ontic flow lifting the joint unitary is at most β times the heat dumped into the bath (barycenter_flow_prod supplies the flowed joint state to landauer_bound).

Honest scope

⚠️ The hypotheses are TH2's and TH4's. The pinching inequality needs full support (strictly positive pointer weights), Landauer needs full-rank final marginals and a full-rank initial system state. These are inherited, not added. The lift hypothesis IsUnitaryLift is W6's (a theorem for the projective unitary actions, isUnitaryLift_of_smul; for LF5's reindexed measurement flow the joint-index instance is W6′). The Gibbs hypothesis of landauer_flow says the bath preparation is thermal; that a bath preparation on Σ has a Gibbs barycentre is not derived here (the canonical-typicality route, Thermo/CanonicalTypicality.lean, is the corpus's approach).

⚠️ Posits unchanged. The sector is posited (specs/POSITS.md); what is proved is that, given it and a flow lifting a unitary, the QIT thermodynamics of preparations holds as the QIT layer states it.

References: specs/qit-chain-scoping.md (W7); LF2/FlowChannel.lean (W6); LF6/DecoherenceChannel.lean; Thermo/SecondLaw.lean (pinch, vonNeumannEntropy_le_pinching); Thermo/Landauer.lean (landauer_bound); Mathlib/QuantumInfo/DataProcessing.lean (channel_traceDist_le).

Bookkeeping

theorem CSD.Thermo.vonNeumannEntropy_congr_of_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : A = B) : QuantumInfo.vonNeumannEntropy hA = QuantumInfo.vonNeumannEntropy hB

Von Neumann entropy depends only on the matrix (transport along an equality of matrices).

The de-isolation channel is the pointer-basis pinching

theorem CSD.Thermo.deisolationChannel_apply_eq_pinch {N : ℕ} [NeZero N] {ρ : Matrix (Fin N) (Fin N) ℂ} (hρ : ρ.IsHermitian) : (LF6.deisolationChannel N).apply ρ = pinch ρ

The coarse-graining of the second law is the de-isolation channel. On a Hermitian input, tracing the pointer out of the von Neumann coupling gives exactly the pointer-basis pinching: (deisolationChannel N).apply ρ = pinch ρ. The pinch of TH2 is not an extra postulated coarse-graining; it is the environment marginal of the de-isolation flow.

The second law on Σ, closed system

theorem CSD.Thermo.isProbabilityMeasure_projectiveLaw_flow {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : LF2.SectorData SigmaSpace P G) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (Φ : SigmaSpace → SigmaSpace) : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ μprep))

The projective law of the flowed preparation is a probability measure.

theorem CSD.Thermo.vonNeumannEntropy_flow_eq {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (D : LF2.SectorData SigmaSpace P G) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (Φ : SigmaSpace → SigmaSpace) (rep : P → EuclideanSpace ℂ ι) (hΦ : Measurable Φ) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (U : Matrix ι ι ℂ) (hU : U.conjTranspose * U = 1) (hlift : LF2.IsUnitaryLift D Φ rep U) : QuantumInfo.vonNeumannEntropy ⋯ = QuantumInfo.vonNeumannEntropy ⋯

★ Entropy is conserved along the ontic flow. The density operator of the flowed preparation is U ρ Uᴴ (barycenter_flow), and conjugation by a unitary preserves the spectrum.

theorem CSD.Thermo.vonNeumannEntropy_le_pinching_flow {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (D : LF2.SectorData SigmaSpace P G) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (Φ : SigmaSpace → SigmaSpace) (rep : P → EuclideanSpace ℂ ι) (hΦ : Measurable Φ) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (U : Matrix ι ι ℂ) (hU : U.conjTranspose * U = 1) (hlift : LF2.IsUnitaryLift D Φ rep U) (hpos : ∀ (i : ι), 0 < (LF2.barycenterMatrix rep (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ μprep)) i i).re) : QuantumInfo.vonNeumannEntropy ⋯ ≤ QuantumInfo.vonNeumannEntropy ⋯

★★ The second law on Σ. Along an ontic flow lifting a unitary, the entropy of a preparation is conserved, and pinching the flowed density operator to the pointer basis does not decrease it: S(ρ(μprep)) = S(ρ(Φ_* μprep)) ≤ S(pinch ρ(Φ_* μprep)), under the full-support hypothesis TH2 needs (strictly positive pointer weights after the flow). Reversible microdynamics on Σ, entropy production from coarse-graining.

The second law and data processing on Σ, open system

theorem CSD.Thermo.traceDist_traceRight_flow_le {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : LF2.SectorData SigmaSpace P G) {n : Type u_4} {e : Type u_5} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (μprep μprep' : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] [MeasureTheory.IsProbabilityMeasure μprep'] (Φ : SigmaSpace → SigmaSpace) (hΦ : Measurable Φ) (rep : P → EuclideanSpace ℂ (n × e)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (repS : P → EuclideanSpace ℂ n) (hrepS_unit : ∀ (p : P), ‖repS p‖ = 1) (hrepS_meas : Measurable repS) (U : Matrix (n × e) (n × e) ℂ) (hU : U.conjTranspose * U = 1) (e₀ : EuclideanSpace ℂ e) (he₀ : ‖e₀‖ = 1) (hlift : LF2.IsUnitaryLift D Φ rep U) (hprod : ∀ᵐ (x : SigmaSpace) ∂μprep, LF2.outerProduct (rep (D.π x)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS (D.π x))) (LF2.outerProduct e₀)) (hprod' : ∀ᵐ (x : SigmaSpace) ∂μprep', LF2.outerProduct (rep (D.π x)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS (D.π x))) (LF2.outerProduct e₀)) : QuantumInfo.traceDist ⋯ ≤ QuantumInfo.traceDist ⋯

★★ Data processing on Σ: de-isolation cannot increase the distinguishability of two preparations. For two preparations on a joint sector, both products with the environment ready in e₀, and an ontic flow lifting U, the trace distance of the reduced flowed density operators is at most the trace distance of the system density operators before the flow (channel_traceDist_le on the channel traceRight_barycenter_flow produces).

theorem CSD.Thermo.vonNeumannEntropy_le_deisolation {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : LF2.SectorData SigmaSpace P G) {N : ℕ} [NeZero N] (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (Φ : SigmaSpace → SigmaSpace) (hΦ : Measurable Φ) (rep : P → EuclideanSpace ℂ (Fin N × Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (repS : P → EuclideanSpace ℂ (Fin N)) (hrepS_unit : ∀ (p : P), ‖repS p‖ = 1) (hrepS_meas : Measurable repS) (hlift : LF2.IsUnitaryLift D Φ rep (LF5.vnUnitary N)) (hprod : ∀ᵐ (x : SigmaSpace) ∂μprep, LF2.outerProduct (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 de-isolation. For a preparation on the system-plus-apparatus sector, product with the apparatus ready in a₀, and an ontic flow lifting the von Neumann coupling vnUnitary N, the entropy of the system's reduced density operator after the flow is at least the entropy of the system's density operator before it. The reduced flowed state is the de-isolation channel's output, which is the pointer-basis pinching (deisolationChannel_apply_eq_pinch), and pinching does not decrease entropy (TH2). Full support of the system state is TH2's hypothesis.

Landauer on Σ

theorem CSD.Thermo.barycenter_flow_prod {SigmaS : Type u_1} {SigmaE : Type u_2} {PS : Type u_3} {PE : Type u_4} {G : Type u_5} [MeasurableSpace SigmaS] [MeasurableSpace SigmaE] [Nonempty SigmaS] [Nonempty SigmaE] [MeasurableSpace PS] [MeasurableSpace PE] [Group G] [MulAction G (SigmaS × SigmaE)] [MulAction G (PS × PE)] [MulAction.IsPretransitive G (PS × PE)] {n : Type u_6} {e : Type u_7} [Fintype n] [Fintype e] (D : LF2.SectorData (SigmaS × SigmaE) (PS × PE) G) (πS : SigmaS → PS) (πE : SigmaE → PE) (hπS : Measurable πS) (hπE : Measurable πE) (hπ : D.π = Prod.map πS πE) (μS : MeasureTheory.Measure SigmaS) [MeasureTheory.IsProbabilityMeasure μS] (μE : MeasureTheory.Measure SigmaE) [MeasureTheory.IsProbabilityMeasure μE] (Φ : SigmaS × SigmaE → SigmaS × SigmaE) (hΦ : Measurable Φ) (rep : PS × PE → EuclideanSpace ℂ (n × e)) (hrep_unit : ∀ (p : PS × PE), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (repS : PS → EuclideanSpace ℂ n) (repE : PE → EuclideanSpace ℂ e) (hprod : ∀ (p : PS) (q : PE), LF2.outerProduct (rep (p, q)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS p)) (LF2.outerProduct (repE q))) (U : Matrix (n × e) (n × e) ℂ) (hlift : LF2.IsUnitaryLift D Φ rep U) : LF2.barycenterMatrix rep (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ (μS.prod μE))) = U * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.barycenterMatrix repS (MeasureTheory.Measure.map πS μS)) (LF2.barycenterMatrix repE (MeasureTheory.Measure.map πE μE)) * star U

The joint density operator of a flowed product preparation is U (ρ_S ⊗ ρ_E) Uᴴ.

theorem CSD.Thermo.landauer_flow {SigmaS : Type u_1} {SigmaE : Type u_2} {PS : Type u_3} {PE : Type u_4} {G : Type u_5} [MeasurableSpace SigmaS] [MeasurableSpace SigmaE] [Nonempty SigmaS] [Nonempty SigmaE] [MeasurableSpace PS] [MeasurableSpace PE] [Group G] [MulAction G (SigmaS × SigmaE)] [MulAction G (PS × PE)] [MulAction.IsPretransitive G (PS × PE)] {n : Type u_6} {e : Type u_7} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] [Nonempty e] (D : LF2.SectorData (SigmaS × SigmaE) (PS × PE) G) (πS : SigmaS → PS) (πE : SigmaE → PE) (hπS : Measurable πS) (hπE : Measurable πE) (hπ : D.π = Prod.map πS πE) (μS : MeasureTheory.Measure SigmaS) [MeasureTheory.IsProbabilityMeasure μS] (μE : MeasureTheory.Measure SigmaE) [MeasureTheory.IsProbabilityMeasure μE] (Φ : SigmaS × SigmaE → SigmaS × SigmaE) (hΦ : Measurable Φ) (rep : PS × PE → EuclideanSpace ℂ (n × e)) (hrep_unit : ∀ (p : PS × PE), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (repS : PS → EuclideanSpace ℂ n) (hrepS_unit : ∀ (p : PS), ‖repS p‖ = 1) (hrepS_meas : Measurable repS) (repE : PE → EuclideanSpace ℂ e) (hprod : ∀ (p : PS) (q : PE), LF2.outerProduct (rep (p, q)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS p)) (LF2.outerProduct (repE q))) (U : Matrix (n × e) (n × e) ℂ) (hU : U.conjTranspose * U = 1) (hlift : LF2.IsUnitaryLift D Φ rep U) (HB : Matrix e e ℂ) (hHB : HB.IsHermitian) {β : ℝ} (hgibbs : LF2.barycenterMatrix repE (MeasureTheory.Measure.map πE μE) = gibbsState HB hHB β) (hpdS : (LF2.barycenterMatrix repS (MeasureTheory.Measure.map πS μS)).PosDef) (hpdS' : (LF2.barycenterMatrix rep (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ (μS.prod μE)))).traceRight.PosDef) (hpdB' : (LF2.barycenterMatrix rep (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ (μS.prod μE)))).traceLeft.PosDef) : QuantumInfo.vonNeumannEntropy ⋯ - QuantumInfo.vonNeumannEntropy ⋯ ≤ β * (energy HB (LF2.barycenterMatrix rep (MeasureTheory.Measure.map D.π (MeasureTheory.Measure.map Φ (μS.prod μE)))).traceLeft - energy HB (gibbsState HB hHB β))

★★ Landauer's principle on Σ. A product preparation on a system-plus-bath sector whose bath preparation has the Gibbs state at inverse temperature β as its density operator, evolved by an ontic flow lifting the joint unitary U, obeys S(ρ_S) − S(ρ_S') ≤ β · ΔQ: the entropy removed from the system preparation is bounded by β times the heat dumped into the bath (landauer_bound with the flowed joint state supplied by barycenter_flow_prod). The full-rank hypotheses are those of landauer_bound.