The density operator of an ontic preparation, and the QIT layer applied to it

Category: 3-Local (the spine from a preparation on Σ to the quantum-information layer; W2 of specs/qit-chain-scoping.md).

Two theorems of LF2 compose to "a preparation on Σ determines a density operator": OperationalPackage.fromPreparation (LF2/Preparation.lean) turns a preparation measure μprep on Σ into an operational package, and effect_gleason_representation (LF2/EffectGleason.lean) turns any operational package into the unique density operator whose trace form is its effect probabilities. Until 2026-09-11 the composition was never stated, its density operator was consumed by no theorem of Mathlib/QuantumInfo/, and every entropy, distance and data-processing theorem there was a statement about a bare matrix nothing CSD-side ever supplied. This module composes them and applies the layer.

• preparationDensity — the density operator of a preparation, (fromPreparation …).qdensity;
• ★★ preparation_traceForm / preparation_qdensity_unique — the composition: the effect probabilities of a preparation are the trace form of preparationDensity, and it is the unique density operator with that property (effect_gleason_representation on fromPreparation);
• preparationDensity_posSemidef, preparationDensity_trace_one, preparationDensity_isHermitian — the instantiation lemmas, in the exact hypothesis forms the QIT layer takes;
• ★ vonNeumannEntropy_preparation_nonneg, ★ vonNeumannEntropy_preparation_le_log — the von Neumann entropy of a preparation on Σ is well-defined, non-negative, and at most log N;
• ★ channel_traceDist_preparation_le — the data-processing inequality for two preparations: no channel increases their trace distance.

Every theorem below is effect_gleason_representation plus one exact; that is the point. The spine was two proved theorems apart, and the QIT layer's hypotheses are DensityOperator's fields.

Honest scope

⚠️ What "preparation" means here. A SectorData on an abstract Σ, a MeasureBridgeData, a probability measure μprep on Σ, and a unit-norm measurable representative rep : P → ℂᴺ — the data fromPreparation takes. The sector is posited (specs/POSITS.md Posit 2); this module does not derive it. What it proves is: given the posited sector, the QIT quantities of its preparations obey the QIT theorems.

Gleason witness here, barycentre one module up. preparationDensity is characterised below by its trace form (uniquely); that it is the barycentre ∫ |ψ⟩⟨ψ| d(π_* μprep) — entrywise, and in the ρ_ep dμ_FS form under absolute continuity — is LF2/PreparationBarycenter.lean (W3, preparationDensity_eq_barycenter, preparationDensity_apply). Nothing below depends on it.

⚠️ Channels are still bare. channel_traceDist_preparation_le takes any QuantumInfo.Channel; that the channel comes from a Σ-flow is W5/W6.

References: specs/qit-chain-scoping.md (W2–W4); LF2/Preparation.lean, LF2/EffectGleason.lean; Mathlib/QuantumInfo/{Entropy,DataProcessing,TraceDistance}.lean.

The composition

noncomputable def CSD.LF2.preparationDensity {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : DensityOperator N

The density operator of a preparation on Σ: the Gleason witness of the operational package fromPreparation builds from it.

Equations

• CSD.LF2.preparationDensity D μFS bridge μprep rep hrep_unit hrep_meas = (CSD.LF2.OperationalPackage.fromPreparation D μFS bridge μprep rep hrep_unit hrep_meas).qdensity

theorem CSD.LF2.preparation_traceForm {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (E : Effect N) : (OperationalPackage.fromPreparation D μFS bridge μprep rep hrep_unit hrep_meas).p E = traceForm (preparationDensity D μFS bridge μprep rep hrep_unit hrep_meas) E

★★ The effect probabilities of a preparation are the trace form of its density operator. fromPreparation composed with p_eq_traceForm_qdensity.

theorem CSD.LF2.preparation_qdensity_unique {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : ∃! ρ : DensityOperator N, ∀ (E : Effect N), (OperationalPackage.fromPreparation D μFS bridge μprep rep hrep_unit hrep_meas).p E = traceForm ρ E

★★ Uniqueness: preparationDensity is the only density operator whose trace form is the preparation's effect probabilities — effect_gleason_representation on fromPreparation.

The instantiation lemmas, in the QIT layer's hypothesis forms

theorem CSD.LF2.preparationDensity_isHermitian {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : (preparationDensity D μFS bridge μprep rep hrep_unit hrep_meas).M.IsHermitian

theorem CSD.LF2.preparationDensity_posSemidef {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : (preparationDensity D μFS bridge μprep rep hrep_unit hrep_meas).M.PosSemidef

theorem CSD.LF2.preparationDensity_trace_one {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : (preparationDensity D μFS bridge μprep rep hrep_unit hrep_meas).M.trace = 1

The QIT layer applied to a preparation

noncomputable def CSD.LF2.preparationEntropy {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : ℝ

The von Neumann entropy of a preparation on Σ.

Equations

• CSD.LF2.preparationEntropy D μFS bridge μprep rep hrep_unit hrep_meas = QuantumInfo.vonNeumannEntropy ⋯

theorem CSD.LF2.vonNeumannEntropy_preparation_nonneg {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : 0 ≤ preparationEntropy D μFS bridge μprep rep hrep_unit hrep_meas

★ The entropy of a preparation is non-negative (vonNeumannEntropy_nonneg).

theorem CSD.LF2.vonNeumannEntropy_preparation_le_log {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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) : preparationEntropy D μFS bridge μprep rep hrep_unit hrep_meas ≤ Real.log ↑N

★ The entropy of a preparation on the N-dimensional sector is at most log N (vonNeumannEntropy_le_log_card).

theorem CSD.LF2.channel_traceDist_preparation_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] {N : ℕ} (D : SectorData SigmaSpace P G) (μFS : MeasureTheory.Measure P) [MeasureTheory.IsProbabilityMeasure μFS] (bridge : MeasureBridgeData D μFS) (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (hrep_meas : Measurable rep) {m : Type u_4} {ι : Type u_5} [Fintype m] [Fintype ι] [DecidableEq m] (Φ : QuantumInfo.Channel (Fin N) m ι) (μprep' : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep'] : QuantumInfo.traceDist ⋯ ≤ QuantumInfo.traceDist ⋯

★ Data processing for two preparations on Σ: for any channel Φ, the trace distance of the channel outputs is at most the trace distance of the preparations' density operators (channel_traceDist_le).