E2: the microcanonical energy window

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

The equilibration arc's second item (specs/equilibration-arc-plan.md E2), re-scoped by E3's verdict. E2 was originally "E1 on the unit sphere of a spectral sector H_R". That formulation is refuted: Thermo/SectorRestriction.lean proves an exact spectral sector is Fubini–Study-null, so restricting to one gives the zero measure and there is nothing to condition on. The surviving route — route 1 of E3's two — is a positive-measure energy window, and this module builds it.

The setting: a diagonal Hamiltonian

For H = diag(λ) in the moment-map basis, the energy expectation of a ray is the linear statistic ⟨H⟩_p = Σ_k λ_k x_k (rayEnergy). That is exactly the shape Q24's linear moments and Chebyshev bound speak about, so the window's measure is controlled by landed results with no new integral.

What is proved

• rayEnergy, energyMean, energyVar — the energy expectation and its first two Fubini–Study moments (fs_energy_mean is fs_linear_expectation; the variance is Q24's).
• energyWindow — the microcanonical window {p : |⟨H⟩_p − ⟨H⟩| < ε} around the mean, and its measurability.
• ★★ energyWindow_ne_zero — the window has positive measure once it is wider than the fluctuation scale (ε² > Var), by Chebyshev. This is the hypothesis E3's verdict makes load-bearing, and it is quantitative: the width condition is explicit in d, λ, N, not assumed.
• microMeasure — the microcanonical law: μ_FS conditioned on the window, a probability measure exactly when the window is non-null.

⚠️ Honest scope — what conditioning does and does not preserve

Conditioning on an energy window breaks the U(N) invariance that Q24's twirl argument uses, so the moment values do not transfer. The situation is not uniform, and the split is sharp:

• the sign flips survive — momentMap_signFlip says a sign flip fixes every moment coordinate, hence fixes rayEnergy and preserves the window setwise;
• the permutations and the Hadamard rotation do not — momentMap_permU permutes the coordinates and the Hadamard mixes them, either of which changes rayEnergy unless λ is constant.

So the vanishing results (which use only sign flips) survive conditioning, while the moment values E[x_i²] = 2/(N(N+1)) etc. do not. Computing conditional moments is a genuinely different problem (a microcanonical density-of-states computation) and is not attempted here.

References

specs/equilibration-arc-plan.md (E2, and E3's verdict that forced this re-scope); Thermo/SectorRestriction.lean (the refutation of the exact-sector formulation); Thermo/CanonicalTypicality.lean (Q24's linear moments and fs_chebyshev_concentration).

The energy expectation of a ray

noncomputable def CSD.Thermo.rayEnergy {N : ℕ} (lam : Fin N → ℝ) (p : LF4.CPN N) : ℝ

The energy expectation of a ray, for a Hamiltonian diag lam in the moment-map basis: the linear statistic ⟨H⟩_p = Σ_k λ_k x_k.

Equations

• CSD.Thermo.rayEnergy lam p = ∑ k : Fin N, lam k * CSD.LF4.momentMap p k

theorem CSD.Thermo.rayEnergy_measurable {N : ℕ} (lam : Fin N → ℝ) : Measurable (rayEnergy lam)

noncomputable def CSD.Thermo.energyMean {N : ℕ} (lam : Fin N → ℝ) : ℝ

The mean energy over Fubini–Study: the equal-weight average of the spectrum.

Equations

• CSD.Thermo.energyMean lam = (∑ k : Fin N, lam k) / ↑N

noncomputable def CSD.Thermo.energyVar {N : ℕ} (lam : Fin N → ℝ) : ℝ

The Fubini–Study variance of the energy (Q24's closed form).

Equations

• CSD.Thermo.energyVar lam = (↑N * ∑ k : Fin N, lam k ^ 2 - (∑ k : Fin N, lam k) ^ 2) / (↑N ^ 2 * (↑N + 1))

theorem CSD.Thermo.fs_energy_mean {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (lam : Fin N → ℝ) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), rayEnergy lam p ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = energyMean lam

The mean energy is fs_linear_expectation, restated.

The window

def CSD.Thermo.energyWindow {N : ℕ} (lam : Fin N → ℝ) (ε : ℝ) : Set (LF4.CPN N)

The microcanonical energy window of half-width ε about the mean energy.

Equations

• CSD.Thermo.energyWindow lam ε = {p : CSD.LF4.CPN N | |CSD.Thermo.rayEnergy lam p - CSD.Thermo.energyMean lam| < ε}

theorem CSD.Thermo.measurableSet_energyWindow {N : ℕ} (lam : Fin N → ℝ) (ε : ℝ) : MeasurableSet (energyWindow lam ε)

theorem CSD.Thermo.compl_energyWindow {N : ℕ} (lam : Fin N → ℝ) (ε : ℝ) : (energyWindow lam ε)ᶜ = {p : LF4.CPN N | ε ≤ |rayEnergy lam p - energyMean lam|}

The window's complement is the Chebyshev tail event.

theorem CSD.Thermo.energyWindow_ne_zero {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (lam : Fin N → ℝ) {ε : ℝ} (hε : 0 < ε) (hwidth : ENNReal.ofReal (energyVar lam / ε ^ 2) < 1) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (energyWindow lam ε) ≠ 0

★★ The energy window has positive measure once it exceeds the fluctuation scale.

This is the hypothesis E3's verdict makes load-bearing — an exact spectral sector is Fubini–Study-null, so a microcanonical statement needs a window that provably carries weight. The condition is quantitative: the Chebyshev tail Var/ε² must be < 1, i.e. the window must be wider than the standard deviation.

noncomputable def CSD.Thermo.microMeasure {N : ℕ} (p₀ : LF4.CPN N) (lam : Fin N → ℝ) (ε : ℝ) : MeasureTheory.Measure (LF4.CPN N)

The microcanonical law: Fubini–Study conditioned on the energy window.

Equations

• CSD.Thermo.microMeasure p₀ lam ε = (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)[|CSD.Thermo.energyWindow lam ε]

theorem CSD.Thermo.microMeasure_isProbability {N : ℕ} (p₀ : LF4.CPN N) (lam : Fin N → ℝ) {ε : ℝ} (hne : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (energyWindow lam ε) ≠ 0) : MeasureTheory.IsProbabilityMeasure (microMeasure p₀ lam ε)

The microcanonical law is a probability measure exactly when the window carries weight — which energyWindow_ne_zero supplies.

★★ What survives conditioning: the sign flips

The point of this section is a sharp split. Conditioning on an energy window destroys the U(N) invariance Q24's twirl argument runs on — but not uniformly. A sign flip fixes every moment coordinate (momentMap_signFlip), hence fixes the energy, hence maps the window to itself; so the whole sign-flip half of the twirl toolkit survives conditioning intact. The permutations and the Hadamard rotation move moment coordinates and therefore change the energy, so they do not.

theorem CSD.Thermo.rayEnergy_signFlip {N : ℕ} [NeZero N] (lam : Fin N → ℝ) (k : Fin N) (p : LF4.CPN N) : rayEnergy lam (signFlip k • p) = rayEnergy lam p

The energy is invariant under a sign flip: the flip fixes every moment coordinate.

theorem CSD.Thermo.energyWindow_signFlip_preimage {N : ℕ} [NeZero N] (lam : Fin N → ℝ) (ε : ℝ) (k : Fin N) : (fun (p : LF4.CPN N) => signFlip k • p) ⁻¹' energyWindow lam ε = energyWindow lam ε

Hence the sign flip preserves the energy window.

theorem CSD.Thermo.map_signFlip_microMeasure {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (lam : Fin N → ℝ) (ε : ℝ) (k : Fin N) : MeasureTheory.Measure.map (fun (p : LF4.CPN N) => signFlip k • p) (microMeasure p₀ lam ε) = microMeasure p₀ lam ε

★ The microcanonical law is sign-flip invariant. The window is preserved and μ_FS is unitarily invariant, so conditioning commutes with the flip.

theorem CSD.Thermo.micro_integral_signFlip {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (lam : Fin N → ℝ) (ε : ℝ) (k : Fin N) {f : LF4.CPN N → ℝ} (hf : Measurable f) : ∫ (p : LF4.CPN N), f p ∂microMeasure p₀ lam ε = ∫ (p : LF4.CPN N), f (signFlip k • p) ∂microMeasure p₀ lam ε

The change-of-variables engine, conditioned: integrals against the microcanonical law are unchanged by a sign flip. The conditioned analogue of fs_integral_unitary, available for the sign flips only.

★★ The four-index vanishing survives conditioning

theorem CSD.Thermo.micro_redOff_cross_vanish {N : ℕ} [NeZero N] {dA dB : ℕ} (p₀ : LF4.CPN N) (lam : Fin N → ℝ) (ε : ℝ) (e : Fin N ≃ Fin dA × Fin dB) {a a' : Fin dA} (haa : a ≠ a') {b b' : Fin dB} (hbb : b ≠ b') : ∫ (p : LF4.CPN 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 ∂microMeasure p₀ lam ε = 0

★★ The four-index expectations vanish microcanonically too. The proof of fs_redOff_cross_vanish used only a sign flip, and sign flips preserve the energy window, so the argument transfers verbatim to the conditioned law. This is the part of E1's machinery that survives E2's conditioning — in contrast to the moment values, which do not (see the module header).