E4: equilibration of time-averaged reduced states, as a conditional theorem

The equilibration arc's fourth item (specs/equilibration-arc-plan.md E4). It spends the generic engine CsdLean4/Mathlib/Dynamics/CorrelationDecay.lean on the observables E1 built.

⚠️ This is a conditional, and the antecedent is the whole content

Both theorems below have the shape

if the flow preserves μ_FS, and its correlations for this observable decay with a summable envelope, then the time averages converge to the Fubini–Study average.

Neither hypothesis is proved, exhibited, or claimed to hold for any Σ. Nothing in the corpus proves that any dynamics mixes, and nothing here changes that. What E4 buys is a reformulation: equilibration stops being a dephasing story and becomes an ergodic-theoretic statement whose one hypothesis is explicit, quantitative, and checkable in principle. Producing an actual witness for the antecedent is E5's separate job, and until that exists these theorems are conditionals with an unpopulated antecedent — which is exactly why the hypothesis is named in the signature rather than folded into a definition.

What is proved

• ★★ blockPop_timeAverage_tendsto — time-averaged subsystem populations converge in L² to d_B/N (= 1/d_A, the maximally-mixed value, by fs_blockPop_mean);
• ★★ hsDeviationNormSq_timeAverage_tendsto — the time-averaged Hilbert–Schmidt deviation ‖ρ_A − I_A/d_A‖₂² converges in L² to the Lubkin–Page value (d_A+d_B)/(N+1) − 1/d_A that E1 computed (fs_hsDeviationNormSq). This is E4 composed with E1.

⚠️ And the antecedent is empty for unitary Σ-dynamics (E5/E6)

• ★★ not_hasCorrelationDecay_blockPop_of_unitary — for d_A ≥ 2 and any unitary U, the antecedent is false along p ↦ U • p, for every summable envelope. A unitary generates a relatively compact group, so its correlations are almost periodic and cannot decay.
• ★ not_hasCorrelationDecay_blockPop_of_periodic — the same for any periodic Φ, unitary or not.

So the conditionals above are sound machinery whose hypothesis finite-dimensional unitary dynamics cannot meet. Read that as a limitation, not a refutation: equilibration in this setting rests on the typicality results (E1/E2), not on mixing. The engine itself is not vacuous — CsdLean4/Mathlib/Dynamics/CorrelationDecayWitness.lean exhibits a genuine witness (the doubling map on the circle), which is precisely a non-atomic, non-unitary system.

⚠️ Honest scope

• Discrete time. Φ is a single map and Φ^[t] its iterates; a continuous Σ-flow enters by sampling at a fixed timestep. The continuous-time statement is not proved — so a continuous unitary Σ-flow is covered only through its time-τ samples, which is what E6 rules out.
• L² convergence, from a second-moment bound. Almost-everywhere convergence is what pointwise Birkhoff would give and is not available (MATHLIB-GAPS.md).
• The flow is a hypothesis, not a construction: no Σ-dynamics is built here, and in particular the D1 dynamics residue is untouched. μ_FS-preservation is likewise assumed, not derived.
• H-TENSOR is inherited from E1: the bipartition travels as the explicit e in every signature.

Reference: specs/equilibration-arc-plan.md (E4, and E5 for the non-vacuity requirement); MATHLIB-GAPS.md; specs/future-work.md.

theorem CSD.Thermo.blockPop_timeAverage_tendsto {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) {Φ : LF4.CPN N → LF4.CPN N} {ε : ℕ → ℝ} (hΦ : MeasureTheory.MeasurePreserving Φ (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)) (hlag : ∀ (u : ℕ), |∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e p a * blockPop e (Φ^[u] p) a ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ - (∫ (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e q a ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ^ 2| ≤ ε u) (hsum : Summable ε) : Filter.Tendsto (fun (T : ℕ) => ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (birkhoffAverage ℝ Φ (fun (q : LF4.CPN N) => blockPop e q a) T p - ↑dB / ↑N) ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀) Filter.atTop (nhds 0)

★★ Time-averaged subsystem populations equilibrate — conditionally.

If Φ preserves the Fubini–Study measure and the population's correlations decay with a summable envelope ε, then the Birkhoff averages of (ρ_A)_{aa} converge in L² to d_B/N, which fs_blockPop_mean identifies as the maximally-mixed value 1/d_A.

The correlation hypothesis is stated at one lag, which is the form a physical estimate produces; HasCorrelationDecay.of_measurePreserving turns it into the two-index form the engine consumes.

theorem CSD.Thermo.hsDeviationNormSq_timeAverage_tendsto {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) {Φ : LF4.CPN N → LF4.CPN N} {ε : ℕ → ℝ} (hΦ : MeasureTheory.MeasurePreserving Φ (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)) (hlag : ∀ (u : ℕ), |∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), hsDeviationNormSq e p * hsDeviationNormSq e (Φ^[u] p) ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ - (∫ (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), hsDeviationNormSq e q ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ^ 2| ≤ ε u) (hsum : Summable ε) : Filter.Tendsto (fun (T : ℕ) => ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (birkhoffAverage ℝ Φ (fun (q : LF4.CPN N) => hsDeviationNormSq e q) T p - ((↑dA + ↑dB) / (↑N + 1) - (↑dA)⁻¹)) ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀) Filter.atTop (nhds 0)

★★ E4 composed with E1. Under the same two hypotheses, the time-averaged Hilbert–Schmidt deviation of the reduced state from maximally mixed converges in L² to the Lubkin–Page value (d_A + d_B)/(N + 1) − 1/d_A proved in fs_hsDeviationNormSq.

For a large environment that value is O(1/d_A · d_A/d_B)-small, so the conditional reads: a μ_FS-preserving flow with decaying correlations spends almost all of its time with the subsystem near maximally mixed. Again — conditional; see the header.

⚠️ E5's sharpness check: when the antecedent is empty

theorem CSD.Thermo.blockPop_variance_ne {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) (hdA : 2 ≤ dA) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e p a * blockPop e p a ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ ≠ (∫ (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e q a ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ^ 2

The Q24 arithmetic both no-goes run on: for a nontrivial subsystem the population's second moment does not equal the square of its mean. fs_blockPop_sq and fs_blockPop_mean give (d_B²+d_B)/(N(N+1)) and d_B/N, and those agree exactly when N = d_B, i.e. d_A = 1.

theorem CSD.Thermo.not_hasCorrelationDecay_blockPop_of_periodic {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) (hdA : 2 ≤ dA) {Φ : LF4.CPN N → LF4.CPN N} {ε : ℕ → ℝ} {k : ℕ} (hk : 0 < k) (hper : Φ^[k] = id) (hsum : Summable ε) : ¬MeasureTheory.HasCorrelationDecay (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) Φ (fun (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => blockPop e q a) ε

⚠️ No periodic flow satisfies E4's antecedent for a nontrivial subsystem.

If Φ^[k] = id and d_A ≥ 2, then HasCorrelationDecay for the population observable is false for every summable envelope. So blockPop_timeAverage_tendsto, applied to a periodic Σ-flow, is a conditional whose antecedent cannot be met.

The proof is Q24 arithmetic against the periodic no-go. A periodic map forces ⟨x²⟩ = ⟨x⟩² (HasCorrelationDecay.integral_mul_self_eq_of_periodic), whereas fs_blockPop_sq and fs_blockPop_mean give ⟨x²⟩ = (d_B²+d_B)/(N(N+1)) and ⟨x⟩ = d_B/N. Those agree exactly when N = d_B, i.e. when d_A = 1 — no subsystem at all.

Superseded in strength by not_hasCorrelationDecay_blockPop_of_unitary (E6, below), which drops the periodicity hypothesis entirely: no unitary flow satisfies the antecedent. This periodic version is kept because it applies to any periodic Φ, not only to unitary ones.

★★ Q12-d route 2: the finite-horizon statement, which E6 does not reach

theorem CSD.Thermo.blockPop_timeAverage_le_of_finiteHorizon {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) {Φ : LF4.CPN N → LF4.CPN N} {ε : ℕ → ℝ} {T : ℕ} (hΦ : MeasureTheory.MeasurePreserving Φ (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)) (hdec : MeasureTheory.HasCorrelationDecayUpTo (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) Φ (fun (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => blockPop e q a) ε T) (hT : 0 < T) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (birkhoffAverage ℝ Φ (fun (q : LF4.CPN N) => blockPop e q a) T p - ↑dB / ↑N) ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ ≤ 2 * (↑T)⁻¹ * ∑ u ∈ Finset.range T, ε u

★★ Equilibration at a finite horizon — and this one a unitary Σ-flow can have.

If the population's correlations are within ε on lags below T, the time average at horizon T sits within (2/T) Σ_{u<T} ε u of the maximally-mixed value. No summability, no limit.

Why this matters. not_hasCorrelationDecay_blockPop_of_unitary (E6) shows no unitary flow can satisfy the asymptotic antecedent: its powers recur, so the correlations recur. That argument needs the bound at arbitrarily large lags and says nothing over a bounded window. A unitary flow on a large space can decorrelate for a very long time before recurring — which is what a physical environment does — and this theorem is exactly the statement that survives.

So E4's conclusion is not lost for finite-dimensional unitary dynamics; what is lost is its asymptotic form. specs/q12-fibre-mechanism-scoping.md records this as Q12-d route 2, the recommended escape from W1.

⚠️ Still conditional, and the antecedent is still not exhibited. Nothing here shows any particular Σ-flow has small ε on lags below T; that is a quantitative estimate about a specific dynamics, and it remains open. What has changed is that the hypothesis is no longer provably unsatisfiable — which is what E6 established for the asymptotic version.

E6: the analytic bridge to the general unitary no-go

The three lemmas below are generic (no CSD content) and are extraction candidates for Mathlib/QuantumInfo/; they live here to keep the rebuild surface small while E6 is in progress.

theorem CSD.Thermo.toEuclideanLin_comp {N : ℕ} (A B : Matrix (Fin N) (Fin N) ℂ) (v : EuclideanSpace ℂ (Fin N)) : (Matrix.toEuclideanLin A) ((Matrix.toEuclideanLin B) v) = (Matrix.toEuclideanLin (A * B)) v

theorem CSD.Thermo.norm_toEuclideanLin_unitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin ↑U) v‖ = ‖v‖

A unitary matrix acts as an isometry. The general statement behind the per-gate signFlip_normSq / perm_normSq / hadamard_normSq of CanonicalTypicality.

theorem CSD.Thermo.continuous_unitaryEntry {N : ℕ} (k j : Fin N) : Continuous fun (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) => ↑V k j

noncomputable def CSD.Thermo.matDev {N : ℕ} (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : ℝ

The deviation of a unitary from the identity, measured entrywise in ℓ¹.

ℓ¹ rather than ℓ² deliberately: it makes the uniform estimate below a triangle inequality plus coord_norm_le, with no Cauchy–Schwarz and no square roots anywhere.

Equations

• CSD.Thermo.matDev V = ∑ k : Fin N, ∑ j : Fin N, ‖↑V k j - 1 k j‖

theorem CSD.Thermo.matDev_nonneg {N : ℕ} (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : 0 ≤ matDev V

theorem CSD.Thermo.continuous_matDev {N : ℕ} : Continuous matDev

@[simp]

theorem CSD.Thermo.matDev_one {N : ℕ} : matDev 1 = 0

theorem CSD.Thermo.toEuclideanLin_entry {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (v : EuclideanSpace ℂ (Fin N)) (k : Fin N) : ((Matrix.toEuclideanLin A) v).ofLp k = ∑ j : Fin N, A k j * v.ofLp j

theorem CSD.Thermo.norm_sub_coord_le {N : ℕ} (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (v : EuclideanSpace ℂ (Fin N)) (k : Fin N) : ‖((Matrix.toEuclideanLin ↑V) v).ofLp k - v.ofLp k‖ ≤ (∑ j : Fin N, ‖↑V k j - 1 k j‖) * ‖v‖

One coordinate of (V - 1)ψ, bounded by the ℓ¹ deviation of that row times ‖ψ‖. Triangle inequality plus coord_norm_le — this is where the ℓ¹ choice pays off.

theorem CSD.Thermo.abs_momentMap_smul_sub_le {N : ℕ} [NeZero N] (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : LF4.CPN N) (k : Fin N) : |LF4.momentMap (V • p) k - LF4.momentMap p k| ≤ 2 * ∑ j : Fin N, ‖↑V k j - 1 k j‖

The uniform estimate, one coordinate. The moment map moves by at most twice the ℓ¹ deviation of the acting unitary's row — uniformly in the state, which is what replaces the unavailable dominated-convergence argument.

theorem CSD.Thermo.blockPop_eq_sum {N dA dB : ℕ} (e : Fin N ≃ Fin dA × Fin dB) (q : LF4.CPN N) (a : Fin dA) : blockPop e q a = ∑ b : Fin dB, LF4.momentMap q (e.symm (a, b))

theorem CSD.Thermo.abs_blockPop_smul_sub_le {N dA dB : ℕ} [NeZero N] (e : Fin N ≃ Fin dA × Fin dB) (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : LF4.CPN N) (a : Fin dA) : |blockPop e (V • p) a - blockPop e p a| ≤ 2 * matDev V

★ The uniform estimate for the population observable: it moves by at most 2 · matDev V, uniformly in the state. Summing the coordinate estimate over the a-block and discarding the other blocks (all terms nonnegative) turns the row sums into the full matDev.

theorem CSD.Thermo.abs_corr_smul_sub_le {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : |∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e p a * blockPop e (V • p) a ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ - ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), blockPop e p a * blockPop e p a ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀| ≤ 2 * matDev V

★ The correlation moves by at most 2 · matDev V. The uniform estimate integrates directly — no dominated convergence, which is what FirstCountableTopology's absence rules out.

theorem CSD.Thermo.smul_iterate {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (u : ℕ) (p : LF4.CPN N) : (fun (q : LF4.CPN N) => U • q)^[u] p = U ^ u • p

theorem CSD.Thermo.not_hasCorrelationDecay_blockPop_of_unitary {N dA dB : ℕ} [NeZero N] (p₀ : LF4.CPN N) (e : Fin N ≃ Fin dA × Fin dB) (a : Fin dA) (hdA : 2 ≤ dA) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {ε : ℕ → ℝ} (hsum : Summable ε) : ¬MeasureTheory.HasCorrelationDecay (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (fun (q : LF4.CPN N) => U • q) (fun (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => blockPop e q a) ε

★★ E6, the general no-go: no unitary flow satisfies E4's antecedent for a nontrivial subsystem. For d_A ≥ 2 and any unitary U, HasCorrelationDecay for the population observable along p ↦ U • p is false for every summable envelope.

This is the almost-periodicity obstruction in full, no longer restricted to the periodic case.

Since 2026-08-24 it is a one-line consequence of the general statement, MeasureTheory.not_hasCorrelationDecay_of_compactGroup: no flow generated by a compact group has decaying correlations for an observable of nonzero variance. The recurrence argument that used to sit here has moved there, and what is left is the three inputs specific to this case — the uniform transfer abs_corr_smul_sub_le as a modulus, smul_iterate to identify iterates with powers, and Q24's arithmetic blockPop_variance_ne for the variance. The general form is what makes the same obstruction available to the Kähler fibre shift (CSD.LF4.KahlerFlow.not_hasCorrelationDecay_kFlow) without repeating any of it.

Read it as a limitation, not a refutation. E4's machinery is sound; what this says is that its antecedent is not populated by finite-dimensional unitary Σ-dynamics, so equilibration in that setting must rest on the typicality results (E1/E2) rather than on mixing.