TH5d: the Jarzynski equality at the Σ level — the record-layer work statistics are TH5a's

Category: 7-SigmaLayer (the record layer — thermodynamics stated on Σ, not on bare matrices; specs/thermo-plan.md TH5, specs/BACKLOG.md ▶ OPEN QUEUE #4; the first thermodynamic consumer of Q29(e)).

Glossary: https://glossary.constraintsurfacedynamics.com/jarzynski-equality/

What "at the Σ level" means here

TH5a (Thermo/Jarzynski.lean) is a theorem about matrices: a joint law tpmLaw DEFINED as Gibbs weight × transition probability, and the identity ∑ tpmLaw · e^{−βW} = Z₁/Z₀. This module runs the same protocol as records on the sector and proves that the record statistics ARE tpmLaw:

• the preparation is the Gibbs state as a mixed preparation on the swap arena (gibbsDensity, mixedReadyPrep — the spectral two-stage sampling of MixedSwap.lean), with the first bank calibrated to the energy eigenrays of H₀ (rotatedBank);
• the first readout is the energy context of H₀ — the apparatus reading the eigenbasis hH₀.eigenvectorBasis (basisContext, RotatedContext.lean);
• between the readouts the system is DRIVEN: its ontic base point moves by the unitary U acting on ℂℙ^{N−1}, the pointer fibre untouched (baseLift (U • ·) = the corpus's U(N) action on Σ, baseLift_unitary_smul), as the driveStage of DrivenTwoTime.lean;
• the second readout is the energy context of H₁.

★★ sigma_tpm_law: the driven two-stage preparation gives the joint record sector (energy record i at t₁, energy record j at t₂) exactly the mass tpmLaw hH₀ hH₁ U β i j. Not a definition — the Gibbs weight is the mixed dynamical Born weight of the first readout (traceForm_gibbsDensity_energy through driven_mixed_two_time_born), and the transition probability is the second context's rate at the DRIVEN collapsed state (basisContext_rate_smul). No positivity hypothesis: Gibbs weights are strictly positive (gibbsWeight_pos), so the conditioning is always licensed.

★★ sigma_jarzynski: hence ∑ᵢⱼ P_Σ(i, j) · e^{−βW(i,j)} = Z₁/Z₀ for the record probabilities P_Σ, with ★★ sigma_jarzynski_freeEnergy (= e^{−βΔF} in TH3's free energies) and ★ sigma_mean_work_ge_freeEnergy_sub (the second law of the driven process, on Σ); sum_tpmSigmaSector (the record law is a probability law), sigma_first_energy_record (the first readout's records carry the Gibbs weights; no retro-action from the drive).

Q29(e) consumed

★★ sigma_tpm_law_hamiltonianFlow, ★★ sigma_jarzynski_hamiltonianFlow: the drive written as the MANIFOLD Hamiltonian flow IsSymplectic.hamiltonianFlow of the Schrödinger Hamiltonian −2⟨H_d⟩ for the Fubini–Study form (HamiltonianFlowVolume.lean), for a driving Hamiltonian H_d over a time τ. Q29(e)'s identification hamiltonianFlow_schrodingerHamiltonian turns it into exp(−iτH_d) • ·, and the theorem above applies. This is the first thermodynamic statement in the corpus whose driving is the sector's own Hamiltonian flow rather than a matrix.

CSD reading

Work is what the two energy records disagree by; the exponential average over the driven record chain is a state function of the two equilibrium endpoints. Nothing in the protocol is a matrix identity: the Gibbs weights are the Born weights the first record dynamics assigns to the mixed preparation, the transition weights are the Born weights the second record dynamics assigns to the relocated-and-driven state, and the equality is bookkeeping on the doubly stochastic transition matrix that unitarity forces (TH5a). The thermodynamics of a driven process lives on the record layer.

⚠️ Honest scope

• Liouville is not consumed by the theorem, and the row's phrasing is corrected. The row (BACKLOG #4) reads "an absolutely continuous preparation density is transported". The Gibbs preparation here is the spectral mixture of Diracs on the base (mixedReadyPrep, Haar on the fibre), and the collapsed states are Diracs; the drive transports them pointwise. The manifold-level Liouville theorem (fsVolume_map_hamiltonianFlow) is what Q29(e) is FOR, but the two-point-measurement law needs only the flow's identification, not its measure-preservation. An absolutely-continuous-density formulation of the Gibbs preparation (ρ_ep dμ_FS, W3's form) would consume Liouville; it is not the corpus's canonical mixed preparation and is not built here.
• The drive is a single unitary U (or exp(−iτH_d) for a constant driving Hamiltonian); a time-dependent protocol is the ordered product of such steps and is not composed here.
• Closed driven system, finite dimension, projective energy readouts in the spectral eigenbases, the same β at both ends — TH5a's scope; the [NeZero N] of the record layer stands in for TH3's [Nonempty n].
• Gleason-free, structurally. LF2/EffectGleason.lean is absent from this module's transitive import closure (declared in scripts/check-import-negative.sh), so no proof here can reach the effect-Gleason representation: the Born weights are the record dynamics'. trace_mul_outerProduct' restates that module's trace_mul_outerProduct on a general index for exactly this reason (rule-of-two note: rehome to LF2/BornWrapper.lean when next touched).

References

specs/thermo-plan.md TH5; specs/BACKLOG.md (▶ OPEN QUEUE #4 = TH5d; Q29(e)); specs/generator-layer-scoping.md §11 (Q29); Thermo/Jarzynski.lean (TH5a: tpmLaw, tpmTransition_eq, gibbsWeight_eq_re_born, jarzynski, jarzynski_freeEnergy, mean_work_ge_freeEnergy_sub); Thermo/FreeEnergy.lean (TH3: gibbsState, gibbsWeight_pos, gibbsState_posDef, gibbsState_trace); RecordLayer/DrivenTwoTime.lean (driven_mixed_two_time_born, baseLift); RecordLayer/RotatedContext.lean (basisContext_rate_mk); RecordLayer/RotatedSwap.lean (basisPoint); Mathlib/Geometry/Manifold/Instances/ProjectiveSpaceSchrodingerFlow.lean (hamiltonianFlow_schrodingerHamiltonian, Q29(e)); LF4/ProjectedDynamics.lean (schrodingerUnitary); specs/future-work.md.

theorem CSD.RecordLayer.trace_mul_outerProduct' {ι : Type u_1} [Fintype ι] (R : Matrix ι ι ℂ) (v : EuclideanSpace ℂ ι) : (R * LF2.outerProduct v).trace = star v.ofLp ⬝ᵥ R.mulVec v.ofLp

tr(R · ∣v⟩⟨v∣) = ⟨v, R v⟩ on a general finite index (trace_mul_outerProduct of LF2/EffectGleason.lean, restated to keep that module out of this closure).

The Gibbs preparation and the energy contexts

noncomputable def CSD.RecordLayer.gibbsDensity {N : ℕ} [NeZero N] {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (β : ℝ) : LF2.DensityOperator N

The Gibbs state as a density operator (TH3's gibbsState, packaged for the record tier).

Equations

• CSD.RecordLayer.gibbsDensity hH₀ β = { M := CSD.Thermo.gibbsState H₀ hH₀ β, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.RecordLayer.gibbsDensity_M {N : ℕ} [NeZero N] {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (β : ℝ) : (gibbsDensity hH₀ β).M = Thermo.gibbsState H₀ hH₀ β

theorem CSD.RecordLayer.traceForm_gibbsDensity_energy {N : ℕ} [NeZero N] {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (β : ℝ) (i : Fin N) : LF2.traceForm (gibbsDensity hH₀ β) (LF2.rankOneEffect (hH₀.eigenvectorBasis i) ⋯) = Thermo.gibbsWeight H₀ hH₀ β (hH₀.eigenvalues i)

The Gibbs weight is the record tier's Born pairing at the energy outcome: Tr(ρ_β ∣e₀ᵢ⟩⟨e₀ᵢ∣) = e^{−βE₀ᵢ}/Z₀.

theorem CSD.RecordLayer.basisContext_rate_smul {N : ℕ} {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (i j : Fin N) : (basisContext hH₁.eigenvectorBasis).rate (U • basisPoint hH₀.eigenvectorBasis i) j = Thermo.tpmTransition hH₀ hH₁ U i j

The second energy readout's rate at the driven collapsed state is the transition probability: the context reading the eigenbasis of H₁, evaluated at U • [e₀ᵢ], assigns outcome j the weight ‖⟨e₁ⱼ, U e₀ᵢ⟩‖² = tpmTransition i j.

The Σ-level two-point-measurement protocol

noncomputable def CSD.RecordLayer.tpmSigmaPrep {N : ℕ} [NeZero N] {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (β : ℝ) : MeasureTheory.Measure (TwoStageArena (LF4.KSigma N) N)

The Σ-level two-point-measurement preparation: the Gibbs state of H₀ as the mixed preparation on the two-stage arena, the first bank calibrated to the energy eigenrays of H₀.

Equations

• CSD.RecordLayer.tpmSigmaPrep hH₀ β = CSD.RecordLayer.rotatedMixedTwoPrep hH₀.eigenvectorBasis (CSD.RecordLayer.gibbsDensity hH₀ β)

instance CSD.RecordLayer.instIsProbabilityMeasureTwoStageArenaKSigmaTpmSigmaPrep {N : ℕ} [NeZero N] {H₀ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (β : ℝ) : MeasureTheory.IsProbabilityMeasure (tpmSigmaPrep hH₀ β)

noncomputable def CSD.RecordLayer.tpmSigmaSector {N : ℕ} [NeZero N] {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (i j : Fin N) : Set (TwoStageArena (LF4.KSigma N) N)

The Σ-level joint record sector: the initial states destined to display energy record i (in the eigenbasis of H₀) at t₁ and, after the drive U on the sector, energy record j (in the eigenbasis of H₁) at t₂.

Equations

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

theorem CSD.RecordLayer.sigma_tpm_law {N : ℕ} [NeZero N] {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (β : ℝ) (i j : Fin N) : (tpmSigmaPrep hH₀ β) (tpmSigmaSector hH₀ hH₁ U i j) = ENNReal.ofReal (Thermo.tpmLaw hH₀ hH₁ U β i j)

★★ TH5d, the law: the record statistics of the Σ-level protocol ARE tpmLaw. The driven two-stage preparation gives the joint sector (energy record i at t₁, energy record j at t₂) exactly the mass gibbsWeight (E₀ i) · ‖⟨e₁ j, U e₀ i⟩‖². No positivity hypothesis: Gibbs weights are strictly positive.

theorem CSD.RecordLayer.sum_tpmSigmaSector {N : ℕ} [NeZero N] {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (β : ℝ) : ∑ i : Fin N, ∑ j : Fin N, (tpmSigmaPrep hH₀ β) (tpmSigmaSector hH₀ hH₁ U i j) = 1

The Σ-level record law is a probability law on the outcome pairs.

theorem CSD.RecordLayer.sigma_first_energy_record {N : ℕ} [NeZero N] {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (β : ℝ) (i : Fin N) : (tpmSigmaPrep hH₀ β) (drivenTwoStage (basinIndex (basisContext hH₀.eigenvectorBasis)) (baseLift fun (p : LF4.CPN N) => U • p) (basinIndex (basisContext hH₁.eigenvectorBasis)) ⁻¹' recordOneEvent i) = ENNReal.ofReal (Thermo.gibbsWeight H₀ hH₀ β (hH₀.eigenvalues i))

The first energy readout's records carry the Gibbs weights, and neither the drive nor the second apparatus retro-acts on them.

★★ Jarzynski on Σ

theorem CSD.RecordLayer.sigma_jarzynski {N : ℕ} [NeZero N] {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (β : ℝ) : ∑ i : Fin N, ∑ j : Fin N, ((tpmSigmaPrep hH₀ β) (tpmSigmaSector hH₀ hH₁ U i j)).toReal * Real.exp (-β * Thermo.tpmWork hH₀ hH₁ i j) = Thermo.partitionFn H₁ hH₁ β / Thermo.partitionFn H₀ hH₀ β

★★ TH5d — the Jarzynski equality on Σ. The exponential average of the two-point- measurement work over the RECORD probabilities of the driven protocol on the sector is the ratio of the partition functions, ∑ᵢⱼ P_Σ(i, j) · e^{−βW(i,j)} = Z₁/Z₀.

theorem CSD.RecordLayer.sigma_jarzynski_freeEnergy {N : ℕ} [NeZero N] {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {β : ℝ} (hβ : 0 < β) : ∑ i : Fin N, ∑ j : Fin N, ((tpmSigmaPrep hH₀ β) (tpmSigmaSector hH₀ hH₁ U i j)).toReal * Real.exp (-β * Thermo.tpmWork hH₀ hH₁ i j) = Real.exp (-β * (Thermo.freeEnergy H₁ β⁻¹ ⋯ - Thermo.freeEnergy H₀ β⁻¹ ⋯))

★★ Jarzynski on Σ, free-energy form: ⟨e^{−βW}⟩_Σ = e^{−β(F₁ − F₀)} in TH3's equilibrium free energies.

theorem CSD.RecordLayer.sigma_mean_work_ge_freeEnergy_sub {N : ℕ} [NeZero N] {H₀ H₁ : Matrix (Fin N) (Fin N) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {β : ℝ} (hβ : 0 < β) : Thermo.freeEnergy H₁ β⁻¹ ⋯ - Thermo.freeEnergy H₀ β⁻¹ ⋯ ≤ ∑ i : Fin N, ∑ j : Fin N, ((tpmSigmaPrep hH₀ β) (tpmSigmaSector hH₀ hH₁ U i j)).toReal * Thermo.tpmWork hH₀ hH₁ i j

★ The second law of the driven process, on Σ: the mean work over the record probabilities is at least the free-energy difference, ΔF ≤ ⟨W⟩_Σ.

Q29(e) consumed: the drive as the manifold Hamiltonian flow

theorem CSD.RecordLayer.hamiltonianFlow_schrodinger_eq {n : ℕ} {Hd : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hHd : Hd.IsHermitian) (τ : ℝ) : ⋯.hamiltonianFlow ⋯ τ = fun (p : LF4.CPN (n + 1)) => Matrix.schrodingerUnitary hHd τ • p

The drive as the Hamiltonian flow of the Schrödinger Hamiltonian. The manifold flow IsSymplectic.hamiltonianFlow of −2⟨H_d⟩ for the Fubini–Study form, run for time τ, is the unitary flow exp(−iτH_d) • · (Q29(e), hamiltonianFlow_schrodingerHamiltonian), as a function.

theorem CSD.RecordLayer.sigma_tpm_law_hamiltonianFlow {n : ℕ} {H₀ H₁ Hd : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (hHd : Hd.IsHermitian) (τ β : ℝ) (i j : Fin (n + 1)) : (tpmSigmaPrep hH₀ β) (drivenJointRecordSector (basinIndex (basisContext hH₀.eigenvectorBasis)) (baseLift (⋯.hamiltonianFlow ⋯ τ)) (basinIndex (basisContext hH₁.eigenvectorBasis)) i j) = ENNReal.ofReal (Thermo.tpmLaw hH₀ hH₁ (Matrix.schrodingerUnitary hHd τ) β i j)

★★ TH5d with the drive as the sector's Hamiltonian flow (Q29(e) consumed): with the system driven for a time τ by the MANIFOLD Hamiltonian flow of the Schrödinger Hamiltonian of H_d on ℂℙⁿ, the joint record law is tpmLaw at the unitary exp(−iτH_d).

theorem CSD.RecordLayer.sigma_jarzynski_hamiltonianFlow {n : ℕ} {H₀ H₁ Hd : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH₀ : H₀.IsHermitian) (hH₁ : H₁.IsHermitian) (hHd : Hd.IsHermitian) (τ β : ℝ) : ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), ((tpmSigmaPrep hH₀ β) (drivenJointRecordSector (basinIndex (basisContext hH₀.eigenvectorBasis)) (baseLift (⋯.hamiltonianFlow ⋯ τ)) (basinIndex (basisContext hH₁.eigenvectorBasis)) i j)).toReal * Real.exp (-β * Thermo.tpmWork hH₀ hH₁ i j) = Thermo.partitionFn H₁ hH₁ β / Thermo.partitionFn H₀ hH₀ β

★★ Jarzynski on Σ with the drive as the sector's Hamiltonian flow (Q29(e) consumed): the exponential average of the work over the record probabilities of the protocol driven by the Hamiltonian flow of −2⟨H_d⟩ for time τ is Z₁/Z₀.