The barycentre: the density operator of a preparation is `∫ |ψ⟩⟨ψ| d(π_* μprep)` #

Category: 3-Local (W3 of specs/qit-chain-scoping.md; the ontic identification of the density operator W2 obtained as a Gleason witness).

W2 (LF2/PreparationQdensity.lean) gave every preparation on Σ a density operator preparationDensity, characterised uniquely by its trace form — effect_gleason_representation on fromPreparation. That characterisation says what the operator does, not what it is. This module says what it is: the barycentre of the rank-one projectors |rep ψ⟩⟨rep ψ| along the projective law π_* μprep, an entrywise Bochner integral. So the density operator of a preparation is the ontic average of pure-state projectors over the preparation's projective distribution — the object Papers C and TN2 write as ∫ |ψ⟩⟨ψ| ρ_ep(ψ) dμ_FS(ψ).

entryFn, barycenterMatrix — the entry functions ψ ↦ ψⱼ conj ψₖ and their integrals;
barycenterMatrix_isHermitian, barycenterMatrix_trace, barycenterMatrix_posSemidef — the barycentre against a probability measure is Hermitian, has trace one (∑ⱼ |ψⱼ|² = ‖ψ‖² = 1 under the integral), and is positive semidefinite (its quadratic form at u is ∫ |⟨u, ψ⟩|², dotProduct_barycenterMatrix_mulVec);
barycenterDensity — the barycentre packaged as a DensityOperator, and barycenterDensity_traceForm — its trace form against an effect is the integral of the effect function (trace_barycenterMatrix_mul: the trace of B · E is the integral of tr(|ψ⟩⟨ψ| E), which effectProjFn_eq_sum expands entrywise);
preparationBarycenter — the barycentre of a preparation on Σ, along π_* μprep;
★★ preparationDensity_eq_barycenter — the identification: preparationDensity (the Gleason witness) equals preparationBarycenter, by the uniqueness half of effect_gleason_representation;
★★ preparationDensity_apply — entrywise: ρ_{jk} = ∫ ψⱼ conj ψₖ d(π_* μprep)(ψ);
★ preparationDensity_apply_rnDeriv — the ρ_ep form: when π_* μprep ≪ μFS, with ρ_ep its Radon–Nikodym derivative, ρ_{jk} = ∫ ρ_ep(ψ) ψⱼ conj ψₖ dμFS(ψ).

Honest scope #

The ρ_ep form takes absolute continuity as a hypothesis here, in the abstract SectorData interface. For region preparations of the SigmaLayer interface it is a theorem (projectivePreparationLaw_absolutelyContinuous), and SigmaLayer/PreparationDensityBridge.lean composes the two: preparationDensity_apply_rhoEp is this formula with Q28's Radon–Nikodym density and no hypothesis, and kahler_preparationDensity_apply is its instance on the Kähler arena with c = 1. The barycentre identification itself (preparationDensity_eq_barycenter) needs no such hypothesis.

⚠️ Same posits as W2. The sector is posited (specs/POSITS.md Posit 2); what is proved is that, given it, the density operator of a preparation is the barycentre.

References: specs/qit-chain-scoping.md (W3); LF2/PreparationQdensity.lean (W2); LF2/EffectGleason.lean (effect_gleason_representation, trace_mul_outerProduct); LF2/Preparation.lean (fromPreparation, effectProjFn_integrable).

The barycentre: the density operator of a preparation is ∫ |ψ⟩⟨ψ| d(π_* μprep) #

Honest scope #

The barycentre of rank-one projectors, over any finite index #

The barycentre is a density operator #

The Fin N case: trace form against effects, and the DensityOperator N packaging #

The identification: the density operator of a preparation IS its barycentre #

The barycentre: the density operator of a preparation is `∫ |ψ⟩⟨ψ| d(π_* μprep)` #

The `Fin N` case: trace form against effects, and the `DensityOperator N` packaging #