TH1: canonical typicality -- thermal equilibrium from Fubini-Study volume

Category: conceptually 1-Mathlib (CSD-free general quantum statistical mechanics on the Fubini-Study Kaehler structure); kept under CSD.Thermo as the flagship first tranche of the thermodynamics track (specs/thermo-plan.md, TH1).

Glossary: https://glossary.constraintsurfacedynamics.com/canonical-typicality/ Plain-language, CSD-role and formal statements of canonical typicality, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

What is proved (the achievable core, EXPECTATION only)

For a global pure state drawn from the Fubini-Study measure mu_FS on CP^{N-1}, the average density operator is maximally mixed, and the average reduced state of any tensor subsystem is maximally mixed on that subsystem:

• fs_first_moment: E_{mu_FS}[ |psi><psi| ] = (1/N) I on CP^{N-1}. The average pure-state density matrix over Fubini-Study is (1/N) I_N. A genuine integral computation via Fubini-Study U(N)-invariance (a "twirl" / Schur argument executed entrywise): permutation invariance forces all diagonal entries equal (each 1/N by normalisation and momentMap_sum_eq_one), and a sign-flip diagonal unitary forces every off-diagonal entry to zero.
• canonical_typicality_expectation: for H = H_S (x) H_E with N = d_S * d_E, the average reduced state E_{mu_FS}[ Tr_E |psi><psi| ] = (1/d_S) I_S. The headline: partial-tracing the Fubini-Study first moment gives the canonical (maximally mixed, equal-energy / microcanonical) state on the subsystem. This is the FS-average ANALOGUE of LF6.maxEntangled_marginal_uniform (which gives the maximally-mixed marginal for the one specific maximally-entangled state): here the maximally-mixed reduced state arises for the Fubini-Study average over all pure states. (Analogy at the mathematical level, not a formal Lean dependency: this theorem does not cite that lemma.)

Honest scope (load-bearing)

EXPECTATION + CHEBYSHEV, not exponential. This tranche proves the reduced state is canonical in expectation over mu_FS, and (Q24, 2026-08-21) that diagonal statistics of a single mu_FS-sample concentrate at the maximally-mixed value at polynomial rate Var = O(1/N) (fs_chebyshev_concentration, from the exact second moments fs_x_sq_moment / fs_x_cross_moment -- twirl algebra, no isoperimetry). The strictly stronger EXPONENTIAL typical-state (Levy) statement -- reduced state close to I_S/d_S with probability 1 - O(exp(-c d_E)) for a small subsystem in a large environment (Popescu-Short-Winter / Goldstein-Lebowitz- Tumulka-Zanghi) -- is the named residual (see the Concentration residual section below). It is NOT proved here: it needs measure concentration on high-dimensional spheres (Levy's lemma: Lipschitz + isoperimetry), which Mathlib does not carry. No sorry, no axiom is used to paper over this.

NOT dynamical thermalisation. This is a typicality (volume-average) statement, not a proof that a given initial state thermalises under a dynamics (that needs mixing / ETH, out of scope).

CSD reading. Born-from-volume (the moment-map / Duistermaat-Heckman cluster, fs_born_volume_ratio_N, Gleason-free) becomes thermal-equilibrium-from-volume: the canonical subsystem state is the Fubini-Study volume-average. The CSD-distinctive claim that this equilibrium emerges from deterministic microdynamics rests on the SO-1 (sector / typicality-law posit) and D1 (dynamics) residues shared with all of LF4/LF6; this file posits mu_FS as the sampling law (SO-1) and proves the statistical-mechanical consequence, it does not derive mu_FS from a flow.

All results are foundational-triple-only (no busch_effect_gleason, no native_decide, no sorry).

Reference: specs/thermo-plan.md (TH1).

The density matrix entry of a projective ray

noncomputable def CSD.Thermo.rayDensity {N : ℕ} (p : LF4.CPN N) (i j : Fin N) : ℂ

The density-matrix entry of a ray. For a projective point p, the (i, j) entry of the rank-1 density operator |psi><psi| / ‖psi‖² of any representative. Fully scale-invariant (both modulus and phase cancel), so it is a genuine function of the ray. Diagonal entries are the moment-map coordinates (rayDensity_diag).

Equations

• CSD.Thermo.rayDensity p i j = (Projectivization.rep p).ofLp i * (starRingEnd ((fun (x : Fin N) => ℂ) j)) ((Projectivization.rep p).ofLp j) / ↑‖Projectivization.rep p‖ ^ 2

theorem CSD.Thermo.rayDensity_smul {N : ℕ} (c : ℂ) (hc : c ≠ 0) (v : EuclideanSpace ℂ (Fin N)) (i j : Fin N) : (c • v).ofLp i * (starRingEnd ((fun (x : Fin N) => ℂ) j)) ((c • v).ofLp j) / ↑‖c • v‖ ^ 2 = v.ofLp i * (starRingEnd ((fun (x : Fin N) => ℂ) j)) (v.ofLp j) / ↑‖v‖ ^ 2

Scale-invariance of the density entry under nonzero rescaling of the vector.

theorem CSD.Thermo.rayDensity_mk {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) (i j : Fin N) : rayDensity (Projectivization.mk ℂ ψ hψ) i j = ψ.ofLp i * (starRingEnd ((fun (x : Fin N) => ℂ) j)) (ψ.ofLp j) / ↑‖ψ‖ ^ 2

The density entry on a representative psi: scale-invariant, so it descends from the vector.

theorem CSD.Thermo.rayDensity_diag {N : ℕ} (p : LF4.CPN N) (i : Fin N) : rayDensity p i i = ↑(LF4.momentMap p i)

The diagonal density entries are the moment-map coordinates (rayDensity p i i = |psi_i|²/‖psi‖² = momentMap p i). This is what links the first moment's diagonal to the Duistermaat-Heckman / Born content.

Measurability, boundedness, integrability

theorem CSD.Thermo.coord_norm_le {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) (i : Fin N) : ‖v.ofLp i‖ ≤ ‖v‖

A single coordinate norm is bounded by the vector norm.

theorem CSD.Thermo.rayDensity_measurable {N : ℕ} (i j : Fin N) : Measurable fun (p : LF4.CPN N) => rayDensity p i j

The density entries are measurable on CP^{N-1}. Scale-invariant, so it descends from the measurable coordinate function on the nonzero subtype (same measurable_iff_measurable_comp_mk' route as momentMap_measurable).

theorem CSD.Thermo.rayDensity_norm_le_one {N : ℕ} (p : LF4.CPN N) (i j : Fin N) : ‖rayDensity p i j‖ ≤ 1

The density entries are bounded by one. ‖rayDensity p i j‖ ≤ 1 (coordinate norms bounded by the vector norm).

theorem CSD.Thermo.rayDensity_integrable {N : ℕ} (p₀ : LF4.CPN N) (i j : Fin N) : MeasureTheory.Integrable (fun (p : LF4.CPN N) => rayDensity p i j) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The density entries are integrable against Fubini-Study (bounded + measurable on a probability measure).

theorem CSD.Thermo.momentMap_integrable {N : ℕ} (p₀ : LF4.CPN N) (i : Fin N) : MeasureTheory.Integrable (fun (p : LF4.CPN N) => LF4.momentMap p i) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The moment coordinate is integrable against Fubini-Study.

The two symmetry unitaries: sign flip and permutation

theorem CSD.Thermo.toLin_unit_ne_zero {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : (Matrix.toEuclideanLin ↑U) v ≠ 0

A general nonzero-preservation for the unitary matrix action (local re-proof; the corpus's toEuclideanLin_unitary_ne_zero is private).

theorem CSD.Thermo.smul_eq_mk {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : LF4.CPN N) : U • p = Projectivization.mk ℂ ((Matrix.toEuclideanLin ↑U) (Projectivization.rep p)) ⋯

The projective unitary action, written as mk of the matrix action on rep.

noncomputable def CSD.Thermo.signFlipMat {N : ℕ} (i : Fin N) : Matrix (Fin N) (Fin N) ℂ

The sign-flip matrix diag(1, ..., -1, ..., 1) with -1 at index i. A real diagonal ±1 unitary; used to kill off-diagonal first-moment entries.

Equations

• CSD.Thermo.signFlipMat i = Matrix.diagonal fun (k : Fin N) => if k = i then -1 else 1

theorem CSD.Thermo.signFlipMat_mem {N : ℕ} (i : Fin N) : signFlipMat i ∈ Matrix.unitaryGroup (Fin N) ℂ

noncomputable def CSD.Thermo.signFlip {N : ℕ} (i : Fin N) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The sign-flip unitary as a group element.

Equations

• CSD.Thermo.signFlip i = ⟨CSD.Thermo.signFlipMat i, ⋯⟩

@[simp]

theorem CSD.Thermo.signFlip_val {N : ℕ} (i : Fin N) : ↑(signFlip i) = signFlipMat i

theorem CSD.Thermo.toEuclideanLin_signFlip_coord {N : ℕ} (i : Fin N) (v : EuclideanSpace ℂ (Fin N)) (a : Fin N) : ((Matrix.toEuclideanLin (signFlipMat i)) v).ofLp a = (if a = i then -1 else 1) * v.ofLp a

Coordinate action of the sign-flip.

theorem CSD.Thermo.signFlip_normSq {N : ℕ} (i : Fin N) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin (signFlipMat i)) v‖ ^ 2 = ‖v‖ ^ 2

The sign-flip is norm-preserving (squared form).

noncomputable def CSD.Thermo.permU {N : ℕ} (σ : Equiv.Perm (Fin N)) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The permutation matrix of sigma, packaged as a unitary group element.

Equations

• CSD.Thermo.permU σ = ⟨Equiv.Perm.permMatrix ℂ σ, ⋯⟩

@[simp]

theorem CSD.Thermo.permU_val {N : ℕ} (σ : Equiv.Perm (Fin N)) : ↑(permU σ) = Equiv.Perm.permMatrix ℂ σ

theorem CSD.Thermo.toEuclideanLin_perm_coord {N : ℕ} (σ : Equiv.Perm (Fin N)) (v : EuclideanSpace ℂ (Fin N)) (a : Fin N) : ((Matrix.toEuclideanLin (Equiv.Perm.permMatrix ℂ σ)) v).ofLp a = v.ofLp (σ a)

Coordinate action of a permutation unitary: (P_sigma v)_a = v_{sigma a}.

theorem CSD.Thermo.perm_normSq {N : ℕ} (σ : Equiv.Perm (Fin N)) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin (Equiv.Perm.permMatrix ℂ σ)) v‖ ^ 2 = ‖v‖ ^ 2

Permutation unitaries are norm-preserving.

The moment map transforms by permutation of coordinates

theorem CSD.Thermo.momentMap_permU {N : ℕ} [NeZero N] (σ : Equiv.Perm (Fin N)) (p : LF4.CPN N) (a : Fin N) : LF4.momentMap (permU σ • p) a = LF4.momentMap p (σ a)

Permutation equivariance of the moment map. momentMap (P_sigma . p) a = momentMap p (sigma a).

Off-diagonal first-moment entries vanish (sign-flip symmetry)

theorem CSD.Thermo.signFlip_smul_offdiag {N : ℕ} [NeZero N] (i j : Fin N) (hji : j ≠ i) (p : LF4.CPN N) : rayDensity (signFlip i • p) i j = -rayDensity p i j

The sign-flip sends an off-diagonal density entry to its negative: rayDensity ((signFlip i) . p) i j = - rayDensity p i j for j ≠ i.

theorem CSD.Thermo.fsFirstMoment_offdiag {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (i j : Fin N) (hij : i ≠ j) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), rayDensity p i j ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 0

The Fubini-Study first moment is diagonal: off-diagonal entries vanish. For i ≠ j, E_{mu_FS}[ rayDensity . i j ] = 0. Genuine change-of-variables against the sign-flip unitary (Fubini-Study invariance) plus the pointwise sign flip: M = -M.

Diagonal first-moment entries equal 1/N (permutation symmetry)

theorem CSD.Thermo.fsFirstMoment_diag_swap {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (i k : Fin N) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p k ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀

Diagonal first-moment entries are equal across coordinates (permutation symmetry): E[momentMap . i] = E[momentMap . k].

theorem CSD.Thermo.fsFirstMoment_diag {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (i : Fin N) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = (↑N)⁻¹

The diagonal first-moment entry is 1/N. All N diagonal integrals are equal (permutation symmetry) and sum to 1 (momentMap_sum_eq_one + measure_univ), so each is 1/N.

Deliverable 1: the Fubini-Study first moment

noncomputable def CSD.Thermo.fsFirstMoment {N : ℕ} (p₀ : LF4.CPN N) : Matrix (Fin N) (Fin N) ℂ

The Fubini-Study first-moment matrix E_{mu_FS}[ |psi><psi| ], entrywise.

Equations

• CSD.Thermo.fsFirstMoment p₀ = Matrix.of fun (i j : Fin N) => ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), CSD.Thermo.rayDensity p i j ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀

theorem CSD.Thermo.fs_first_moment {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) : fsFirstMoment p₀ = (↑N)⁻¹ • 1

Deliverable 1 (the key lemma): the Fubini-Study first moment is maximally mixed. E_{mu_FS}[ |psi><psi| ] = (1/N) I on CP^{N-1}. The average pure-state density operator over Fubini-Study is the maximally mixed state. Proved by a genuine integral computation: off-diagonal entries vanish by sign-flip invariance (fsFirstMoment_offdiag), diagonal entries are 1/N by permutation invariance + normalisation (fsFirstMoment_diag). Foundational-triple, Gleason-free.

Deliverable 2: canonical typicality in expectation (the headline)

noncomputable def CSD.Thermo.rayDensityMat {N : ℕ} (p : LF4.CPN N) : Matrix (Fin N) (Fin N) ℂ

The rank-1 density matrix of a ray as a genuine Matrix.

Equations

• CSD.Thermo.rayDensityMat p = Matrix.of (CSD.Thermo.rayDensity p)

noncomputable def CSD.Thermo.reducedRayDensity {N dS dE : ℕ} (e : Fin dS × Fin dE ≃ Fin N) (p : LF4.CPN N) : Matrix (Fin dS) (Fin dS) ℂ

The reduced density matrix of a ray, obtained by reindexing along a system-environment tensor split e : Fin d_S × Fin d_E ≃ Fin N and taking the partial trace over the environment (Matrix.traceRight, the genuine corpus partial trace).

Equations

• CSD.Thermo.reducedRayDensity e p = ((CSD.Thermo.rayDensityMat p).submatrix ⇑e ⇑e).traceRight

theorem CSD.Thermo.reducedRayDensity_apply {N dS dE : ℕ} (e : Fin dS × Fin dE ≃ Fin N) (p : LF4.CPN N) (i i' : Fin dS) : reducedRayDensity e p i i' = ∑ k : Fin dE, rayDensity p (e (i, k)) (e (i', k))

The reduced density entry as an explicit environment sum.

noncomputable def CSD.Thermo.fsReducedFirstMoment {N dS dE : ℕ} (e : Fin dS × Fin dE ≃ Fin N) (p₀ : LF4.CPN N) : Matrix (Fin dS) (Fin dS) ℂ

The average reduced state, entrywise: E_{mu_FS}[ Tr_E |psi><psi| ].

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.Thermo.canonical_typicality_expectation {N dS dE : ℕ} [NeZero N] [NeZero dS] [NeZero dE] (e : Fin dS × Fin dE ≃ Fin N) (p₀ : LF4.CPN N) : fsReducedFirstMoment e p₀ = (↑dS)⁻¹ • 1

Deliverable 2 (the headline): canonical typicality in expectation. For a tensor split H = H_S (x) H_E with N = d_S * d_E (encoded by the reindex equiv e), the Fubini-Study average reduced state is the canonical (maximally mixed, equal-energy / microcanonical) state on the subsystem: E_{mu_FS}[ Tr_E |psi><psi| ] = (1/d_S) I_S.

This is "thermal equilibrium from Fubini-Study volume", the FS-average ANALOGUE of LF6.maxEntangled_marginal_uniform (the specific maximally-entangled state's marginal) -- an analogy, not a formal Lean dependency (this theorem does not cite that lemma). Proof: partial-trace the first moment (fs_first_moment); the environment sum of (1/N) delta over d_E diagonal cells is (d_E/N) delta = (1/d_S) delta.

HONEST SCOPE: expectation (average), not the typical single state (concentration / Levy; see the residual section in the module docstring). Foundational-triple.

Concentration residual (the named stretch -- NOT proved here)

The strictly stronger typical-state statement (canonical typicality proper, Popescu-Short-Winter / Goldstein-Lebowitz-Tumulka-Zanghi) is:

for a small subsystem d_S in a large environment d_E, a mu_FS-typical single pure state psi has reduced state close to I_S/d_S: mu_FS { psi : ‖ Tr_E |psi><psi| - I_S/d_S ‖ >= eps } <= C * exp(-c * d_E * eps²).

This is not proved here. It requires Levy's lemma (measure concentration on the high-dimensional sphere S^{2N-1}: an L-Lipschitz function concentrates around its mean with Gaussian tails of width ~ L/sqrt(N)), which follows from the sphere's isoperimetric inequality / Ricci-curvature lower bound. Mathlib carries neither Levy's lemma nor the spherical isoperimetric inequality, so the concentration upgrade is the named residual of this tranche. The fs_first_moment result above is exactly the mean around which Levy's lemma would concentrate; what is missing is only the deviation bound, not the target value.

No sorry / axiom stands in for this: TH1 delivers the EXPECTATION and (Q24, below) the POLYNOMIAL Chebyshev tier, and names the exponential tier precisely as the residual.

Q24: the Chebyshev tier — second moments and polynomial concentration

(2026-08-21, specs/th1-concentration-scoping.md.) The concentration residual above splits into two tiers. The EXPONENTIAL (Lévy) tier still needs spherical isoperimetry and stays the recorded Mathlib-scale residual. The POLYNOMIAL (Chebyshev) tier needs only second moments, and those turn out to require no integrals at all: TH1's own twirl style, one moment higher, determines them algebraically. With a := E[xᵢ²], b := E[xᵢxⱼ] (i ≠ j, x := momentMap): permutation swaps make a index-free; the pointwise normalisation integrates to a + (N−1)b = 1/N; and invariance under a two-coordinate Hadamard rotation — with a sign flip killing the linear cross term and a quarter-phase flip halving the squared real part — gives a = 2b FOR EACH PAIR separately. Solve: a = 2/(N(N+1)), b = 1/(N(N+1)) — the Dirichlet values, by twirl algebra. Downstream: the second moment of any diagonal statistic is exact (fs_linear_sq_moment, giving Var = O(1/N)) and Chebyshev gives polynomial-rate typicality (fs_chebyshev_concentration), with no isoperimetry anywhere.

The quarter-phase unitary

noncomputable def CSD.Thermo.phaseFlipMat {N : ℕ} (i : Fin N) : Matrix (Fin N) (Fin N) ℂ

The quarter-phase matrix diag(1, ..., I, ..., 1) with Complex.I at index i. The signFlipMat pattern with a genuinely complex phase; used to kill squared off-diagonal entries (r² ↦ −r²) and to equate E[(Re r)²] with E[(Im r)²].

Equations

• CSD.Thermo.phaseFlipMat i = Matrix.diagonal fun (k : Fin N) => if k = i then Complex.I else 1

theorem CSD.Thermo.phaseFlipMat_mem {N : ℕ} (i : Fin N) : phaseFlipMat i ∈ Matrix.unitaryGroup (Fin N) ℂ

noncomputable def CSD.Thermo.phaseFlip {N : ℕ} (i : Fin N) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The quarter-phase unitary as a group element.

Equations

• CSD.Thermo.phaseFlip i = ⟨CSD.Thermo.phaseFlipMat i, ⋯⟩

@[simp]

theorem CSD.Thermo.phaseFlip_val {N : ℕ} (i : Fin N) : ↑(phaseFlip i) = phaseFlipMat i

theorem CSD.Thermo.toEuclideanLin_phaseFlip_coord {N : ℕ} (i : Fin N) (v : EuclideanSpace ℂ (Fin N)) (a : Fin N) : ((Matrix.toEuclideanLin (phaseFlipMat i)) v).ofLp a = (if a = i then Complex.I else 1) * v.ofLp a

Coordinate action of the quarter-phase.

theorem CSD.Thermo.phaseFlip_normSq {N : ℕ} (i : Fin N) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin (phaseFlipMat i)) v‖ ^ 2 = ‖v‖ ^ 2

The quarter-phase is norm-preserving (squared form).

The two-coordinate Hadamard rotation

noncomputable def CSD.Thermo.hadamardMat {N : ℕ} (i j : Fin N) : Matrix (Fin N) (Fin N) ℂ

The Hadamard rotation matrix at the (distinct) coordinate pair (i, j): the (1/√2)·[[1,1],[1,−1]] block on {i,j}, the identity elsewhere. Real symmetric; mixes exactly two coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.Thermo.hadamardMat_apply {N : ℕ} (i j a b : Fin N) : hadamardMat i j a b = if a = i then if b = i then (↑√2)⁻¹ else if b = j then (↑√2)⁻¹ else 0 else if a = j then if b = i then (↑√2)⁻¹ else if b = j then -(↑√2)⁻¹ else 0 else if b = a then 1 else 0

The Hadamard-rotation entries, unfolded.

theorem CSD.Thermo.hadamardMat_apply_of_ne {N : ℕ} (i j : Fin N) {a : Fin N} (hai : a ≠ i) (haj : a ≠ j) (b : Fin N) : hadamardMat i j a b = if b = a then 1 else 0

Off the pair {i, j}, a Hadamard-rotation row is a delta row.

theorem CSD.Thermo.hadamardMat_conjTranspose {N : ℕ} (i j : Fin N) (hij : i ≠ j) : (hadamardMat i j).conjTranspose = hadamardMat i j

The Hadamard rotation is Hermitian (real symmetric).

theorem CSD.Thermo.hadamardMat_mem {N : ℕ} (i j : Fin N) (hij : i ≠ j) : hadamardMat i j ∈ Matrix.unitaryGroup (Fin N) ℂ

noncomputable def CSD.Thermo.hadamardU {N : ℕ} (i j : Fin N) (hij : i ≠ j) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The Hadamard rotation as a unitary group element.

Equations

• CSD.Thermo.hadamardU i j hij = ⟨CSD.Thermo.hadamardMat i j, ⋯⟩

@[simp]

theorem CSD.Thermo.hadamardU_val {N : ℕ} (i j : Fin N) (hij : i ≠ j) : ↑(hadamardU i j hij) = hadamardMat i j

Coordinate actions of the new unitaries

theorem CSD.Thermo.toEuclideanLin_hadamard_coord_i {N : ℕ} (i j : Fin N) (hij : i ≠ j) (v : EuclideanSpace ℂ (Fin N)) : ((Matrix.toEuclideanLin (hadamardMat i j)) v).ofLp i = (↑√2)⁻¹ * (v.ofLp i + v.ofLp j)

Coordinate i of the Hadamard rotation: (H v)ᵢ = (vᵢ + vⱼ)/√2.

theorem CSD.Thermo.toEuclideanLin_hadamard_coord_j {N : ℕ} (i j : Fin N) (hij : i ≠ j) (v : EuclideanSpace ℂ (Fin N)) : ((Matrix.toEuclideanLin (hadamardMat i j)) v).ofLp j = (↑√2)⁻¹ * (v.ofLp i - v.ofLp j)

Coordinate j of the Hadamard rotation: (H v)ⱼ = (vᵢ − vⱼ)/√2.

theorem CSD.Thermo.toEuclideanLin_hadamard_coord_ne {N : ℕ} (i j : Fin N) {a : Fin N} (hai : a ≠ i) (haj : a ≠ j) (v : EuclideanSpace ℂ (Fin N)) : ((Matrix.toEuclideanLin (hadamardMat i j)) v).ofLp a = v.ofLp a

Away from the pair, the Hadamard rotation fixes coordinates.

theorem CSD.Thermo.hadamard_normSq {N : ℕ} (i j : Fin N) (hij : i ≠ j) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin (hadamardMat i j)) v‖ ^ 2 = ‖v‖ ^ 2

The Hadamard rotation is norm-preserving (squared form): the parallelogram law on the pair, the identity elsewhere.

Actions on the moment coordinates and the density entry

theorem CSD.Thermo.momentMap_signFlip {N : ℕ} [NeZero N] (i : Fin N) (p : LF4.CPN N) (a : Fin N) : LF4.momentMap (signFlip i • p) a = LF4.momentMap p a

The sign flip fixes every moment coordinate.

theorem CSD.Thermo.momentMap_phaseFlip {N : ℕ} [NeZero N] (i : Fin N) (p : LF4.CPN N) (a : Fin N) : LF4.momentMap (phaseFlip i • p) a = LF4.momentMap p a

The quarter-phase fixes every moment coordinate.

theorem CSD.Thermo.phaseFlip_smul_cross {N : ℕ} [NeZero N] (i j : Fin N) (hji : j ≠ i) (p : LF4.CPN N) : rayDensity (phaseFlip i • p) i j = Complex.I * rayDensity p i j

The quarter-phase multiplies the (i, j) density entry by I (j ≠ i).

theorem CSD.Thermo.momentMap_hadamard {N : ℕ} [NeZero N] (i j : Fin N) (hij : i ≠ j) (p : LF4.CPN N) : LF4.momentMap (hadamardU i j hij • p) i = (LF4.momentMap p i + LF4.momentMap p j + 2 * (rayDensity p i j).re) / 2

The Hadamard rotation mixes the pair through the density entry: x'ᵢ = (xᵢ + xⱼ + 2·Re r)/2 with r the (i,j) density entry.

The twirl transport, packaged once

theorem CSD.Thermo.fs_integral_unitary {N : ℕ} (p₀ : LF4.CPN N) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {f : LF4.CPN N → ℝ} (hf : Measurable f) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f (U • p) ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀

The change-of-variables engine: a Fubini–Study integral of a measurable real statistic equals its integral against any unitary pushforward. The fsFirstMoment_offdiag calc, packaged for reuse.

Measurability and integrability of the second-moment integrands

theorem CSD.Thermo.re_rayDensity_measurable {N : ℕ} (i j : Fin N) : Measurable fun (p : LF4.CPN N) => (rayDensity p i j).re

theorem CSD.Thermo.abs_re_rayDensity_le_one {N : ℕ} (p : LF4.CPN N) (i j : Fin N) : |(rayDensity p i j).re| ≤ 1

theorem CSD.Thermo.abs_im_rayDensity_le_one {N : ℕ} (p : LF4.CPN N) (i j : Fin N) : |(rayDensity p i j).im| ≤ 1

theorem CSD.Thermo.abs_momentMap_le_one {N : ℕ} (p : LF4.CPN N) (i : Fin N) : |LF4.momentMap p i| ≤ 1

theorem CSD.Thermo.fs_integrable_mul {N : ℕ} (p₀ : LF4.CPN N) {f g : LF4.CPN N → ℝ} (hf : Measurable f) (hg : Measurable g) (hfb : ∀ (p : LF4.CPN N), |f p| ≤ 1) (hgb : ∀ (p : LF4.CPN N), |g p| ≤ 1) : MeasureTheory.Integrable (fun (p : LF4.CPN N) => f p * g p) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

Integrability of a product of two of the bounded statistics, from explicit [-1, 1] bounds.

The kill lemmas

theorem CSD.Thermo.fs_cross_linear_zero {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] (a i j : Fin N) (hji : j ≠ i) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p a * (rayDensity p i j).re ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 0

The linear cross terms die: E[xₐ · Re r] = 0 for the (i,j) density entry r (j ≠ i), by the sign flip at i.

theorem CSD.Thermo.rayDensity_re_sq_add_im_sq {N : ℕ} (p : LF4.CPN N) (i j : Fin N) : (rayDensity p i j).re ^ 2 + (rayDensity p i j).im ^ 2 = LF4.momentMap p i * LF4.momentMap p j

Pointwise: (Re r)² + (Im r)² = xᵢ·xⱼ — the squared modulus of the density entry is the product of the two moment coordinates.

theorem CSD.Thermo.fs_re_sq_eq_im_sq {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] (i j : Fin N) (hji : j ≠ i) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (rayDensity p i j).re ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (rayDensity p i j).im ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀

E[(Re r)²] = E[(Im r)²], by the quarter-phase flip at i.

theorem CSD.Thermo.fs_re_sq_moment {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] (i j : Fin N) (hij : i ≠ j) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (rayDensity p i j).re ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = (∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i * LF4.momentMap p j ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀) / 2

The squared real part carries half the product: E[(Re r)²] = E[xᵢxⱼ]/2.

theorem CSD.Thermo.fs_x_sq_swap {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] (i k : Fin N) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p k ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀

Second moments of the coordinates are index-independent (permutation swap).

The engine: a = 2b, per pair

theorem CSD.Thermo.fs_x_sq_eq_two_cross {N : ℕ} (p₀ : LF4.CPN N) [NeZero N] {i j : Fin N} (hij : i ≠ j) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 2 * ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i * LF4.momentMap p j ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀

★ The Hadamard identity a = 2b (Q24, the route discovery): invariance of the second moment under the two-coordinate Hadamard rotation, with the sign flip killing the linear cross terms and the quarter-phase halving the squared real part, forces E[xᵢ²] = 2·E[xᵢxⱼ] — for each pair separately, with no integral ever computed.

The second moments themselves

With a = 2b (per pair) and the integrated normalisation a + (N−1)·b = 1/N, both moments are determined: a = 2/(N(N+1)), b = 1/(N(N+1)) — the Dirichlet values, with no simplex integral in sight.

theorem CSD.Thermo.fs_x_sq_moment {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (i : Fin N) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 2 / (↑N * (↑N + 1))

★ The diagonal second moment: E[xᵢ²] = 2/(N(N+1)).

theorem CSD.Thermo.fs_x_cross_moment {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) {i j : Fin N} (hij : i ≠ j) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), LF4.momentMap p i * LF4.momentMap p j ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 1 / (↑N * (↑N + 1))

★ The cross second moment: E[xᵢxⱼ] = 1/(N(N+1)) for i ≠ j.

Diagonal statistics: expectation, second moment, Chebyshev

theorem CSD.Thermo.fs_linear_expectation {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (lam : Fin N → ℝ) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), ∑ k : Fin N, lam k * LF4.momentMap p k ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = (∑ k : Fin N, lam k) / ↑N

The expectation of a diagonal statistic Σ λₖ·xₖ is (Σλ)/N — the maximally-mixed value.

theorem CSD.Thermo.fs_linear_sq_moment {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (lam : Fin N → ℝ) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (∑ k : Fin N, lam k * LF4.momentMap p k) ^ 2 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = ((∑ k : Fin N, lam k) ^ 2 + ∑ k : Fin N, lam k ^ 2) / (↑N * (↑N + 1))

★ The second moment of a diagonal statistic: E[(Σ λₖxₖ)²] = ((Σλ)² + Σλ²)/(N(N+1)).

theorem CSD.Thermo.fs_chebyshev_concentration {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) (lam : Fin N → ℝ) {ε : ℝ} (hε : 0 < ε) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) {p : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) | ε ≤ |∑ k : Fin N, lam k * LF4.momentMap p k - (∑ k : Fin N, lam k) / ↑N|} ≤ ENNReal.ofReal ((↑N * ∑ k : Fin N, lam k ^ 2 - (∑ k : Fin N, lam k) ^ 2) / (↑N ^ 2 * (↑N + 1)) / ε ^ 2)

★★ Chebyshev-grade canonical typicality (Q24, diagonal form): a single Fubini–Study sample concentrates its diagonal statistics at the maximally-mixed value, at rate Var = (N·Σλ² − (Σλ)²)/(N²(N+1)) = O(1/N) — polynomial concentration with no isoperimetry, from the twirl algebra alone.