E1: the Fubini–Study second moment of the reduced state

Category: conceptually 1-Mathlib (CSD-free quantum statistical mechanics), kept under CSD.Thermo beside TH-1.

The equilibration arc's first item (specs/equilibration-arc-plan.md E1) — in the Q24 scoping note's vocabulary, its gated bricks B4/B5. TH-1 proved the first moment (the mean reduced state is I_A/d_A); Q24 proved the Fubini–Study second moments of the moment map by twirl algebra. This module spends both on the reduced state itself.

⚠️ H-TENSOR — the bipartition is a hypothesis, never an inference

Every statement carries the bipartition as an explicit argument

e : Fin N ≃ Fin dA × Fin dB

exactly as canonical_typicality_expectation does. It is deliberately not obtained from a tensor-product API (QuantumInfo.regTensorEquiv would make that easy, and is the temptation this note exists to block). Rationale: a silently-chosen factorisation is a structural posit doing load-bearing work — a second D1. Which factorisation is meant is physics input, so it belongs in the signature where a reader and a referee can see it. (TODO(author): confirm the intended D4/G6 referent — in this repo those IDs name an audit record and a root-repair item, so they are presumably paper-side.)

What is proved

With x_i = momentMap p i and r_{ij} = rayDensity p i j:

• blockPop — the subsystem populations (ρ_A)_{aa} = Σ_b x_{e⁻¹(a,b)}, a linear statistic in the moment map, so Q24's linear moments apply verbatim (blockPop_eq_linear);
• ★ fs_blockPop_mean — E[(ρ_A)_{aa}] = d_B/N (= 1/d_A), the first moment in moment-map form;
• ★ fs_blockPop_sq — E[(ρ_A)_{aa}²] = (d_B² + d_B)/(N(N+1));
• signFlip_smul_rayDensity_ne — a sign flip leaves a density entry alone when it touches neither index (companion to signFlip_smul_offdiag);
• ★ fs_redOff_cross_vanish — the genuinely four-index expectations vanish: a coordinate occurring an odd number of times is killed by the sign flip. This is the novel ingredient; everything else here is Q24 specialised;
• ★★ fs_redOff_normSq — E|(ρ_A)_{aa'}|² = d_B/(N(N+1)) for a ≠ a': expanding the modulus of the sum, the b = b' terms are the landed cross moment and the b ≠ b' terms vanish.

And then the assembly those moments were for:

• reducedMatrix / hsDeviation / hsDeviationNormSq — the reduced state as a matrix, its deviation ρ_A − I_A/d_A, and the entrywise Hilbert–Schmidt norm squared of that deviation;
• ★ fs_hsDeviation_diag_sq and ★ fs_hsDeviation_off_sq — the two kinds of entry;
• ★★ fs_hsDeviationNormSq — the Lubkin–Page purity average E‖ρ_A − I_A/d_A‖₂² = (d_A + d_B)/(N + 1) − 1/d_A. The cardinality identity N = d_A d_B it needs is read off the bipartition itself (card_eq_mul_of_tensorEquiv), not assumed;
• ★ fs_hsDeviation_typicality — Markov on that second moment, i.e. the statement in the form "a Fubini–Study-typical ray has a near-maximally-mixed subsystem".

⚠️ Honest scope — what is NOT proved here

• The trace-norm form the brief asks for would follow by ‖·‖₁ ≤ √d_A ‖·‖₂, which needs the matrix-norm API rather than these moment computations.
• The reduced state is written entrywise in the ray-density vocabulary, which is what makes Q24's twirl results apply directly. Identifying these entries with Matrix.traceRight of the projector (the canonical_typicality_expectation spelling) is index bookkeeping, not done here — so hsDeviationNormSq is defined as the sum of squared moduli of the entries of ρ_A − I_A/d_A rather than derived from a Matrix norm instance.
• The concentration here is Markov on a quadratic functional, which is weaker than fs_chebyshev_concentration. Chebyshev does apply, but to the linear statistics: each individual population blockPop e · a is one of Q24's ∑ λₖ xₖ and gets the O(1/N) rate. Exponential (Lévy) rates remain out of reach — see MATHLIB-GAPS.md.

The reduced state's entries, in moment-map / ray-density vocabulary

noncomputable def CSD.Thermo.blockIndicator {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) (k : Fin N) : ℝ

The block indicator: 1 on the wires of subsystem level a.

Equations

• CSD.Thermo.blockIndicator e a k = if (e k).1 = a then 1 else 0

noncomputable def CSD.Thermo.blockPop {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a : Fin dA) : ℝ

The subsystem population (ρ_A)_{aa}: the total moment-map weight of the a-block.

Equations

• CSD.Thermo.blockPop e p a = ∑ b : Fin dB, CSD.LF4.momentMap p (e.symm (a, b))

noncomputable def CSD.Thermo.redOff {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a a' : Fin dA) : ℂ

The off-diagonal entry (ρ_A)_{aa'} of the reduced state.

Equations

• CSD.Thermo.redOff e p a a' = ∑ b : Fin dB, CSD.Thermo.rayDensity p (e.symm (a, b)) (e.symm (a', b))

theorem CSD.Thermo.blockPop_eq_linear {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a : Fin dA) : blockPop e p a = ∑ k : Fin N, blockIndicator e a k * LF4.momentMap p k

The population is the linear statistic of the block indicator — the bridge that lets Q24's linear moment theorems apply unchanged.

The block indicator's own sums

theorem CSD.Thermo.sum_blockIndicator {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : ∑ k : Fin N, blockIndicator e a k = ↑dB

theorem CSD.Thermo.sum_blockIndicator_sq {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : ∑ k : Fin N, blockIndicator e a k ^ 2 = ↑dB

★ The population's first and second moments (Q24's linear moments, specialised)

theorem CSD.Thermo.fs_blockPop_mean {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e p a ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ↑dB / ↑N

★ The mean subsystem population is d_B/N (that is, 1/d_A) — the first moment.

theorem CSD.Thermo.fs_blockPop_sq {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e p a ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = (↑dB ^ 2 + ↑dB) / (↑N * (↑N + 1))

★ The population's second moment: (d_B² + d_B)/(N(N+1)).

The sign flip away from both indices

theorem CSD.Thermo.signFlip_smul_rayDensity_ne {N : ℕ} [NeZero N] (k i j : Fin N) (hik : i ≠ k) (hjk : j ≠ k) (p : LF4.CPN N) : rayDensity (signFlip k • p) i j = rayDensity p i j

A sign flip that touches neither index leaves the density entry alone. The companion of signFlip_smul_offdiag (which handles the case where the flipped coordinate is one of the indices), and the engine behind the four-index vanishing below.

★★ The off-diagonal second moment

theorem CSD.Thermo.fs_redOff_cross_vanish {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) {a a' : Fin dA} (haa : a ≠ a') {b b' : Fin dB} (hbb : b ≠ b') : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (rayDensity p (e.symm (a, b)) (e.symm (a', b))).re * (rayDensity p (e.symm (a, b')) (e.symm (a', b'))).re + (rayDensity p (e.symm (a, b)) (e.symm (a', b))).im * (rayDensity p (e.symm (a, b')) (e.symm (a', b'))).im ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 0

★ The four-index expectations vanish. For a ≠ a' and b ≠ b', the coordinate e⁻¹(a,b) occurs an odd number of times in the product, so the sign flip there negates the integrand and the integral is its own negative.

★★ The off-diagonal second moment

noncomputable def CSD.Thermo.redTerm {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a a' : Fin dA) (b : Fin dB) (p : LF4.CPN N) : ℂ

The b-th summand of an off-diagonal reduced entry, named so the expansion below stays readable.

Equations

• CSD.Thermo.redTerm e a a' b p = CSD.Thermo.rayDensity p (e.symm (a, b)) (e.symm (a', b))

theorem CSD.Thermo.redOff_eq_sum {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a a' : Fin dA) : redOff e p a a' = ∑ b : Fin dB, redTerm e a a' b p

theorem CSD.Thermo.redTerm_self {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a a' : Fin dA) (b : Fin dB) (p : LF4.CPN N) : (redTerm e a a' b p).re * (redTerm e a a' b p).re + (redTerm e a a' b p).im * (redTerm e a a' b p).im = LF4.momentMap p (e.symm (a, b)) * LF4.momentMap p (e.symm (a', b))

The b = b' term of the expansion is a product of two moment-map coordinates.

theorem CSD.Thermo.redTerm_measurable {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a a' : Fin dA) (b : Fin dB) : Measurable (redTerm e a a' b)

theorem CSD.Thermo.fs_redOff_normSq {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) {a a' : Fin dA} (haa : a ≠ a') : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), Complex.normSq (redOff e p a a') ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ↑dB / (↑N * (↑N + 1))

★★ The off-diagonal entries' second moment: E|(ρ_A)_{aa'}|² = d_B/(N(N+1)) for a ≠ a'. The b = b' terms contribute the landed cross moment E[x_i x_j]; the b ≠ b' terms vanish by fs_redOff_cross_vanish.

The reduced state as a matrix, and its deviation from maximal mixing

noncomputable def CSD.Thermo.reducedMatrix {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) : Matrix (Fin dA) (Fin dA) ℂ

The reduced density matrix of a ray, entrywise in the ray-density vocabulary: (ρ_A)_{aa'} = Σ_b r_{(a,b),(a',b)}. (Still entrywise — identifying this with Matrix.traceRight of the projector is the bookkeeping the header declares out of scope.)

Equations

• CSD.Thermo.reducedMatrix e p = Matrix.of fun (a a' : Fin dA) => CSD.Thermo.redOff e p a a'

@[simp]

theorem CSD.Thermo.reducedMatrix_apply {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a a' : Fin dA) : reducedMatrix e p a a' = redOff e p a a'

theorem CSD.Thermo.redOff_diag {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a : Fin dA) : redOff e p a a = ↑(blockPop e p a)

The diagonal of the reduced matrix is the subsystem population — the bridge between the two vocabularies of this file (rayDensity_diag under the b-sum).

noncomputable def CSD.Thermo.hsDeviation {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) : Matrix (Fin dA) (Fin dA) ℂ

The deviation from the maximally mixed state, ρ_A − I_A/d_A.

Equations

• CSD.Thermo.hsDeviation e p = CSD.Thermo.reducedMatrix e p - (↑dA)⁻¹ • 1

theorem CSD.Thermo.hsDeviation_diag {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a : Fin dA) : hsDeviation e p a a = ↑(blockPop e p a - (↑dA)⁻¹)

On the diagonal the deviation is real: the population minus 1/d_A.

theorem CSD.Thermo.hsDeviation_off {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) {a a' : Fin dA} (haa : a ≠ a') : hsDeviation e p a a' = redOff e p a a'

Off the diagonal, subtracting a multiple of the identity changes nothing.

noncomputable def CSD.Thermo.hsDeviationNormSq {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) : ℝ

The Hilbert–Schmidt norm squared of the deviation, ‖ρ_A − I_A/d_A‖₂², written entrywise as the sum of squared moduli of the entries.

Equations

• CSD.Thermo.hsDeviationNormSq e p = ∑ a : Fin dA, ∑ a' : Fin dA, Complex.normSq (CSD.Thermo.hsDeviation e p a a')

Analytic plumbing for the population

theorem CSD.Thermo.blockPop_measurable {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : Measurable fun (p : LF4.CPN N) => blockPop e p a

theorem CSD.Thermo.blockPop_nonneg {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a : Fin dA) : 0 ≤ blockPop e p a

theorem CSD.Thermo.blockPop_le_one {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a : Fin dA) : blockPop e p a ≤ 1

A subsystem population is at most one: it is a sub-sum of the moment map's simplex sum.

theorem CSD.Thermo.abs_blockPop_le_one {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a : Fin dA) : |blockPop e p a| ≤ 1

theorem CSD.Thermo.blockPop_integrable {N dA dB : ℕ} (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : MeasureTheory.Integrable (fun (p : LF4.CPN N) => blockPop e p a) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

theorem CSD.Thermo.blockPop_sq_integrable {N dA dB : ℕ} (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : MeasureTheory.Integrable (fun (p : LF4.CPN N) => blockPop e p a ^ 2) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

theorem CSD.Thermo.card_eq_mul_of_tensorEquiv {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) : N = dA * dB

The bipartition's cardinality identity, read off the equivalence itself: N = d_A · d_B. Part of H-TENSOR's point — the factorisation is carried by e, so its arithmetic is too.

★ The diagonal contribution

theorem CSD.Thermo.fs_hsDeviation_diag_sq {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), Complex.normSq (hsDeviation e p a a) ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = (↑dB ^ 2 + ↑dB) / (↑N * (↑N + 1)) - (↑dA)⁻¹ ^ 2

★ The diagonal deviation's second moment: E[((ρ_A)_{aa} − 1/d_A)²] = (d_B² + d_B)/(N(N+1)) − 1/d_A².

The mean population is exactly 1/d_A (that is what d_B/N = 1/d_A says once N = d_A d_B is read off the bipartition), so the cross term collapses against the constant and only one subtraction survives.

★ The off-diagonal contribution, and entrywise integrability

theorem CSD.Thermo.redOff_measurable {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a a' : Fin dA) : Measurable fun (p : LF4.CPN N) => redOff e p a a'

theorem CSD.Thermo.norm_redOff_le {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a a' : Fin dA) : ‖redOff e p a a'‖ ≤ ↑dB

theorem CSD.Thermo.normSq_redOff_measurable {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a a' : Fin dA) : Measurable fun (p : LF4.CPN N) => Complex.normSq (redOff e p a a')

theorem CSD.Thermo.normSq_hsDeviation_integrable {N dA dB : ℕ} (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a a' : Fin dA) : MeasureTheory.Integrable (fun (p : LF4.CPN N) => Complex.normSq (hsDeviation e p a a')) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

Every entry of the deviation is square-integrable against Fubini–Study. Proved by cases: the diagonal is the (bounded) population deviation, the off-diagonal a sum of d_B density entries each of modulus at most one.

theorem CSD.Thermo.fs_hsDeviation_off_sq {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) {a a' : Fin dA} (haa : a ≠ a') : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), Complex.normSq (hsDeviation e p a a') ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ↑dB / (↑N * (↑N + 1))

★ The off-diagonal contribution: E|(ρ_A)_{aa'}|² = d_B/(N(N+1)) for a ≠ a' — subtracting I_A/d_A leaves these entries untouched, so this is fs_redOff_normSq.

★★ The Hilbert–Schmidt assembly

theorem CSD.Thermo.fs_hsDeviationNormSq {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), hsDeviationNormSq e p ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = (↑dA + ↑dB) / (↑N + 1) - (↑dA)⁻¹

★★ The Lubkin–Page purity average, in Hilbert–Schmidt form:

E‖ρ_A − I_A/d_A‖₂² = (d_A + d_B)/(N + 1) − 1/d_A

(equivalently E[Tr ρ_A²] = (d_A + d_B)/(N + 1), since ‖ρ_A − I_A/d_A‖₂² = Tr ρ_A² − 1/d_A for any trace-one ρ_A).

Every ingredient is one of the moments above: the d_A diagonal entries each contribute fs_hsDeviation_diag_sq, the d_A(d_A − 1) off-diagonal entries each contribute fs_hsDeviation_off_sq, and N = d_A d_B — read off the bipartition e itself by card_eq_mul_of_tensorEquiv — collapses the result.

For a large environment (d_B ≫ d_A) the right-hand side is ≈ d_B/(N+1) ≈ 1/d_A, so the deviation's mean square is second order: a Fubini–Study-typical global ray has a subsystem state close to maximally mixed. Combined with fs_chebyshev_concentration this is canonical typicality at Chebyshev grade.

★ The typicality statement (Markov)

theorem CSD.Thermo.hsDeviationNormSq_nonneg {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) : 0 ≤ hsDeviationNormSq e p

theorem CSD.Thermo.hsDeviationNormSq_integrable {N dA dB : ℕ} (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) : MeasureTheory.Integrable (fun (p : LF4.CPN N) => hsDeviationNormSq e p) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

theorem CSD.Thermo.normSq_hsDeviation_measurable {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (a a' : Fin dA) : Measurable fun (p : LF4.CPN N) => Complex.normSq (hsDeviation e p a a')

theorem CSD.Thermo.hsDeviationNormSq_measurable {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) : Measurable fun (p : LF4.CPN N) => hsDeviationNormSq e p

theorem CSD.Thermo.normSq_hsDeviation_le {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) (a a' : Fin dA) : Complex.normSq (hsDeviation e p a a') ≤ 1 + ↑dB ^ 2

A crude but uniform entry bound, enough to make the functional a bounded observable.

theorem CSD.Thermo.hsDeviationNormSq_le {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (p : LF4.CPN N) : hsDeviationNormSq e p ≤ ↑dA ^ 2 * (1 + ↑dB ^ 2)

The Hilbert–Schmidt functional is a bounded observable — what lets the equilibration engine (MeasureTheory.HasCorrelationDecay) accept it.

theorem CSD.Thermo.fs_hsDeviation_typicality {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) {ε : ℝ} (hε : 0 < ε) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀).real {p : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) | ε ≤ hsDeviationNormSq e p} ≤ ((↑dA + ↑dB) / (↑N + 1) - (↑dA)⁻¹) / ε

★ Canonical typicality, in usable form. Markov's inequality on the second moment: the Fubini–Study probability that a ray's subsystem state sits Hilbert–Schmidt-far from maximally mixed is at most ((d_A+d_B)/(N+1) − 1/d_A)/ε.

Note this is Markov on a quadratic functional, not fs_chebyshev_concentration — the latter applies to the linear moment-map statistics (each individual population blockPop is one of those, and does get the Chebyshev rate).