diff --git a/.github/workflows/paper.yml b/.github/workflows/paper.yml new file mode 100644 index 0000000..95883a6 --- /dev/null +++ b/.github/workflows/paper.yml @@ -0,0 +1,28 @@ +name: Paper + +on: + push: + paths: + - "paper/**" + - ".github/workflows/paper.yml" + pull_request: + paths: + - "paper/**" + - ".github/workflows/paper.yml" + +jobs: + build-pdf: + runs-on: ubuntu-latest + # For a release, pin this image by digest so the TeX Live snapshot is frozen. + container: texlive/texlive:latest + steps: + - uses: actions/checkout@v4 + - name: Build manuscript + run: | + cd paper + latexmk -pdf -interaction=nonstopmode -halt-on-error main.tex + - name: Upload PDF + uses: actions/upload-artifact@v4 + with: + name: paper-pdf + path: paper/main.pdf diff --git a/.gitignore b/.gitignore index cf1dacc..6dbd14d 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,18 @@ .lake/ +# LaTeX build output +paper/*.aux +paper/*.bbl +paper/*.bcf +paper/*.blg +paper/*.fdb_latexmk +paper/*.fls +paper/*.log +paper/*.out +paper/*.pdf +paper/*.run.xml +paper/*.synctex.gz + # local agent configs .codex/ .claude/ diff --git a/ARTIFACT.md b/ARTIFACT.md new file mode 100644 index 0000000..f4c8b5d --- /dev/null +++ b/ARTIFACT.md @@ -0,0 +1,144 @@ +# Artifact guide and paper theorem spine + +This file gives reviewers and contributors a compact route through the continuous-time result that the paper treats as the main contribution. + +## Claim under review + +The artifact connects one chain of objects: + +> finite-state generator -> normalized fixed-horizon path measure -> finite-horizon sector-tail non-explosion -> actual terminal and finite-dimensional marginals -> measurable global driven path law -> physical Crooks--Jarzynski relations. + +The paper does not rely on every module in the repository. The six stages below are the intended reviewer path. + +## Snapshot and dependencies + +- Core formalization baseline: [`efbf55e`](https://github.com/kiyo-e/CrooksJarzynskiLean/commit/efbf55ea2876fe016df8d64b25a661a7394b6464), which includes the time-reversal mirror theorems (`ContinuousTimeJumpTrajectoryReversal.lean`) and the KL dissipation identity (`ContinuousTimeJumpDrivenKL.lean`) cited in the manuscript. +- Manuscript sources, this artifact guide, and the interior-time theorem (`ContinuousTimeJumpTwoStateInteriorTime.lean`): contained in the artifact commit that extends the baseline (the head of the manuscript branch; checking out the baseline alone does not reproduce them). +- Lean toolchain: `leanprover/lean4:v4.32.0`. +- Mathlib and all Lake dependencies: fixed by `lake-manifest.json`. +- Physlib: pinned by commit in `lakefile.lean`. + +A publication release should replace both commit references with a single versioned artifact tag and archival DOI, so that one checkout reproduces the manuscript and every Lean declaration it cites. + +## Build and proof audit + +```bash +lake exe cache get +lake build +``` + +The CI workflow additionally rejects `sorry`, `admit`, `sorryAx`, and custom `axiom` or `constant` declarations, then runs: + +```bash +lake env lean CrooksJarzynski/AxiomAudit.lean +lake env lean CrooksJarzynski/AxiomAuditDriven.lean +``` + +The audit permits only the standard environment axioms `propext`, `Classical.choice`, and `Quot.sound`. + +## Six-stage theorem spine + +### 1. A nonzero fixed-horizon reference + +File: [`CrooksJarzynski/ContinuousTimeJumpSimplex.lean`](CrooksJarzynski/ContinuousTimeJumpSimplex.lean) + +Key declarations: + +- `MeasureProtocol.ContinuousTimeJump.Simplex.volume_freeSimplexSet` proves free-coordinate volume `1 / n!`; +- `MeasureProtocol.ContinuousTimeJump.Simplex.sum_holdingTimesOfFree` proves that the residual coordinate makes the total holding time exactly `T`; +- `MeasureProtocol.ContinuousTimeJump.Simplex.rawPathProbability_ae_horizon` proves fixed-horizon support. + +Why it matters: restricting ambient product Lebesgue measure to `sum τ = T` would be null. The free-coordinate chart gives a nonzero measure that can be normalized and reversed. + +### 2. Tail disappearance and normalization + +File: [`CrooksJarzynski/ContinuousTimeJumpFiniteGeneratorPathLaw.lean`](CrooksJarzynski/ContinuousTimeJumpFiniteGeneratorPathLaw.lean) + +Key declarations: + +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.tendsto_arrivalMassFrom` proves disappearance of the unfinished-arrival mass; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.sum_sectorMassFrom_add_arrivalMassFrom` is the telescoping identity; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.tsum_sectorMassFrom` proves that all completed sector masses sum to one. + +Why it matters: this is the finite-horizon non-explosion argument. No probability mass escapes to infinitely many jumps before the horizon. + +### 3. The actual full path probability measure + +File: [`CrooksJarzynski/ContinuousTimeJumpFiniteGeneratorFullPath.lean`](CrooksJarzynski/ContinuousTimeJumpFiniteGeneratorFullPath.lean) + +Key declarations: + +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom` constructs the measure on the disjoint union of jump sectors; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.instIsProbabilityMeasurePathLawFrom` packages normalization as an `IsProbabilityMeasure` instance; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_terminalState_singleton` proves that the arithmetic transition mass is the terminal pushforward of this measure. + +Why it matters: all downstream theorems refer to a constructed probability law, not only to separately computed sector sums. + +### 4. Matrix exponential and Markov semigroup + +File: [`CrooksJarzynski/ContinuousTimeJumpFiniteGeneratorBridge.lean`](CrooksJarzynski/ContinuousTimeJumpFiniteGeneratorBridge.lean) + +Key declarations: + +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.transitionReal_eq_exp` identifies the residual-fraction renewal solution with the matrix exponential; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_terminalState_eq_exp_generator` identifies the actual terminal marginal with a row of `exp (TQ)`; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.transitionKernel` packages the terminal laws as a Mathlib Markov kernel; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.transitionKernel_add` proves the kernel semigroup law. + +Related path-level result: + +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_add` in `ContinuousTimeJumpConcatPathLaw.lean` proves Chapman--Kolmogorov before taking the terminal pushforward. + +### 5. Finite-dimensional distributions + +File: [`CrooksJarzynski/ContinuousTimeJumpFiniteDimensional.lean`](CrooksJarzynski/ContinuousTimeJumpFiniteDimensional.lean) + +Key declarations: + +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_finiteDimensional_eq` identifies the finite-time sampling pushforward with the chronological transition-kernel path measure for nondecreasing observation families starting at time zero; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_sampleAt_real_singleton_eq_exp_product` gives the matrix-exponential product formula for the corresponding finite-dimensional atoms; +- `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_finiteDimensional_eq_general` and `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_sampleAt_real_singleton_eq_exp_product_general` extend both statements to arbitrary nondecreasing observation times, without the time-zero requirement. + +Why it matters: the bridge is not restricted to the endpoint. The constructed real-time path has the expected finite-dimensional laws. + +### 6. Global driven laws and fluctuation relations + +Files: + +- [`CrooksJarzynski/ContinuousTimeJumpDrivenConcat.lean`](CrooksJarzynski/ContinuousTimeJumpDrivenConcat.lean) +- [`CrooksJarzynski/ContinuousTimeJumpDrivenGlobalLaw.lean`](CrooksJarzynski/ContinuousTimeJumpDrivenGlobalLaw.lean) +- [`CrooksJarzynski/ContinuousTimeJumpDrivenGlobalCrooks.lean`](CrooksJarzynski/ContinuousTimeJumpDrivenGlobalCrooks.lean) + +Key declarations: + +- `MeasureProtocol.ContinuousTimeJump.Driven.concatenateWindows` glues complete window paths in chronological order; +- `MeasureProtocol.ContinuousTimeJump.Driven.measurable_concatenateWindows` proves measurability; +- `MeasureProtocol.ContinuousTimeJump.Driven.forwardGlobalLaw` and `reverseGlobalLaw` construct probability laws on one global `FullPath` chart; +- `MeasureProtocol.ContinuousTimeJump.Driven.globalWork` reads switching work from the global trajectory; +- `MeasureProtocol.ContinuousTimeJump.Driven.global_crooks_of_gibbsDetailedBalance` proves the global path-measure Crooks relation; +- `MeasureProtocol.ContinuousTimeJump.Driven.global_jarzynski_of_gibbsDetailedBalance` proves Jarzynski's equality; +- `MeasureProtocol.ContinuousTimeJump.Driven.global_second_law_of_gibbsDetailedBalance` proves the average-work second law; +- `MeasureProtocol.ContinuousTimeJump.Driven.global_work_distribution_crooks_reverseWork_of_gibbsDetailedBalance` and `global_crooks_work_atom_of_gibbsDetailedBalance` provide the work-distribution and conventional atomwise forms. + +## Concrete validation targets + +- `FiniteJumpGenerator.ThreeStateBranching` exercises a genuinely branching chain beyond two-state parity. +- `Driven.ThreeStateTwoWindow` has positive-probability work values `0` and `log 2`, including events with the same endpoint pair `(0, 0)`, proving that work is not almost surely an endpoint-only observable. +- `TwoState.AsymmetricExample` supplies explicit rates, Gibbs weights, partition functions, free energy, work atoms, mean work, strict second law, and a one-window driven specialization. + +## Documentation map + +- [`PAPER.md`](PAPER.md): publication-package entry point; +- [`paper/main.tex`](paper/main.tex): manuscript draft; +- [`RELATED_WORK.md`](RELATED_WORK.md): literature positioning and bounded priority statement; +- [`FORMALIZATION.md`](FORMALIZATION.md): complete paper-level-to-Lean declaration map; +- [`DRIVEN_PROTOCOL.md`](DRIVEN_PROTOCOL.md): design notes for marked windows, concatenation, global work, and examples; +- [`CITATION.cff`](CITATION.cff): software citation metadata. + +## Release checklist + +1. Freeze a versioned tag from a green CI commit. +2. Archive the tag and add its DOI to `CITATION.cff` and the paper. +3. Re-audit Ripple and PhysicsAI at fixed commits and update `RELATED_WORK.md` if their scope has changed. +4. Compile `paper/main.tex` and archive the PDF with the source. +5. Keep the abstract and introduction focused on the end-to-end connection rather than on broad “first” claims. diff --git a/CrooksJarzynski.lean b/CrooksJarzynski.lean index 849dc0f..0ec0885 100644 --- a/CrooksJarzynski.lean +++ b/CrooksJarzynski.lean @@ -28,6 +28,7 @@ import CrooksJarzynski.ContinuousTimeJumpRenewalIntegrals import CrooksJarzynski.ContinuousTimeJumpFiniteGenerator import CrooksJarzynski.ContinuousTimeJumpTwoStateNormalization import CrooksJarzynski.ContinuousTimeJumpTwoStateFiniteGenerator +import CrooksJarzynski.ContinuousTimeJumpTwoStateInteriorTime import CrooksJarzynski.ContinuousTimeJumpTwoStateAsymmetric import CrooksJarzynski.ContinuousTimeJumpTwoStateAsymmetricNormalization import CrooksJarzynski.ContinuousTimeJumpTwoStateAsymmetricJarzynski @@ -47,6 +48,7 @@ import CrooksJarzynski.ContinuousTimeJumpConcatPathLaw import CrooksJarzynski.ContinuousTimeJumpConcatPathLawBridge import CrooksJarzynski.ContinuousTimeJumpFiniteDimensional import CrooksJarzynski.ContinuousTimeJumpFullPathReversal +import CrooksJarzynski.ContinuousTimeJumpTrajectoryReversal import CrooksJarzynski.ContinuousTimeJumpDriven import CrooksJarzynski.ContinuousTimeJumpDrivenBalance import CrooksJarzynski.ContinuousTimeJumpDrivenDensity @@ -64,6 +66,7 @@ import CrooksJarzynski.ContinuousTimeJumpDrivenEndpointLaw import CrooksJarzynski.ContinuousTimeJumpDrivenEndpointExp import CrooksJarzynski.ContinuousTimeJumpDrivenThreeStateTwoWindow import CrooksJarzynski.ContinuousTimeJumpDrivenGlobalCrooks +import CrooksJarzynski.ContinuousTimeJumpDrivenKL import CrooksJarzynski.ContinuousTimeJumpDrivenGlobalThreeStateTwoWindow import CrooksJarzynski.ContinuousTimeJumpDrivenTwoState import CrooksJarzynski.ContinuousTimeJumpDrivenTwoStateComparison diff --git a/CrooksJarzynski/AxiomAudit.lean b/CrooksJarzynski/AxiomAudit.lean index 43e19f1..bb85e84 100644 --- a/CrooksJarzynski/AxiomAudit.lean +++ b/CrooksJarzynski/AxiomAudit.lean @@ -127,6 +127,7 @@ the trusted base of the development. #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.TwoState.conditionalTerminalLaw_real_singleton_eq #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.TwoState.exp_smul_generator_apply #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.TwoState.conditionalTerminalLaw_eq_exp_generator +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.TwoState.trajectory_interior_not_ae_endpointFunction #print axioms CrooksJarzynski.Protocol.measure_forwardWeight_singleton #print axioms CrooksJarzynski.Protocol.measure_reverseWeight_singleton #print axioms CrooksJarzynski.Protocol.measure_crooks @@ -198,8 +199,10 @@ the trusted base of the development. #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathKernel_add #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.transitionKernel_add_from_pathLawFrom_add #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_finiteDimensional_eq +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_finiteDimensional_eq_general #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.map_pathLawFrom_trajectory_eq_transitionKernel #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_sampleAt_real_singleton_eq_exp_product +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_sampleAt_real_singleton_eq_exp_product_general #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_trajectory_real_singleton_eq_exp_generator #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.ThreeStateBranching.pathLawFrom_terminalState_eq_exp_generator #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.TwoState.finiteGenerator_pathLawFrom_terminalState_eq_exp_generator diff --git a/CrooksJarzynski/AxiomAuditDriven.lean b/CrooksJarzynski/AxiomAuditDriven.lean index 5c0e2f1..477b9a3 100644 --- a/CrooksJarzynski/AxiomAuditDriven.lean +++ b/CrooksJarzynski/AxiomAuditDriven.lean @@ -13,7 +13,9 @@ import CrooksJarzynski.MeasureProtocolMarkedEndpoints import CrooksJarzynski.ContinuousTimeJumpDrivenEndpointLaw import CrooksJarzynski.ContinuousTimeJumpDrivenEndpointExp import CrooksJarzynski.ContinuousTimeJumpDrivenGlobalCrooks +import CrooksJarzynski.ContinuousTimeJumpDrivenKL import CrooksJarzynski.ContinuousTimeJumpDrivenGlobalThreeStateTwoWindow +import CrooksJarzynski.ContinuousTimeJumpTrajectoryReversal /-! # Axiom audit for stepwise driven jump protocols @@ -110,5 +112,12 @@ headline list while subjecting both files to the same CI allowlist. #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.global_crooks_of_gibbsDetailedBalance #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.global_jarzynski_of_gibbsDetailedBalance #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.global_second_law_of_gibbsDetailedBalance +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.JumpPath.trajectory_reverse_eq_mirror +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FullPath.trajectory_reverse_eq_mirror +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_ae_trajectory_reverse_eq_mirror +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.map_trajectory_reverse_eq_map_mirror +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.reverseGlobalLaw_eq_forwardGlobalLaw_withDensity +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.llr_forwardGlobalLaw_reverseGlobalLaw +#print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.klDiv_forwardGlobalLaw_reverseGlobalLaw #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.ThreeStateTwoWindow.global_work_zero_atom_pos #print axioms CrooksJarzynski.MeasureProtocol.ContinuousTimeJump.Driven.ThreeStateTwoWindow.global_work_log_two_atom_pos diff --git a/CrooksJarzynski/ContinuousTimeJumpDrivenKL.lean b/CrooksJarzynski/ContinuousTimeJumpDrivenKL.lean new file mode 100644 index 0000000..0a0261f --- /dev/null +++ b/CrooksJarzynski/ContinuousTimeJumpDrivenKL.lean @@ -0,0 +1,233 @@ +/- +Copyright (c) 2026 kiyo-e. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: kiyo-e +-/ +import CrooksJarzynski.ContinuousTimeJumpDrivenGlobalCrooks +import Mathlib.InformationTheory.KullbackLeibler.Basic + +/-! +# Relative entropy of forward and reverse driven path laws + +The global Crooks density identifies the log-likelihood ratio of the forward +law with the dissipated work. Integrating that identity gives the equality +between mean entropy production and Kullback--Leibler divergence. +-/ + +open MeasureTheory ProbabilityTheory Function InformationTheory +open scoped ENNReal NNReal ProbabilityTheory + +namespace CrooksJarzynski +namespace MeasureProtocol +namespace ContinuousTimeJump +namespace Driven + +universe u + +variable {Ω : Type u} [Fintype Ω] +variable [MeasurableSpace Ω] [MeasurableSingletonClass Ω] +variable [DecidableEq Ω] [Nonempty Ω] + +omit [DecidableEq Ω] [Nonempty Ω] in +private theorem integrable_count_fintype_kl (f : Ω → ℝ) : + Integrable f (Measure.count : Measure Ω) := by + apply Integrable.of_bound + (Measurable.of_discrete : Measurable f).aestronglyMeasurable + (∑ x : Ω, ‖f x‖) + filter_upwards [] with x + exact Finset.single_le_sum (f := fun y : Ω => ‖f y‖) + (fun _ _ => norm_nonneg _) (Finset.mem_univ x) + +/-- A strictly positive exponential density has the expected +log-likelihood ratio against its base measure. -/ +private theorem llr_withDensity_exp_neg_mul + {α : Type*} [MeasurableSpace α] (μ : Measure α) [SigmaFinite μ] + (β : ℝ) (f : α → ℝ) (hf : Measurable f) : + llr μ (μ.withDensity fun x => ENNReal.ofReal (Real.exp (-β * f x))) =ᵐ[μ] + fun x => β * f x := by + let q : α → ℝ≥0∞ := fun x => ENNReal.ofReal (Real.exp (-β * f x)) + have hq : Measurable q := + ENNReal.measurable_ofReal.comp + (Real.measurable_exp.comp (measurable_const.mul hf)) + have hq0 : ∀ᵐ x ∂μ, q x ≠ 0 := ae_of_all _ fun x => by + simp [q, Real.exp_pos] + have hqtop : ∀ᵐ x ∂μ, q x ≠ ∞ := ae_of_all _ fun x => by simp [q] + have hrn := Measure.rnDeriv_withDensity_right μ μ + hq.aemeasurable hq0 hqtop + filter_upwards [hrn, μ.rnDeriv_self] with x hrn hself + rw [llr, hrn, hself] + simp only [mul_one, q] + rw [ENNReal.toReal_inv, ENNReal.toReal_ofReal (Real.exp_pos _).le, + Real.log_inv, Real.log_exp] + ring + +/-- The aligned reverse global law is the forward law tilted by the negative +dissipated work. -/ +theorem reverseGlobalLaw_eq_forwardGlobalLaw_withDensity + {M : ℕ} (β : ℝ) (hβ : β ≠ 0) + (energy : Fin (M + 1) → Ω → ℝ) + (generator : Fin M → FiniteJumpGenerator Ω) + (duration : Fin M → NNReal) + (hbalance : ∀ i, + (generator i).IsGibbsDetailedBalance β (energy i.castSucc)) : + reverseGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β + (energy (Fin.last M))) generator duration = + (forwardGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β (energy 0)) + generator duration).withDensity + (fun γ => ENNReal.ofReal (Real.exp (-β * + (globalWork energy duration γ - + deltaFreeEnergy (Measure.count : Measure Ω) β energy)))) := by + let forward := forwardGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β (energy 0)) generator duration + let reverse := reverseGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β (energy (Fin.last M))) + generator duration + let q : FullPath Ω → ℝ≥0∞ := fun γ => + ENNReal.ofReal (Real.exp (-β * globalWork energy duration γ)) + let c : ℝ≥0∞ := ENNReal.ofReal (Real.exp (-β * + deltaFreeEnergy (Measure.count : Measure Ω) β energy)) + let r : FullPath Ω → ℝ≥0∞ := fun γ => ENNReal.ofReal (Real.exp (-β * + (globalWork energy duration γ - + deltaFreeEnergy (Measure.count : Measure Ω) β energy))) + have hq : Measurable q := by + dsimp [q] + exact ENNReal.measurable_ofReal.comp + (Real.measurable_exp.comp + (measurable_const.mul + (measurable_globalWork energy duration fun _ => Measurable.of_discrete))) + have hc0 : c ≠ 0 := by simp [c, Real.exp_pos] + have hctop : c ≠ ∞ := by simp [c] + have hcrooks : forward.withDensity q = c • reverse := by + simpa [CrooksRelation, forward, reverse, q, c] using + global_crooks_of_gibbsDetailedBalance + β hβ energy generator duration hbalance + have hrq : c⁻¹ • q = r := by + funext γ + dsimp [q, c, r] + rw [← ENNReal.ofReal_inv_of_pos (Real.exp_pos _), ← ENNReal.ofReal_mul (by positivity), + ← Real.exp_neg, ← Real.exp_add] + congr 2 + ring + change reverse = forward.withDensity r + calc + reverse = c⁻¹ • (c • reverse) := by + rw [smul_smul, ENNReal.inv_mul_cancel hc0 hctop, one_smul] + _ = c⁻¹ • forward.withDensity q := by rw [hcrooks] + _ = forward.withDensity (c⁻¹ • q) := by + rw [MeasureTheory.withDensity_smul c⁻¹ hq] + _ = forward.withDensity r := by rw [hrq] + +/-- The forward-to-aligned-reverse log-likelihood ratio is the dimensionless +dissipated work. -/ +theorem llr_forwardGlobalLaw_reverseGlobalLaw + {M : ℕ} (β : ℝ) (hβ : β ≠ 0) + (energy : Fin (M + 1) → Ω → ℝ) + (generator : Fin M → FiniteJumpGenerator Ω) + (duration : Fin M → NNReal) + (hbalance : ∀ i, + (generator i).IsGibbsDetailedBalance β (energy i.castSucc)) : + llr + (forwardGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β (energy 0)) + generator duration) + (reverseGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β + (energy (Fin.last M))) generator duration) =ᵐ[ + forwardGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β (energy 0)) + generator duration] + fun γ => β * (globalWork energy duration γ - + deltaFreeEnergy (Measure.count : Measure Ω) β energy) := by + let initial := Gibbs.measure (Measure.count : Measure Ω) β (energy 0) + letI : IsProbabilityMeasure initial := + Gibbs.isProbabilityMeasure_measure + (Measure.count : Measure Ω) β (energy 0) + (integrable_count_fintype_kl + (fun x => Real.exp (-β * energy 0 x))) + rw [reverseGlobalLaw_eq_forwardGlobalLaw_withDensity + β hβ energy generator duration hbalance] + apply llr_withDensity_exp_neg_mul + exact (measurable_globalWork energy duration fun _ => Measurable.of_discrete).sub + measurable_const + +/-- **Mean entropy production equals path-space relative entropy.** -/ +theorem klDiv_forwardGlobalLaw_reverseGlobalLaw + {M : ℕ} (β : ℝ) (hβ : 0 < β) + (energy : Fin (M + 1) → Ω → ℝ) + (generator : Fin M → FiniteJumpGenerator Ω) + (duration : Fin M → NNReal) + (hbalance : ∀ i, + (generator i).IsGibbsDetailedBalance β (energy i.castSucc)) : + klDiv + (forwardGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β (energy 0)) + generator duration) + (reverseGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β + (energy (Fin.last M))) generator duration) = + ENNReal.ofReal (β * + (∫ γ, globalWork energy duration γ + ∂forwardGlobalLaw + (Gibbs.measure (Measure.count : Measure Ω) β (energy 0)) + generator duration - + deltaFreeEnergy (Measure.count : Measure Ω) β energy)) := by + let initial := Gibbs.measure (Measure.count : Measure Ω) β (energy 0) + let final := Gibbs.measure (Measure.count : Measure Ω) β (energy (Fin.last M)) + let forward := forwardGlobalLaw initial generator duration + let reverse := reverseGlobalLaw final generator duration + change klDiv forward reverse = ENNReal.ofReal (β * + (∫ γ, globalWork energy duration γ ∂forward - + deltaFreeEnergy (Measure.count : Measure Ω) β energy)) + letI : IsProbabilityMeasure initial := + Gibbs.isProbabilityMeasure_measure + (Measure.count : Measure Ω) β (energy 0) + (integrable_count_fintype_kl + (fun x => Real.exp (-β * energy 0 x))) + letI : IsProbabilityMeasure final := + Gibbs.isProbabilityMeasure_measure + (Measure.count : Measure Ω) β (energy (Fin.last M)) + (integrable_count_fintype_kl + (fun x => Real.exp (-β * energy (Fin.last M) x))) + have hreverseDensity := reverseGlobalLaw_eq_forwardGlobalLaw_withDensity + β hβ.ne' energy generator duration hbalance + change reverse = forward.withDensity + (fun γ => ENNReal.ofReal (Real.exp (-β * + (globalWork energy duration γ - + deltaFreeEnergy (Measure.count : Measure Ω) β energy)))) at hreverseDensity + have hac : forward ≪ reverse := by + rw [hreverseDensity] + apply withDensity_absolutelyContinuous' + · exact (ENNReal.measurable_ofReal.comp + (Real.measurable_exp.comp + (measurable_const.mul + ((measurable_globalWork energy duration + fun _ => Measurable.of_discrete).sub measurable_const)))).aemeasurable + · filter_upwards + simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le] + intro γ + positivity + have hwork : Integrable (globalWork energy duration) forward := + integrable_globalWork initial energy generator duration + have hllr := llr_forwardGlobalLaw_reverseGlobalLaw + β hβ.ne' energy generator duration hbalance + have hllrInt : Integrable (llr forward reverse) forward := by + rw [integrable_congr hllr] + exact (hwork.sub (integrable_const _)).const_mul β + rw [klDiv_of_ac_of_integrable hac hllrInt] + have hforwardMass : forward.real Set.univ = 1 := by simp + have hreverseMass : reverse.real Set.univ = 1 := by simp + rw [show ∫ γ, llr forward reverse γ ∂forward = + β * (∫ γ, globalWork energy duration γ ∂forward - + deltaFreeEnergy (Measure.count : Measure Ω) β energy) by + rw [integral_congr_ae hllr, integral_const_mul, + integral_sub hwork (integrable_const _), integral_const] + simp] + rw [hforwardMass, hreverseMass] + ring_nf + +end Driven +end ContinuousTimeJump +end MeasureProtocol +end CrooksJarzynski diff --git a/CrooksJarzynski/ContinuousTimeJumpFiniteDimensional.lean b/CrooksJarzynski/ContinuousTimeJumpFiniteDimensional.lean index 443d89b..973e38c 100644 --- a/CrooksJarzynski/ContinuousTimeJumpFiniteDimensional.lean +++ b/CrooksJarzynski/ContinuousTimeJumpFiniteDimensional.lean @@ -604,6 +604,137 @@ theorem map_pathLawFrom_trajectory_eq_transitionKernel Measure.map_congr (G.pathLawFrom_ae_trajectory_horizon t x) _ = G.transitionKernel t x := (G.transitionKernel_apply t x).symm +/-- The finite distribution represented by one row of the transition kernel. -/ +private noncomputable def transitionDistribution + (G : FiniteJumpGenerator Ω) (t : NNReal) (x : Ω) : + FiniteDistribution Ω where + prob y := (G.transitionKernel t x).real {y} + nonneg _ := measureReal_nonneg + sum_prob := by + calc + (∑ y, (G.transitionKernel t x).real {y}) = + (G.transitionKernel t x).real (Finset.univ : Finset Ω) := + sum_measureReal_singleton (Finset.univ : Finset Ω) + _ = (G.transitionKernel t x).real Set.univ := by simp + _ = 1 := by + rw [Measure.real_def, measure_univ, ENNReal.toReal_one] + +private theorem transitionDistribution_toMeasure + (G : FiniteJumpGenerator Ω) (t : NNReal) (x : Ω) : + (transitionDistribution G t x).toMeasure = G.transitionKernel t x := by + apply Measure.ext_of_singleton + intro y + rw [FiniteDistribution.toMeasure_singleton] + change ENNReal.ofReal ((G.transitionKernel t x).real {y}) = _ + rw [Measure.real_def, ENNReal.ofReal_toReal] + exact ne_of_lt measure_singleton_lt_top + +/-- **General finite-dimensional distributions.** Sampling the fixed-initial path law +at any monotone finite family of times, not necessarily starting at zero, gives the +chronological transition-kernel path measure started from the time-`time 0` marginal. -/ +theorem pathLawFrom_finiteDimensional_eq_general + (G : FiniteJumpGenerator Ω) (T : NNReal) (x : Ω) + {n : ℕ} (time : Fin (n + 1) → NNReal) + (hmono : Monotone time) (hT : time (Fin.last n) ≤ T) : + (G.pathLawFrom T x).map (FullPath.sampleAt time) = + Markov.chronologicalForwardPathMeasure (G.transitionKernel (time 0) x) + (fun i : Fin n => + G.transitionKernel (time i.succ - time i.castSucc)) := by + rw [G.map_pathLawFrom_sampleAt_horizon_le + (time (Fin.last n)) T hT x time le_rfl hmono] + induction n with + | zero => + let lift : Ω → Trajectory Ω 0 := + fun y => Trajectory.ofFn fun _ => y + have hlift : Measurable lift := by + apply Trajectory.measurable_ofFn.comp + exact measurable_pi_iff.2 fun _ => measurable_id + have hsample : + FullPath.sampleAt time = + lift ∘ fun γ : FullPath Ω => FullPath.trajectory γ (time 0) := by + funext γ + apply Trajectory.ext + intro i + simp only [FullPath.sampleAt, lift, Function.comp_apply, + Trajectory.stateAt_ofFn] + rw [Fin.eq_zero i] + rw [show time (Fin.last 0) = time 0 by rfl, hsample] + rw [← Measure.map_map hlift (FullPath.measurable_trajectory (time 0))] + rw [G.map_pathLawFrom_trajectory_eq_transitionKernel + (time 0) (time 0) le_rfl x] + let initial := transitionDistribution G (time 0) x + have hinitial : initial.toMeasure = G.transitionKernel (time 0) x := by + simpa [initial] using transitionDistribution_toMeasure G (time 0) x + rw [← hinitial] + have hforward : + (fun i : Fin 0 => + G.transitionKernel (time i.succ - time i.castSucc)) = + fun i : Fin 0 => MathlibBridge.toKernel (Fin.elim0 i) := by + funext i + exact Fin.elim0 i + rw [hforward] + apply Measure.ext_of_singleton + intro γ + rw [Measure.map_apply hlift (measurableSet_singleton γ)] + have hpre : lift ⁻¹' {γ} = {Trajectory.stateAt γ 0} := by + rcases γ with ⟨y, c⟩ + cases c + ext z + simp [lift, Trajectory.ofFn, Trajectory.stateAt] + rw [hpre, FiniteDistribution.toMeasure_singleton, + MathlibBridge.chronologicalForwardPathMeasure_singleton] + simp [transitionWeight] + | succ n ih => + let earlierTime : Fin (n + 1) → NNReal := fun i => time i.castSucc + have hmonoEarlier : Monotone earlierTime := fun _ _ hij => + hmono (Fin.castSucc_le_castSucc_iff.mpr hij) + have hTEarlier : earlierTime (Fin.last n) ≤ T := + (hmono (Fin.le_last (Fin.last n).castSucc)).trans hT + rw [G.map_pathLawFrom_sampleAt_succ x time hmono] + rw [ih earlierTime hmonoEarlier hTEarlier] + rw [Markov.chronologicalForwardPathMeasure_succ] + congr 2 + +/-- The atom of every general finite-dimensional marginal is the matrix-exponential +entry from the initial state times the product of matrix-exponential entries between +consecutive observation times. -/ +theorem pathLawFrom_sampleAt_real_singleton_eq_exp_product_general + (G : FiniteJumpGenerator Ω) (T : NNReal) (x : Ω) + {n : ℕ} (time : Fin (n + 1) → NNReal) + (hmono : Monotone time) (hT : time (Fin.last n) ≤ T) (γ : Trajectory Ω n) : + ((G.pathLawFrom T x).map (FullPath.sampleAt time)).real {γ} = + NormedSpace.exp (((time 0 : NNReal) : ℝ) • G.generator) x + (Trajectory.stateAt γ 0) * + ∏ i : Fin n, + NormedSpace.exp + ((((time i.succ - time i.castSucc) : NNReal) : ℝ) • G.generator) + (Trajectory.stateAt γ i.castSucc) (Trajectory.stateAt γ i.succ) := by + let initial := transitionDistribution G (time 0) x + let K : Fin n → CrooksJarzynski.Kernel Ω := fun i y => + transitionDistribution G (time i.succ - time i.castSucc) y + have hinitial : initial.toMeasure = G.transitionKernel (time 0) x := by + simpa [initial] using transitionDistribution_toMeasure G (time 0) x + have hK (i : Fin n) : + MathlibBridge.toKernel (K i) = + G.transitionKernel (time i.succ - time i.castSucc) := by + apply ProbabilityTheory.Kernel.ext + intro y + rw [MathlibBridge.toKernel_apply] + simpa [K] using transitionDistribution_toMeasure G + (time i.succ - time i.castSucc) y + rw [G.pathLawFrom_finiteDimensional_eq_general T x time hmono hT] + rw [← hinitial] + simp_rw [← hK] + rw [Measure.real_def, + MathlibBridge.chronologicalForwardPathMeasure_singleton] + rw [ENNReal.toReal_ofReal + (mul_nonneg (initial.nonneg γ.1) (transitionWeight_nonneg K γ.1 γ.2))] + rw [Trajectory.transitionWeight_eq_transitionProduct] + simp only [Trajectory.transitionProduct, K, initial, + transitionDistribution] + simp_rw [G.transitionKernel_real_singleton_eq_exp_generator] + rw [Trajectory.stateAt_zero] + /-- The mass of observing a state at any time before the path horizon is the corresponding entry of the matrix exponential. -/ theorem pathLawFrom_trajectory_real_singleton_eq_exp_generator diff --git a/CrooksJarzynski/ContinuousTimeJumpTrajectoryReversal.lean b/CrooksJarzynski/ContinuousTimeJumpTrajectoryReversal.lean new file mode 100644 index 0000000..76c9322 --- /dev/null +++ b/CrooksJarzynski/ContinuousTimeJumpTrajectoryReversal.lean @@ -0,0 +1,339 @@ +/- +Copyright (c) 2026 kiyo-e. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: kiyo-e +-/ +import CrooksJarzynski.ContinuousTimeJumpConcatLaw +import CrooksJarzynski.ContinuousTimeJumpFullPathReversal + +/-! +# Real-time trajectories under path reversal + +Record reversal agrees with physical time reversal away from jump times. The +pointwise statement includes the exact-horizon condition carried almost surely +by the finite-generator path law; `IsValid` alone only says that the terminal +state has been reached by the horizon. +-/ + +open MeasureTheory +open scoped ENNReal + +namespace CrooksJarzynski +namespace MeasureProtocol +namespace ContinuousTimeJump + +universe u + +namespace JumpPath + +variable {Ω : Type u} + +/-- Rewrite a partial sum over `Fin` as a sum over a natural-number range. -/ +private theorem sum_Iio_eq_sum_range {k : ℕ} (a : Fin k) (f : Fin k → ℝ) : + (∑ i ∈ Finset.Iio a, f i) = + ∑ r ∈ Finset.range a.val, if hr : r < k then f ⟨r, hr⟩ else 0 := by + have ha : a.val < k := a.isLt + apply Finset.sum_bij (fun i _ => i.val) + · intro i hi + exact Finset.mem_range.mpr (by simpa using (Finset.mem_Iio.mp hi)) + · intro i _ j _ h + exact Fin.ext h + · intro r hr + have hrlt : r < a.val := Finset.mem_range.mp hr + have hrk : r < k := lt_trans hrlt ha + refine ⟨⟨r, hrk⟩, Finset.mem_Iio.mpr ?_, rfl⟩ + simpa [Fin.lt_def] using hrlt + · intro i hi + rw [dif_pos i.isLt] + +/-- Remove the initial state and holding interval from a path with at least one +jump. -/ +def dropFirst {n : ℕ} (γ : JumpPath Ω (n + 1)) : JumpPath Ω n := + (fun i => γ.1 i.succ, fun i => γ.2 i.succ) + +/-- The first holding interval followed by the jump times of `dropFirst` +recovers the noninitial jump times of the original path. -/ +theorem jumpTimes_succ_eq {n : ℕ} (γ : JumpPath Ω (n + 1)) + (k : Fin (n + 1)) : + jumpTimes γ k.succ = (γ.2 0 : ℝ) + jumpTimes (dropFirst γ) k := by + unfold jumpTimes dropFirst + rw [sum_Iio_eq_sum_range (a := k.succ), sum_Iio_eq_sum_range (a := k)] + change + (∑ r ∈ Finset.range (k.val + 1), + if hr : r < n + 2 then (γ.2 ⟨r, hr⟩ : ℝ) else 0) = _ + rw [Finset.sum_range_succ'] + rw [add_comm] + congr 1 + apply Finset.sum_congr rfl + intro i hi + simp only [Finset.mem_range] at hi + rw [dif_pos (by omega : i + 1 < n + 2), dif_pos (by omega : i < n + 1)] + rfl + +/-- Dropping the first interval after reversing is the reversal of dropping the +last interval. -/ +@[simp] +theorem dropFirst_reverse {n : ℕ} (γ : JumpPath Ω (n + 1)) : + dropFirst (reverse γ) = reverse (dropLast γ) := by + apply Prod.ext <;> funext i + · simp only [dropFirst, reverse, dropLast, Fin.rev_succ] + · simp only [dropFirst, reverse, dropLast, Fin.rev_succ] + +/-- Dropping the first and last intervals commutes. -/ +@[simp] +theorem dropFirst_dropLast {n : ℕ} (γ : JumpPath Ω (n + 2)) : + dropFirst (dropLast γ) = dropLast (dropFirst γ) := by + rfl + +/-- Before the first jump, the trajectory occupies its initial state. -/ +theorem trajectory_eq_initial_of_lt_first : ∀ {n : ℕ} + (γ : JumpPath Ω (n + 1)) (t : ℝ), + 0 ≤ t → t < γ.2 0 → trajectory γ t = γ.1 0 + | 0, γ, t, _, ht => by + simp only [trajectory] + rw [if_neg] + · rfl + · rw [show jumpTimes γ (Fin.last 1) = (γ.2 0 : ℝ) by + unfold jumpTimes + rw [sum_Iio_eq_sum_range] + simp] + exact not_le.mpr ht + | n + 1, γ, t, ht0, ht => by + rw [trajectory] + have hlast : ¬ jumpTimes γ (Fin.last (n + 2)) ≤ t := by + apply not_le.mpr + calc + t < (γ.2 0 : ℝ) := ht + _ = jumpTimes γ (1 : Fin (n + 3)) := by + unfold jumpTimes + rw [sum_Iio_eq_sum_range] + simp + _ ≤ jumpTimes γ (Fin.last (n + 2)) := + jumpTimes_mono γ (by + apply Fin.le_last) + rw [if_neg hlast] + exact trajectory_eq_initial_of_lt_first (dropLast γ) t ht0 ht + +/-- After the first holding interval, deleting that interval and shifting the +clock does not change the trajectory. -/ +theorem trajectory_dropFirst : ∀ {n : ℕ} (γ : JumpPath Ω (n + 1)) + (t : ℝ), (γ.2 0 : ℝ) ≤ t → + trajectory γ t = trajectory (dropFirst γ) (t - (γ.2 0 : ℝ)) + | 0, γ, t, ht => by + simp only [trajectory, dropFirst] + rw [if_pos (by + rw [show jumpTimes γ (Fin.last 1) = (γ.2 0 : ℝ) by + unfold jumpTimes + rw [sum_Iio_eq_sum_range] + simp] + exact ht)] + apply congrArg γ.1 + apply Fin.ext + simp + | n + 1, γ, t, ht => by + have htime := jumpTimes_succ_eq γ (Fin.last (n + 1)) + have hlast : Fin.last (n + 2) = (Fin.last (n + 1)).succ := by + apply Fin.ext + simp + change + (if jumpTimes γ (Fin.last (n + 2)) ≤ t then + γ.1 (Fin.last (n + 2)) + else trajectory (dropLast γ) t) = + (if jumpTimes (dropFirst γ) (Fin.last (n + 1)) ≤ + t - (γ.2 0 : ℝ) then + (dropFirst γ).1 (Fin.last (n + 1)) + else trajectory (dropLast (dropFirst γ)) + (t - (γ.2 0 : ℝ))) + rw [hlast, htime] + by_cases h : jumpTimes (dropFirst γ) (Fin.last (n + 1)) ≤ + t - (γ.2 0 : ℝ) + · rw [if_pos (by linarith), if_pos h] + rfl + · rw [if_neg (by intro h'; exact h (by linarith)), if_neg h, + ← dropFirst_dropLast] + exact trajectory_dropFirst (dropLast γ) t ht + +/-- The last jump time is the total holding time of the chart with its terminal +interval removed. -/ +theorem jumpTimes_last_eq_totalHoldingTime_dropLast {n : ℕ} + (γ : JumpPath Ω (n + 1)) : + jumpTimes γ (Fin.last (n + 1)) = + (totalHoldingTime (dropLast γ) : ℝ) := by + unfold jumpTimes totalHoldingTime dropLast + rw [NNReal.coe_sum, Finset.sum_fin_eq_sum_range, + sum_Iio_eq_sum_range] + apply Finset.sum_congr rfl + intro i hi + simp only [Finset.mem_range] at hi + rw [dif_pos (by omega : i < n + 2), dif_pos (by omega : i < n + 1)] + rfl + +/-- Removing the terminal interval splits the total holding time into the +remaining prefix and that terminal interval. -/ +theorem totalHoldingTime_dropLast_add_last {n : ℕ} + (γ : JumpPath Ω (n + 1)) : + totalHoldingTime (dropLast γ) + γ.2 (Fin.last (n + 1)) = + totalHoldingTime γ := by + unfold totalHoldingTime dropLast + exact (Fin.sum_univ_castSucc (fun i => γ.2 i)).symm + +/-- **Pointwise physical time reversal.** On an exact-horizon valid chart, +record reversal evaluates at the mirrored time whenever the mirrored time is +not a noninitial jump time of the original chart. -/ +theorem trajectory_reverse_eq_mirror : ∀ {n : ℕ} {T : NNReal} + (γ : JumpPath Ω n) (_hvalid : IsValid T γ) + (_htotal : totalHoldingTime γ = T) (t : ℝ) + (_ht0 : 0 ≤ t) (_htT : t ≤ T) + (_hnot : ∀ k : Fin n, jumpTimes γ k.succ ≠ (T : ℝ) - t), + trajectory (reverse γ) t = trajectory γ ((T : ℝ) - t) + | 0, _, γ, _, _, _, _, _, _ => by + simp [trajectory, reverse] + | n + 1, T, γ, hvalid, htotal, t, ht0, htT, hnot => by + let pre := dropLast γ + let terminalHolding := γ.2 (Fin.last (n + 1)) + have hsplit : pre.totalHoldingTime + terminalHolding = T := by + rw [totalHoldingTime_dropLast_add_last] + exact htotal + have hsplitReal : (pre.totalHoldingTime : ℝ) + + (terminalHolding : ℝ) = (T : ℝ) := by + exact_mod_cast hsplit + have hjump : jumpTimes γ (Fin.last (n + 1)) = + (pre.totalHoldingTime : ℝ) := + jumpTimes_last_eq_totalHoldingTime_dropLast γ + have hne : (T : ℝ) - t ≠ (pre.totalHoldingTime : ℝ) := by + intro h + apply hnot (Fin.last n) + simpa [hjump] using h.symm + rcases lt_or_gt_of_ne hne with hbefore | hafter + · have htshift : (terminalHolding : ℝ) ≤ t := by + linarith + rw [trajectory_dropFirst (reverse γ) t (by simpa [reverse] using htshift), + dropFirst_reverse] + have hpreValid : IsValid pre.totalHoldingTime pre := by + refine ⟨?_, jumpTimes_le_totalHoldingTime pre _⟩ + intro i + exact hvalid.1 i.castSucc + have htshift0 : 0 ≤ t - (terminalHolding : ℝ) := sub_nonneg.mpr htshift + have htshiftT : t - (terminalHolding : ℝ) ≤ pre.totalHoldingTime := by + linarith + have hmirror : (pre.totalHoldingTime : ℝ) - + (t - (terminalHolding : ℝ)) = (T : ℝ) - t := by + linarith + have hpreNot : ∀ k : Fin n, + jumpTimes pre k.succ ≠ + (pre.totalHoldingTime : ℝ) - + (t - (terminalHolding : ℝ)) := by + intro k hk + apply hnot k.castSucc + rw [← hmirror, ← hk, jumpTimes_dropLast] + rfl + change trajectory (reverse pre) (t - (terminalHolding : ℝ)) = + trajectory γ ((T : ℝ) - t) + rw [trajectory_reverse_eq_mirror pre hpreValid rfl + (t - (terminalHolding : ℝ)) htshift0 htshiftT hpreNot, + hmirror] + change trajectory (dropLast γ) ((T : ℝ) - t) = + (if jumpTimes γ (Fin.last (n + 1)) ≤ (T : ℝ) - t then + γ.1 (Fin.last (n + 1)) + else trajectory (dropLast γ) ((T : ℝ) - t)) + rw [if_neg (by rw [hjump]; exact not_le.mpr hbefore)] + · have hterminal : trajectory γ ((T : ℝ) - t) = + γ.1 (Fin.last (n + 1)) := by + exact trajectory_eq_terminal_of_last_le γ _ (by rw [hjump]; exact hafter.le) + have htlt : t < (terminalHolding : ℝ) := by + linarith + have hreverseInitial : trajectory (reverse γ) t = + (reverse γ).1 0 := + trajectory_eq_initial_of_lt_first (reverse γ) t ht0 (by + simpa [reverse] using htlt) + rw [hterminal, hreverseInitial] + simp [reverse] + +end JumpPath + +namespace FullPath + +variable {Ω : Type u} + +/-- **Pointwise physical time reversal for complete paths.** An exact-horizon +valid complete path agrees with its mirrored trajectory at every deterministic +time whose mirror is not a jump time. -/ +theorem trajectory_reverse_eq_mirror {T : NNReal} (γ : FullPath Ω) + (hvalid : IsValid T γ) (htotal : totalHoldingTime γ = T) + (t : NNReal) (ht : t ≤ T) (hnot : ¬ HasJumpAt (T - t) γ) : + trajectory (reverse γ) t = trajectory γ (T - t) := by + rcases γ with ⟨n, γ⟩ + apply JumpPath.trajectory_reverse_eq_mirror γ hvalid htotal t + (by positivity) (by exact_mod_cast ht) + intro k hk + apply hnot + refine ⟨k, ?_⟩ + rw [NNReal.coe_sub ht] + exact hk + +end FullPath + +namespace FiniteJumpGenerator + +variable {Ω : Type u} [Fintype Ω] [DecidableEq Ω] +variable [MeasurableSpace Ω] [MeasurableSingletonClass Ω] + +omit [MeasurableSingletonClass Ω] in +/-- At every fixed time, sector-law record reversal agrees almost surely with +physical time reversal. -/ +theorem sectorLawFrom_ae_trajectory_reverse_eq_mirror + (G : FiniteJumpGenerator Ω) (T : NNReal) (x : Ω) (n : ℕ) + (t : NNReal) (ht : t ≤ T) : + (fun γ => JumpPath.trajectory (JumpPath.reverse γ) t) =ᵐ[G.sectorLawFrom T x n] + fun γ => JumpPath.trajectory γ (T - t) := by + filter_upwards [G.sectorLawFrom_ae_isValid T x n, + G.sectorLawFrom_ae_totalHoldingTime T x n, + G.sectorLawFrom_ae_noJumpAt T x n (T - t)] with γ hvalid htotal hnot + apply JumpPath.trajectory_reverse_eq_mirror γ hvalid htotal t + (by positivity) (by exact_mod_cast ht) + intro k hk + apply hnot + refine ⟨k, ?_⟩ + rw [NNReal.coe_sub ht] + exact hk + +omit [MeasurableSingletonClass Ω] in +/-- **Almost-sure physical time reversal.** At a fixed observation time, +record reversal under the normalized fixed-initial path law realizes the +mirrored real-time trajectory. -/ +theorem pathLawFrom_ae_trajectory_reverse_eq_mirror + (G : FiniteJumpGenerator Ω) (T : NNReal) (x : Ω) + (t : NNReal) (ht : t ≤ T) : + (fun γ => FullPath.trajectory (FullPath.reverse γ) t) =ᵐ[G.pathLawFrom T x] + fun γ => FullPath.trajectory γ (T - t) := by + filter_upwards [G.pathLawFrom_ae_isValid T x, + G.pathLawFrom_ae_totalHoldingTime T x, + (show ∀ᵐ γ ∂G.pathLawFrom T x, ¬ FullPath.HasJumpAt (T - t) γ by + simpa [tsub_add_cancel_of_le ht] using + G.pathLawFrom_ae_noJumpAt (T - t) t x)] with γ hvalid htotal hnot + exact FullPath.trajectory_reverse_eq_mirror γ hvalid htotal t ht hnot + +omit [MeasurableSingletonClass Ω] in +/-- **Finite-dimensional physical time reversal.** Joint evaluation of +record-reversed paths has the same law as joint evaluation of the original +paths at the mirrored deterministic times. -/ +theorem map_trajectory_reverse_eq_map_mirror + (G : FiniteJumpGenerator Ω) (T : NNReal) (x : Ω) {k : ℕ} + (time : Fin k → NNReal) (_hmono : Monotone time) + (htime : ∀ i, time i ≤ T) : + (G.pathLawFrom T x).map + (fun γ i => FullPath.trajectory (FullPath.reverse γ) (time i)) = + (G.pathLawFrom T x).map + (fun γ i => FullPath.trajectory γ (T - time i)) := by + apply Measure.map_congr + apply (ae_all_iff.2 fun i => + G.pathLawFrom_ae_trajectory_reverse_eq_mirror T x (time i) (htime i)).mono + intro γ hγ + funext i + exact hγ i + +end FiniteJumpGenerator + +end ContinuousTimeJump +end MeasureProtocol +end CrooksJarzynski diff --git a/CrooksJarzynski/ContinuousTimeJumpTwoStateInteriorTime.lean b/CrooksJarzynski/ContinuousTimeJumpTwoStateInteriorTime.lean new file mode 100644 index 0000000..397e410 --- /dev/null +++ b/CrooksJarzynski/ContinuousTimeJumpTwoStateInteriorTime.lean @@ -0,0 +1,161 @@ +/- +Copyright (c) 2026 kiyo-e. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: kiyo-e +-/ +import CrooksJarzynski.ContinuousTimeJumpFiniteDimensional +import CrooksJarzynski.ContinuousTimeJumpTwoStateFiniteGenerator +import CrooksJarzynski.ContinuousTimeJumpTwoStateGenerator + +/-! +# Interior-time non-determination for the two-state chain + +This is the interior-time companion of the endpoint-nondetermination theorem +for driven work. It shows that a window's boundary pair does not determine the +real-time trajectory inside the window, so retaining complete window paths is +essential for path-level observables. +-/ + +open MeasureTheory ProbabilityTheory +open scoped BigOperators ENNReal ProbabilityTheory + +namespace CrooksJarzynski +namespace MeasureProtocol +namespace ContinuousTimeJump +namespace TwoState + +/-- Every explicit transition probability of the symmetric two-state chain is +strictly positive at a positive time. -/ +theorem transitionProbability_pos (t : ℝ) (ht : 0 < t) (x y : State) : + 0 < transitionProbability t x y := by + unfold transitionProbability + split_ifs + · positivity + · have hexp : Real.exp (-2 * t) < 1 := by + rw [← Real.exp_zero] + exact Real.exp_lt_exp.mpr (by linarith) + positivity + +/-- Both possible states at the interior observation time have positive mass +when the path starts and ends at `State.zero`. -/ +theorem interior_event_pos (T : NNReal) (hT : 0 < T) (y : State) : + let time : Fin 3 → NNReal := ![0, T / 2, T] + let γy : Trajectory State 2 := + Trajectory.ofFn ![State.zero, y, State.zero] + 0 < (finiteGenerator.pathLawFrom T State.zero) + (FullPath.sampleAt time ⁻¹' {γy}) := by + let time : Fin 3 → NNReal := ![0, T / 2, T] + let γy : Trajectory State 2 := + Trajectory.ofFn ![State.zero, y, State.zero] + have hhalf : 0 < T / 2 := div_pos hT (by norm_num) + have hhalfReal : 0 < ((T / 2 : NNReal) : ℝ) := by + exact_mod_cast hhalf + have hhalfReal' : 0 < (T : ℝ) / 2 := by + simpa using hhalfReal + have hsecondHalf : (T : ℝ) - (T : ℝ) / 2 = (T : ℝ) / 2 := by + ring + have hmono : Monotone time := by + intro i j hij + fin_cases i <;> fin_cases j <;> simp_all [time] + have hzero : time 0 = 0 := by simp [time] + have hlast : time (Fin.last 2) ≤ T := by simp [time] + have hreal : + 0 < ((finiteGenerator.pathLawFrom T State.zero).map + (FullPath.sampleAt time)).real {γy} := by + rw [FiniteJumpGenerator.pathLawFrom_sampleAt_real_singleton_eq_exp_product + finiteGenerator T State.zero time hmono hzero hlast γy] + simp [γy, time, Trajectory.ofFn, Fin.prod_univ_two, + finiteGenerator_generator_eq, exp_smul_generator_apply] + rw [hsecondHalf] + exact mul_pos + (transitionProbability_pos ((T : ℝ) / 2) hhalfReal' State.zero y) + (transitionProbability_pos ((T : ℝ) / 2) hhalfReal' y State.zero) + change 0 < (finiteGenerator.pathLawFrom T State.zero) + (FullPath.sampleAt time ⁻¹' {γy}) + rw [← Measure.map_apply (FullPath.measurable_sampleAt time) + (measurableSet_singleton γy)] + exact pos_iff_ne_zero.mpr fun hzeroMeasure => by + rw [Measure.real_def, hzeroMeasure] at hreal + simp at hreal + +/-- On a positive interior-state event, an almost-everywhere endpoint +representation must take the pinned endpoint pair to that interior state. -/ +private theorem ae_endpoint_pair_value (T : NNReal) (hT : 0 < T) (y : State) + (f : State → State → State) + (hf : (fun γ => FullPath.trajectory γ ((T / 2 : NNReal) : ℝ)) + =ᵐ[finiteGenerator.pathLawFrom T State.zero] + (fun γ => f (FullPath.initialState γ) (FullPath.terminalState γ))) : + f State.zero State.zero = y := by + let μ := finiteGenerator.pathLawFrom T State.zero + let time : Fin 3 → NNReal := ![0, T / 2, T] + let γy : Trajectory State 2 := + Trajectory.ofFn ![State.zero, y, State.zero] + let event : Set (FullPath State) := FullPath.sampleAt time ⁻¹' {γy} + let good : FullPath State → Prop := fun γ => + FullPath.trajectory γ ((T / 2 : NNReal) : ℝ) = + f (FullPath.initialState γ) (FullPath.terminalState γ) ∧ + FullPath.initialState γ = State.zero ∧ + FullPath.trajectory γ (T : ℝ) = FullPath.terminalState γ + have hgoodAE : ∀ᵐ γ ∂μ, good γ := by + filter_upwards [hf, + finiteGenerator.pathLawFrom_ae_initialState T State.zero, + finiteGenerator.pathLawFrom_ae_trajectory_horizon T State.zero] with + γ hfunction hinitial hterminal + exact ⟨hfunction, hinitial, hterminal⟩ + have hnull : μ {γ | ¬ good γ} = 0 := by + rw [← ae_iff] + exact hgoodAE + have hevent : 0 < μ event := by + exact interior_event_pos T hT y + have hnonempty : (event \ {γ | ¬ good γ}).Nonempty := by + exact MeasureTheory.nonempty_of_measure_ne_zero + (by + rw [show μ (event \ {γ | ¬ good γ}) = μ event by + apply measure_sdiff_null' + exact measure_mono_null Set.inter_subset_right hnull] + exact ne_of_gt hevent) + rcases hnonempty with ⟨γ, hγevent, hγgood⟩ + have hgood : good γ := by + by_contra h + exact hγgood (by simpa using h) + change + FullPath.trajectory γ ((T / 2 : NNReal) : ℝ) = + f (FullPath.initialState γ) (FullPath.terminalState γ) ∧ + FullPath.initialState γ = State.zero ∧ + FullPath.trajectory γ (T : ℝ) = FullPath.terminalState γ at hgood + have hsample : FullPath.sampleAt time γ = γy := by + simpa [event] using hγevent + have hsampleAt (i : Fin 3) : + FullPath.trajectory γ (time i) = Trajectory.stateAt γy i := by + have h := congrFun (congrArg Trajectory.stateAt hsample) i + simpa only [FullPath.sampleAt, Trajectory.stateAt_ofFn] using h + have hmiddle : + FullPath.trajectory γ ((T / 2 : NNReal) : ℝ) = y := by + simpa [time, γy] using hsampleAt (1 : Fin 3) + have hend : FullPath.trajectory γ (T : ℝ) = State.zero := by + simpa [time, γy] using hsampleAt (2 : Fin 3) + have hterminal : FullPath.terminalState γ = State.zero := + hgood.2.2.symm.trans hend + rw [hgood.2.1, hterminal] at hgood + exact hgood.1.symm.trans hmiddle + +/-- **The real-time state at the window interior is not almost surely a +function of the path's initial and terminal states.** -/ +theorem trajectory_interior_not_ae_endpointFunction + (T : NNReal) (hT : 0 < T) : + ¬ ∃ f : State → State → State, + (fun γ => FullPath.trajectory γ ((T / 2 : NNReal) : ℝ)) + =ᵐ[finiteGenerator.pathLawFrom T State.zero] + (fun γ => f (FullPath.initialState γ) (FullPath.terminalState γ)) := by + rintro ⟨f, hf⟩ + have hzero : f State.zero State.zero = State.zero := + ae_endpoint_pair_value T hT State.zero f hf + have hone : f State.zero State.zero = State.one := + ae_endpoint_pair_value T hT State.one f hf + have : State.zero = State.one := hzero.symm.trans hone + cases this + +end TwoState +end ContinuousTimeJump +end MeasureProtocol +end CrooksJarzynski diff --git a/FORMALIZATION.md b/FORMALIZATION.md index 1a8bafa..1de1255 100644 --- a/FORMALIZATION.md +++ b/FORMALIZATION.md @@ -131,8 +131,10 @@ change-of-variables lemmas above expose this as a reusable public API in | Path-level Chapman--Kolmogorov in kernel form | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathKernel_add` | | The transition-kernel semigroup law recovered from path-level concatenation | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.transitionKernel_add_from_pathLawFrom_add` | | Every finite-dimensional marginal is the chronological path measure of the transition kernels | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_finiteDimensional_eq` | +| Every general finite-dimensional marginal, without a time-zero assumption, is the chronological path measure started from its first observed marginal | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_finiteDimensional_eq_general` | | Every single-time marginal is the corresponding transition-kernel row | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.map_pathLawFrom_trajectory_eq_transitionKernel` | | Every finite-dimensional atom is a product of matrix-exponential entries | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_sampleAt_real_singleton_eq_exp_product` | +| Every general finite-dimensional atom, without a time-zero assumption, starts with the matrix-exponential entry to its first observed state | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_sampleAt_real_singleton_eq_exp_product_general` | | Every single-time atom is the corresponding matrix-exponential entry | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_trajectory_real_singleton_eq_exp_generator` | A `FiniteJumpGenerator` packages nonnegative finite-state jump rates into a @@ -198,6 +200,12 @@ atom with a product of matrix-exponential entries. | Conventional global atomwise ratio `P_F(W=w) = e^{β(w-ΔF)} P_R(W_R=-w)` | `MeasureProtocol.ContinuousTimeJump.Driven.global_crooks_work_atom_of_gibbsDetailedBalance` | | Jarzynski equality for global trajectory work | `MeasureProtocol.ContinuousTimeJump.Driven.global_jarzynski_of_gibbsDetailedBalance` | | Average-work second law for global trajectory work | `MeasureProtocol.ContinuousTimeJump.Driven.global_second_law_of_gibbsDetailedBalance` | +| Pointwise cadlag time-reversal mirror on exact-horizon records | `MeasureProtocol.ContinuousTimeJump.JumpPath.trajectory_reverse_eq_mirror`, `MeasureProtocol.ContinuousTimeJump.FullPath.trajectory_reverse_eq_mirror` | +| Almost-sure fixed-time mirror under the normalized fixed-initial law | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.pathLawFrom_ae_trajectory_reverse_eq_mirror` | +| Finite-dimensional time-reversal mirror of the windowed path law | `MeasureProtocol.ContinuousTimeJump.FiniteJumpGenerator.map_trajectory_reverse_eq_map_mirror` | +| Aligned reverse global law as the dissipation-tilted forward law | `MeasureProtocol.ContinuousTimeJump.Driven.reverseGlobalLaw_eq_forwardGlobalLaw_withDensity` | +| Log-likelihood ratio equals dimensionless dissipated work | `MeasureProtocol.ContinuousTimeJump.Driven.llr_forwardGlobalLaw_reverseGlobalLaw` | +| Mean entropy production equals path-space relative entropy | `MeasureProtocol.ContinuousTimeJump.Driven.klDiv_forwardGlobalLaw_reverseGlobalLaw` | | One-window work is the terminal energy quench | `MeasureProtocol.ContinuousTimeJump.Driven.work_one` | | Reverse work observable is the negated forward work | `MeasureProtocol.ContinuousTimeJump.Driven.reverseWork_eq_neg` | | Work-distribution Crooks relation for driven protocols | `MeasureProtocol.ContinuousTimeJump.Driven.work_distribution_crooks_of_gibbsDetailedBalance` | diff --git a/PAPER.md b/PAPER.md new file mode 100644 index 0000000..43340b9 --- /dev/null +++ b/PAPER.md @@ -0,0 +1,46 @@ +# Paper and publication package + +The continuous-time paper is organized around one deliberately scoped contribution: + +> finite-state generator -> normalized fixed-horizon path measure -> finite-horizon sector-tail non-explosion -> actual terminal and finite-dimensional marginals -> measurable global driven path law -> physical Crooks--Jarzynski relations. + +The individual physical identities and standard CTMC constructions are classical. The paper contribution is the machine-checked connection between these layers for one explicitly constructed family of probability laws. + +## Start here + +- [`paper/main.tex`](paper/main.tex) is the full manuscript draft. +- [`paper/references.bib`](paper/references.bib) contains the manuscript bibliography. +- [`RELATED_WORK.md`](RELATED_WORK.md) records the literature comparison, safe novelty language, and bounded search statement. +- [`ARTIFACT.md`](ARTIFACT.md) gives a reviewer-oriented six-stage theorem route through the Lean development. +- [`FORMALIZATION.md`](FORMALIZATION.md) is the complete paper-level-to-Lean declaration map. +- [`DRIVEN_PROTOCOL.md`](DRIVEN_PROTOCOL.md) documents the driven protocol and global path-law design. + +## Paper direction + +The recommended title is: + +> **Machine-Checked Path Measures and Fluctuation Relations for Finite-State Continuous-Time Jump Processes in Lean 4** + +The paper does not claim the first mechanized CTMC, the first Lean trajectory measure, the first machine-checked non-explosion theorem, or the first Lean fluctuation theorem. It claims an end-to-end construction for finite-state, finite-horizon jump processes and finitely many piecewise-constant protocol windows. + +General calendar-time-dependent hazards, countably infinite state spaces, diffusions, Langevin dynamics, and SDE path measures are outside the current scope. + +## Build the manuscript + +A TeX Live installation with `latexmk` and `biber` is sufficient: + +```bash +cd paper +make +``` + +The generated PDF and LaTeX auxiliary files are ignored by Git. The Lean artifact itself is built independently with: + +```bash +lake exe cache get +lake build +``` + +## Publication checklist + +Before submission, freeze a green versioned release, archive it with a persistent identifier, replace the draft author metadata and artifact baseline, and re-audit the fixed Ripple and PhysicsAI snapshots recorded in [`RELATED_WORK.md`](RELATED_WORK.md). diff --git a/README.md b/README.md index 3dd2391..3dd3c49 100644 --- a/README.md +++ b/README.md @@ -39,6 +39,15 @@ physical laws: Crooks' relation and Jarzynski's equality are established results. Claims of priority for the formalization itself are intentionally left to a separate literature review. +## Paper + +A manuscript draft for the continuous-time core lives in +[`paper/`](paper/); [`PAPER.md`](PAPER.md) is the entry point to the +publication package, [`ARTIFACT.md`](ARTIFACT.md) gives reviewers a six-stage +theorem route through the Lean development, and +[`RELATED_WORK.md`](RELATED_WORK.md) records the literature comparison behind +the paper's positioning statement. + ## Main results The library proves: diff --git a/RELATED_WORK.md b/RELATED_WORK.md new file mode 100644 index 0000000..a4fedbd --- /dev/null +++ b/RELATED_WORK.md @@ -0,0 +1,107 @@ +# Related work and positioning + +- Review completed: 2026-08-26; final quality check: 2026-08-27. +- CrooksJarzynskiLean core-formalization baseline: [`efbf55e`](https://github.com/kiyo-e/CrooksJarzynskiLean/commit/efbf55ea2876fe016df8d64b25a661a7394b6464). The manuscript sources and the interior-time theorem live in the artifact commit that extends this baseline; a release replaces both references with a single versioned artifact tag. +- Intended audience: researchers in stochastic thermodynamics, probability, and interactive theorem proving. + +## Positioning in one sentence + +CrooksJarzynskiLean contributes an end-to-end Lean 4 construction that starts from finite-state jump generators, builds normalized fixed-horizon path measures, identifies their actual terminal and finite-dimensional laws with the matrix-exponential semigroup, and transports windowwise Gibbs detailed balance through finitely many piecewise-constant windows to global Crooks--Jarzynski relations. + +The fluctuation relations, finite-state CTMC theory, and jump-path densities are classical. The contribution is the machine-checked connection between them. + +## What is and is not claimed + +A safe paper statement is: + +> We present an end-to-end Lean 4 construction that starts from finite-state jump generators, builds normalized finite-horizon path measures, identifies their terminal and finite-dimensional laws with the matrix-exponential semigroup, and transports windowwise Gibbs detailed balance through finitely many piecewise-constant protocol windows to global Crooks--Jarzynski relations. + +The following priority claims are intentionally avoided: + +- first formalization of continuous-time Markov chains; +- first Lean CTMC or jump-and-hold path law; +- first machine-checked proof of non-explosion; +- first Lean trajectory measure; +- first formalization of thermodynamics or statistical mechanics in Lean; +- first Lean fluctuation theorem, Crooks relation, Jarzynski identity, or second-law consequence; and +- first rigorous Markov-jump path density. + +The fully connected scope is finite-state, finite-horizon, and finitely many piecewise-constant protocol windows. The project does not claim arbitrary calendar-time-dependent rates, countably infinite state spaces, diffusions, Langevin dynamics, or SDE path measures. + +## Comparison by the connected probability law + +The important comparison is not whether an artifact contains an individual CTMC or fluctuation theorem, but whether it connects all layers to the same constructed law. + +| Development | CTMC or trajectory law | Non-explosion form | Constructed terminal law identified with `exp(TQ)` | FDD identified with kernel chain | Global driven path law | Crooks/Jarzynski on that law | +| --- | --- | --- | --- | --- | --- | --- | +| [Hölzl / AFP Markov Models](https://isa-afp.org/entries/Markov_Models.html) | Jump-and-hold CTMC in Isabelle/HOL | Infinite-process a.s. non-explosion under bounded escape rates in the current AFP artifact | Not identified in the reviewed source snapshot | Not a stated focus | No | No | +| [Marion / Mathlib](https://arxiv.org/abs/2506.18616) | General Ionescu--Tulcea trajectory measure | Not specific to CTMC explosion | General infrastructure rather than this bridge | General trajectory infrastructure | No | No | +| [Ripple](https://github.com/zinan-huang/Ripple/tree/e9ce148d3975f9e75bb9724e01ec763ad9b368a9) | Canonical finite-state CTMC jump-and-hold law | Infinite record construction, a.s. under additional assumptions | A matrix-exponential transition API exists; a bridge from the reviewed canonical law was not identified | A bridge from the reviewed canonical law was not identified | No | No | +| [PhysicsAI DFT moment body](https://github.com/gecrooks/PhysicsAI/tree/0e03deca084de46e11047a8bb9aafa3e22261a70/dft-moment-body) | Takes a DFT measure identity as input | Not applicable | Not applicable | Not applicable | No | Abstract DFT consequences, integral FT, second law, and Crooks pairs | +| CrooksJarzynskiLean | Sum of explicit fixed-horizon jump-count sectors | Finite-horizon arrival tail vanishes, so no mass escapes to infinitely many jumps | Yes, for the actual terminal pushforward | Yes, for every finite monotone observation family | Yes, by measurable concatenation of complete windows | Yes, on the resulting global laws | + +“Not identified” reports a search of the specified public snapshot. It is negative evidence, not a mathematical proof of absence. + +## Classical stochastic thermodynamics + +Jarzynski introduced the nonequilibrium work equality in 1997 and also derived it using a time-dependent master equation. Crooks derived forward/reverse work relations for microscopically reversible Markovian dynamics and developed the path-ensemble formulation. For continuous-time Markov and jump processes, path-space entropy production and fluctuation symmetries were developed by Lebowitz--Spohn, Maes--Netočný, Seifert, and others. Time-dependent finite-state jump processes and detailed fluctuation theorems are standard models. + +Principal sources: + +- C. Jarzynski, [“A nonequilibrium equality for free energy differences”](https://arxiv.org/abs/cond-mat/9610209), *Physical Review Letters* 78 (1997). +- C. Jarzynski, [“Equilibrium free energy differences from nonequilibrium measurements: a master equation approach”](https://arxiv.org/abs/cond-mat/9707325), *Physical Review E* 56 (1997). +- G. E. Crooks, [“Nonequilibrium Measurements of Free Energy Differences for Microscopically Reversible Markovian Systems”](https://doi.org/10.1023/A:1023208217925), *Journal of Statistical Physics* 90 (1998). +- G. E. Crooks, [“The Entropy Production Fluctuation Theorem and the Nonequilibrium Work Relation for Free Energy Differences”](https://arxiv.org/abs/cond-mat/9901352), *Physical Review E* 60 (1999). +- J. L. Lebowitz and H. Spohn, [“A Gallavotti--Cohen Type Symmetry in the Large Deviation Functional for Stochastic Dynamics”](https://arxiv.org/abs/cond-mat/9811220), *Journal of Statistical Physics* 95 (1999). +- C. Maes and K. Netočný, [“Time-Reversal and Entropy”](https://doi.org/10.1023/A:1021026930129), *Journal of Statistical Physics* 110 (2003). +- U. Seifert, [“Entropy Production along a Stochastic Trajectory and an Integral Fluctuation Theorem”](https://doi.org/10.1103/PhysRevLett.95.040602), *Physical Review Letters* 95 (2005). +- R. Rao and M. Esposito, [“Detailed Fluctuation Theorems: A Unifying Perspective”](https://doi.org/10.3390/e20090635), *Entropy* 20 (2018). + +Accordingly, the paper states explicitly: + +> The fluctuation relations formalized here are classical. Our contribution is a machine-checked construction that connects them to explicitly constructed finite-state jump-process path measures. + +## CTMC path laws and matrix exponentials + +The embedded jump chain, exponential holding times, explosion theory, Kolmogorov equations, and `P_t = exp(tQ)` are standard; a primary textbook reference is J. R. Norris, *Markov Chains*, Chapter 2. Explicit finite-state jump-path densities on a disjoint union of finite records are also standard. Rao and Teh give a closely related path representation and density in the Markov-jump-process literature. + +- J. R. Norris, [*Markov Chains*](https://www.cambridge.org/core/books/markov-chains/B0A8AB4D3187DFE76E17B1E7F33D1B20), Cambridge University Press (1997). +- V. Rao and Y. W. Teh, [“Fast MCMC Sampling for Markov Jump Processes and Extensions”](https://www.jmlr.org/papers/v14/rao13a.html), *JMLR* 14 (2013). + +The free-coordinate path density and products of matrix exponentials are therefore not novelty claims. The formal contribution is the verified bridge from the constructed measure to those standard objects. + +## Mechanized probability and physics + +### Isabelle/HOL + +Johannes Hölzl's [“Markov Processes in Isabelle/HOL”](https://doi.org/10.1145/3018610.3018628) constructs Markov processes and a jump-and-hold CTMC, proving the Markov property, a transition semigroup, and a backward equation. The current [AFP Markov Models](https://isa-afp.org/entries/Markov_Models.html) artifact also contains an almost-sure non-explosion result under bounded escape rates. This rules out broad “first mechanized CTMC” and “first formal non-explosion” claims. + +### Lean trajectory measures + +Étienne Marion's [formalization of the Ionescu--Tulcea theorem in Mathlib](https://arxiv.org/abs/2506.18616) provides general trajectory-measure infrastructure. CrooksJarzynskiLean should be presented as an application and extension within that ecosystem, not as the first Lean trajectory measure. + +### Ripple + +[Ripple](https://github.com/zinan-huang/Ripple) is the closest Lean CTMC comparison. The reviewed snapshot, commit [`e9ce148d`](https://github.com/zinan-huang/Ripple/commit/e9ce148d3975f9e75bb9724e01ec763ad9b368a9), includes finite-state Q-matrices, exponential holding-time laws, an embedded chain, a canonical Ionescu--Tulcea record measure, matrix-exponential transition probabilities, and non-explosion results for its infinite record construction under additional assumptions. + +In that snapshot, the review did not identify a theorem connecting the terminal pushforward of the canonical path law to the matrix-exponential transition API, a finite-dimensional pushforward bridge, or a driven stochastic-thermodynamic layer. This comparison must be rechecked against a fixed Ripple commit immediately before submission. + +### PhysicsAI DFT moment body + +The reviewed [PhysicsAI DFT moment-body snapshot](https://github.com/gecrooks/PhysicsAI/tree/0e03deca084de46e11047a8bb9aafa3e22261a70/dft-moment-body) formalizes a detailed fluctuation theorem as a measure identity and derives reflection, integral fluctuation, second-law, moment, and finite-support Crooks-pair consequences. It assumes the DFT law rather than constructing Markov generators, holding times, CTMC path measures, global driven protocols, or physical work/free energy. + +The two projects are complementary: PhysicsAI studies the structure and consequences of fluctuation-symmetric distributions, while CrooksJarzynskiLean derives a physical fluctuation relation from explicit finite-state dynamics. + +### Lean physics ecosystem + +[LeanChemicalTheories](https://arxiv.org/abs/2210.12150) and [Physlib](https://github.com/leanprover-community/physlib) are prior Lean developments in chemical physics, thermodynamics, and canonical ensembles. They rule out broad priority claims about formalizing thermodynamics or statistical mechanics in Lean, while providing relevant ecosystem context. + +## Search-bounded positioning statement + +The following language may be used in the paper or artifact description: + +> To our knowledge, among the public Lean 4 and Mathlib artifacts reviewed at the fixed snapshots recorded in the bibliography (search completed on 26 August 2026), we did not identify a development that connects an explicitly constructed finite-state continuous-time jump-process path measure to its matrix-exponential terminal and finite-dimensional laws and then to global path measures for finitely many piecewise-constant protocol windows carrying physical Crooks--Jarzynski work relations. + +This is a bounded search report, not a universal “first” claim. The reviewed search covered primary papers, official artifacts, arXiv, AFP, Mathlib, and public GitHub sources. It does not cover private repositories, unpublished manuscripts, or every proof-assistant project in every language. + +The full bibliography used by the manuscript is in [`paper/references.bib`](paper/references.bib). diff --git a/paper/Makefile b/paper/Makefile new file mode 100644 index 0000000..15b6c8d --- /dev/null +++ b/paper/Makefile @@ -0,0 +1,25 @@ +LATEXMK ?= latexmk +DOCKER_IMAGE ?= texlive/texlive:latest +SECTIONS := $(wildcard sections/*.tex) + +LATEXMK_ARGS := -pdf -interaction=nonstopmode -halt-on-error main.tex + +.PHONY: all clean + +all: main.pdf + +main.pdf: main.tex references.bib $(SECTIONS) +ifneq (,$(shell command -v $(LATEXMK))) + $(LATEXMK) $(LATEXMK_ARGS) +else + docker run --rm -v "$(CURDIR)":/work -w /work $(DOCKER_IMAGE) \ + latexmk $(LATEXMK_ARGS) +endif + +clean: +ifneq (,$(shell command -v $(LATEXMK))) + $(LATEXMK) -C main.tex +else + docker run --rm -v "$(CURDIR)":/work -w /work $(DOCKER_IMAGE) \ + latexmk -C main.tex +endif diff --git a/paper/README.md b/paper/README.md new file mode 100644 index 0000000..6d6da37 --- /dev/null +++ b/paper/README.md @@ -0,0 +1,38 @@ +# Paper draft + +This directory contains the first full manuscript draft for the continuous-time core of CrooksJarzynskiLean. + +## Direction + +The paper is deliberately centered on one end-to-end contribution: + +> finite-state generator -> normalized fixed-horizon path measure -> finite-horizon sector-tail non-explosion -> actual terminal and finite-dimensional marginals -> piecewise-constant global driven path law -> physical Crooks--Jarzynski relations. + +The manuscript does **not** claim new fluctuation identities, the first mechanized CTMC, the first Lean trajectory measure, or the first Lean fluctuation theorem. See [`../RELATED_WORK.md`](../RELATED_WORK.md) for the reviewed comparison and the exact scope of the positioning statement. + +## Build + +A standard TeX Live installation with `latexmk` and `biber` is sufficient: + +```bash +cd paper +make +``` + +The generated `main.pdf` is intentionally ignored by Git. Use `make clean` to remove auxiliary files. + +## Files + +- [`main.tex`](main.tex): manuscript entry point and shared preamble; +- [`sections/`](sections/): the eleven top-level paper sections; +- [`references.bib`](references.bib): paper bibliography; +- [`Makefile`](Makefile): reproducible local build. + +The Lean theorem spine is documented in [`../ARTIFACT.md`](../ARTIFACT.md) and the complete declaration map remains in [`../FORMALIZATION.md`](../FORMALIZATION.md). + +## Before submission + +1. Replace the draft author name and affiliation as appropriate. +2. Freeze a versioned release and archival DOI, then update the artifact snapshot in the paper and `CITATION.cff`. +3. Re-audit the fixed Ripple and PhysicsAI comparison snapshots immediately before submission. +4. Select the venue template only after the content and page budget are stable; `main.tex` currently uses the portable `article` class. diff --git a/paper/main.tex b/paper/main.tex new file mode 100644 index 0000000..b1c5f2b --- /dev/null +++ b/paper/main.tex @@ -0,0 +1,70 @@ +\documentclass[11pt]{article} + +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{lmodern} +\usepackage{microtype} +\usepackage[margin=1in]{geometry} +\usepackage{amsmath,amssymb,mathtools} +\usepackage{amsthm} +\usepackage{booktabs} +\usepackage{array} +\usepackage{enumitem} +\usepackage{xurl} +\usepackage{hyperref} +\usepackage[backend=biber,style=authoryear,maxcitenames=2,maxbibnames=99,doi=true,isbn=false,url=true]{biblatex} +\addbibresource{references.bib} + +\hypersetup{ + colorlinks=true, + linkcolor=blue, + citecolor=blue, + urlcolor=blue, + pdftitle={Machine-Checked Path Measures and Fluctuation Relations for Finite-State Continuous-Time Jump Processes in Lean 4}, + pdfauthor={kiyo-e} +} + +\emergencystretch=1.5em + +\newtheorem{theorem}{Theorem} +\newtheorem{corollary}{Corollary} + +\newcommand{\Lean}{Lean~4} +\newcommand{\CJ}{CrooksJarzynskiLean} +\newcommand{\R}{\mathbb{R}} +\newcommand{\E}{\mathbb{E}} +\newcommand{\Pp}{\mathbb{P}} +\newcommand{\dd}{\,\mathrm{d}} +\newcommand{\lean}[1]{\ifmmode\text{\ttfamily\detokenize{#1}}\else\nolinkurl{#1}\fi} +\newcommand{\file}[1]{\ifmmode\text{\ttfamily\detokenize{#1}}\else\nolinkurl{#1}\fi} +\newcommand{\artifactbase}{\texttt{efbf55e}} + +\title{Machine-Checked Path Measures and Fluctuation Relations\\ +for Finite-State Continuous-Time Jump Processes in Lean 4} +\author{kiyo-e\\ +\small \url{https://github.com/kiyo-e/CrooksJarzynskiLean}} +\date{Draft of 27 August 2026} + +\begin{document} +\maketitle + +\begin{abstract} +Compact derivations of fluctuation relations for Markov jump processes move directly between generator dynamics, trajectory-weight ratios, and work distributions, without keeping a single normalized path measure explicit throughout. We give an end-to-end, machine-checked Lean~4 construction for finite-state processes on a finite time horizon. Starting from a conservative generator, we build a normalized measure on finite jump records, prove finite-horizon non-explosion, and identify its terminal and finite-dimensional marginals with the semigroup $\exp(tQ)$. We then concatenate finitely many constant-generator windows separated by instantaneous energy switches. If each window generator satisfies detailed balance with respect to the Gibbs distribution of its current energy landscape, the forward path law and the chronology-aligned reverse law obtained by windowwise record reversal obey the path-measure Crooks identity $e^{-\beta W}\,\Pp_F = e^{-\beta\Delta F}\,\Pp_R^{\Theta}$, where $W$ is the inclusive work done on the system. Jarzynski's equality and, for $\beta>0$, the average-work inequality $\langle W\rangle_F \ge \Delta F$ follow on the same constructed path space. The result covers finite state spaces, finite time, and finite stepwise protocols; no new fluctuation identity is claimed. +\end{abstract} + + +\input{sections/01-introduction.tex} +\input{sections/02-mathematical-setting.tex} +\input{sections/03-normalized-path-measure.tex} +\input{sections/04-matrix-exponential-semigroup.tex} +\input{sections/05-driven-global-laws.tex} +\input{sections/06-formalization-architecture.tex} +\input{sections/07-examples.tex} +\input{sections/08-related-work.tex} +\input{sections/09-limitations.tex} +\input{sections/10-artifact.tex} +\input{sections/11-conclusion.tex} + +\printbibliography + +\end{document} diff --git a/paper/references.bib b/paper/references.bib new file mode 100644 index 0000000..095885b --- /dev/null +++ b/paper/references.bib @@ -0,0 +1,304 @@ +@article{Jarzynski1997PRL, + author = {Jarzynski, Christopher}, + title = {Nonequilibrium Equality for Free Energy Differences}, + journaltitle = {Physical Review Letters}, + year = {1997}, + volume = {78}, + number = {14}, + pages = {2690--2693}, + doi = {10.1103/PhysRevLett.78.2690}, + eprint = {cond-mat/9610209}, + eprinttype = {arXiv} +} + +@article{Jarzynski1997PRE, + author = {Jarzynski, Christopher}, + title = {Equilibrium Free-Energy Differences from Nonequilibrium Measurements: A Master-Equation Approach}, + journaltitle = {Physical Review E}, + year = {1997}, + volume = {56}, + number = {5}, + pages = {5018--5035}, + doi = {10.1103/PhysRevE.56.5018}, + eprint = {cond-mat/9707325}, + eprinttype = {arXiv} +} + +@article{Crooks1998, + author = {Crooks, Gavin E.}, + title = {Nonequilibrium Measurements of Free Energy Differences for Microscopically Reversible Markovian Systems}, + journaltitle = {Journal of Statistical Physics}, + year = {1998}, + volume = {90}, + pages = {1481--1487}, + doi = {10.1023/A:1023208217925} +} + +@article{Crooks1999, + author = {Crooks, Gavin E.}, + title = {Entropy Production Fluctuation Theorem and the Nonequilibrium Work Relation for Free Energy Differences}, + journaltitle = {Physical Review E}, + year = {1999}, + volume = {60}, + number = {3}, + pages = {2721--2726}, + doi = {10.1103/PhysRevE.60.2721}, + eprint = {cond-mat/9901352}, + eprinttype = {arXiv} +} + +@article{Crooks2000, + author = {Crooks, Gavin E.}, + title = {Path-Ensemble Averages in Systems Driven Far from Equilibrium}, + journaltitle = {Physical Review E}, + year = {2000}, + volume = {61}, + number = {3}, + pages = {2361--2366}, + doi = {10.1103/PhysRevE.61.2361} +} + +@article{LebowitzSpohn1999, + author = {Lebowitz, Joel L. and Spohn, Herbert}, + title = {A Gallavotti--Cohen-Type Symmetry in the Large Deviation Functional for Stochastic Dynamics}, + journaltitle = {Journal of Statistical Physics}, + year = {1999}, + volume = {95}, + pages = {333--365}, + eprint = {cond-mat/9811220}, + eprinttype = {arXiv} +} + +@article{MaesNetocny2003, + author = {Maes, Christian and Neto\v{c}n\'y, Karel}, + title = {Time-Reversal and Entropy}, + journaltitle = {Journal of Statistical Physics}, + year = {2003}, + volume = {110}, + pages = {269--310}, + doi = {10.1023/A:1021026930129} +} + +@article{Seifert2005, + author = {Seifert, Udo}, + title = {Entropy Production along a Stochastic Trajectory and an Integral Fluctuation Theorem}, + journaltitle = {Physical Review Letters}, + year = {2005}, + volume = {95}, + pages = {040602}, + doi = {10.1103/PhysRevLett.95.040602} +} + +@article{Seifert2012, + author = {Seifert, Udo}, + title = {Stochastic thermodynamics, fluctuation theorems and molecular machines}, + journaltitle = {Reports on Progress in Physics}, + volume = {75}, + number = {12}, + pages = {126001}, + year = {2012}, + doi = {10.1088/0034-4885/75/12/126001} +} + +@book{Sekimoto2010, + author = {Sekimoto, Ken}, + title = {Stochastic Energetics}, + series = {Lecture Notes in Physics}, + volume = {799}, + publisher = {Springer}, + address = {Berlin, Heidelberg}, + year = {2010}, + doi = {10.1007/978-3-642-05411-2} +} + +@article{VandenBroeckEsposito2015, + author = {Van den Broeck, Christian and Esposito, Massimiliano}, + title = {Ensemble and trajectory thermodynamics: A brief introduction}, + journaltitle = {Physica A: Statistical Mechanics and its Applications}, + volume = {418}, + pages = {6--16}, + year = {2015}, + doi = {10.1016/j.physa.2014.04.035} +} + +@article{Maes2021, + author = {Maes, Christian}, + title = {Local detailed balance}, + journaltitle = {SciPost Physics Lecture Notes}, + pages = {32}, + year = {2021}, + doi = {10.21468/SciPostPhysLectNotes.32} +} + +@article{SpinneyFord2012, + author = {Spinney, Richard E. and Ford, Ian J.}, + title = {Nonequilibrium Thermodynamics of Stochastic Systems with Odd and Even Variables}, + journaltitle = {Physical Review Letters}, + volume = {108}, + number = {17}, + pages = {170603}, + year = {2012}, + doi = {10.1103/PhysRevLett.108.170603} +} + +@article{MaesNetocnyWynants2008, + author = {Maes, Christian and Neto\v{c}n\'y, Karel and Wynants, Bram}, + title = {On and beyond Entropy Production: The Case of Markov Jump Processes}, + journaltitle = {Markov Processes and Related Fields}, + year = {2008}, + volume = {14}, + pages = {445--464}, + eprint = {0709.4327}, + eprinttype = {arXiv} +} + +@article{ShargelChou2009, + author = {Shargel, Benjamin H. and Chou, Tom}, + title = {Fluctuation Theorems for Entropy Production and Heat Dissipation in Periodically Driven Markov Chains}, + journaltitle = {Journal of Statistical Physics}, + year = {2009}, + volume = {137}, + pages = {165--188}, + doi = {10.1007/s10955-009-9836-8} +} + +@article{RaoTeh2013, + author = {Rao, Vinayak and Teh, Yee Whye}, + title = {Fast {MCMC} Sampling for Markov Jump Processes and Extensions}, + journaltitle = {Journal of Machine Learning Research}, + year = {2013}, + volume = {14}, + pages = {3295--3320}, + url = {https://www.jmlr.org/papers/v14/rao13a.html} +} + +@article{RaoEsposito2018, + author = {Rao, Riccardo and Esposito, Massimiliano}, + title = {Detailed Fluctuation Theorems: A Unifying Perspective}, + journaltitle = {Entropy}, + year = {2018}, + volume = {20}, + number = {9}, + pages = {635}, + doi = {10.3390/e20090635} +} + +@book{Gardiner2009, + author = {Gardiner, Crispin}, + title = {Stochastic Methods: A Handbook for the Natural and Social Sciences}, + edition = {4}, + publisher = {Springer}, + year = {2009} +} + +@article{KawaiParrondoVandenBroeck2007, + author = {Kawai, R. and Parrondo, J. M. R. and Van den Broeck, C.}, + title = {Dissipation: The Phase-Space Perspective}, + journal = {Physical Review Letters}, + volume = {98}, + pages = {080602}, + year = {2007}, + doi = {10.1103/PhysRevLett.98.080602} +} + +@book{Norris1997, + author = {Norris, J. R.}, + title = {Markov Chains}, + publisher = {Cambridge University Press}, + year = {1997}, + doi = {10.1017/CBO9780511810633} +} + +@book{PelitiPigolotti2021, + author = {Peliti, Luca and Pigolotti, Simone}, + title = {Stochastic Thermodynamics: An Introduction}, + publisher = {Princeton University Press}, + year = {2021} +} + +@inproceedings{Hoelzl2017, + author = {H\"olzl, Johannes}, + title = {Markov Processes in {Isabelle/HOL}}, + booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}, + year = {2017}, + pages = {100--111}, + doi = {10.1145/3018610.3018628} +} + +@online{AFPMarkovModels, + author = {H\"olzl, Johannes and Nipkow, Tobias}, + title = {Markov Models}, + year = {2012}, + organization = {Archive of Formal Proofs}, + url = {https://isa-afp.org/entries/Markov_Models.html}, + urldate = {2026-08-26}, + note = {First submitted 2012; session snapshot accessed 26 August 2026} +} + +@online{Marion2025, + author = {Marion, \'Etienne}, + title = {A Formalization of the Ionescu--Tulcea Theorem in Mathlib}, + year = {2025}, + eprint = {2506.18616}, + eprinttype = {arXiv}, + url = {https://arxiv.org/abs/2506.18616} +} + +@online{Ripple2026, + author = {Chen, H.-L. and Huang, X.}, + title = {Ripple: An Open, AI-Formalized Lean 4 Framework for Computing with CRNs}, + year = {2026}, + eprint = {2607.13531}, + eprinttype = {arXiv}, + url = {https://github.com/zinan-huang/Ripple}, + note = {CTMC source reviewed at commit e9ce148d3975f9e75bb9724e01ec763ad9b368a9} +} + +@online{PhysicsAIDFT, + author = {{PhysicsAI Project}}, + title = {The Exact Moment Body of the Detailed Fluctuation Theorem}, + year = {2026}, + url = {https://github.com/gecrooks/PhysicsAI/tree/0e03deca084de46e11047a8bb9aafa3e22261a70/dft-moment-body}, + urldate = {2026-08-26}, + note = {Repository snapshot 0e03deca084de46e11047a8bb9aafa3e22261a70} +} + +@article{Bobbin2024, + author = {Bobbin, Maxwell P. and Sharlin, Samiha and Feyzishendi, Parivash and Dang, An Hong and Wraback, Catherine M. and Josephson, Tyler R.}, + title = {Formalizing Chemical Physics using the Lean Theorem Prover}, + journaltitle = {Digital Discovery}, + year = {2024}, + volume = {3}, + pages = {264--280}, + doi = {10.1039/D3DD00077J}, + eprint = {2210.12150}, + eprinttype = {arXiv} +} + +@online{Physlib, + author = {{Lean Community}}, + title = {Physlib: A Physical Mathematics Library for Lean 4}, + year = {2026}, + url = {https://github.com/leanprover-community/physlib}, + urldate = {2026-08-26} +} + +@inproceedings{Moura2021, + author = {de Moura, Leonardo and Ullrich, Sebastian}, + title = {The {Lean} 4 Theorem Prover and Programming Language}, + booktitle = {Automated Deduction -- CADE 28}, + series = {Lecture Notes in Computer Science}, + volume = {12699}, + year = {2021}, + pages = {625--635}, + doi = {10.1007/978-3-030-79876-5_37} +} + +@inproceedings{Mathlib2020, + author = {{The mathlib Community}}, + title = {The {Lean} Mathematical Library}, + booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs}, + year = {2020}, + pages = {367--381}, + doi = {10.1145/3372885.3373824} +} diff --git a/paper/sections/01-introduction.tex b/paper/sections/01-introduction.tex new file mode 100644 index 0000000..cc7b18e --- /dev/null +++ b/paper/sections/01-introduction.tex @@ -0,0 +1,50 @@ +\section{Introduction} + +Are the trajectories entering Crooks' fluctuation relation the same stochastic process whose one-time probabilities solve the master equation? For a standard continuous-time Markov chain the answer is, of course, yes: stochastic thermodynamics routinely moves between a rate generator, a normalized trajectory ensemble, and forward and reverse trajectory likelihoods, and their compatibility is standard in informal calculations. The contribution of this paper is to establish that compatibility as one end-to-end, machine-checked construction: for finite-state, finite-time, stepwise-driven jump processes, all three descriptions are proved to refer to the same constructed probability law. + +Fluctuation relations connect nonequilibrium trajectory statistics to equilibrium free-energy differences. Jarzynski's equality and Crooks' fluctuation relation are classical results, with formulations for Markovian systems, master equations, and path ensembles \parencite{Jarzynski1997PRL,Jarzynski1997PRE,Crooks1998,Crooks1999,Crooks2000}. Continuous-time Markov chains and finite-state jump processes are likewise standard: a conservative generator determines exponential holding times, an embedded jump chain away from absorbing states, a transition semigroup $P_t=\exp(tQ)$, and explicit finite-record path densities \parencite{Norris1997,Gardiner2009,RaoTeh2013}. +What is less automatic in a proof assistant is that the objects used at different levels of the usual argument are actually the same probability law. A sector-mass calculation does not by itself identify a pushforward of a constructed path measure. A matrix exponential defined independently of the path space does not by itself describe the terminal or finite-dimensional marginals of that measure. A list of window laws does not by itself yield a measurable global real-time trajectory. Finally, an abstract detailed fluctuation identity does not by itself show that concrete forward and reverse laws generated by physical dynamics satisfy it. + +This paper presents an end-to-end mechanization of that connection. The formal development begins with nonnegative jump rates on a finite state space, constructs a fixed-horizon probability measure on the disjoint union of all finite jump records, identifies the actual terminal and finite-dimensional pushforwards with the matrix-exponential semigroup, concatenates finitely many piecewise-constant windows into one real-time path, and proves physical fluctuation relations on the resulting global laws. + +The main contributions are as follows. + +\begin{enumerate}[leftmargin=*,label=(\arabic*)] + \item We construct forward and reverse global path laws for a finite stepwise protocol directly from rates, energies, and durations, and prove the Crooks and Jarzynski relations and, for positive inverse temperature, the second-law inequality on that constructed global path space. + + \item Underlying the protocol, we construct the finite-horizon jump-trajectory measure of each window as a sum over jump-count sectors and prove its normalization, equivalently finite-horizon non-explosion. + + \item We identify the terminal law and all finite-dimensional distributions of that same measure, at nondecreasing observation times, with the Markov semigroup $\exp(tQ)$. +\end{enumerate} + +\paragraph{Main physical result.} +For a finite state space and finitely many constant-control windows separated by instantaneous quenches, assume that each window generator is reversible with respect to the Gibbs distribution of its own energy landscape at a common inverse temperature $\beta>0$. Starting the forward experiment from the initial Gibbs state and the reverse experiment from the final Gibbs state, the constructed global laws are mutually absolutely continuous and satisfy +\[ + \frac{\dd\Pp_F^{\mathrm{glob}}}{\dd\Pp_R^{\Theta}}(\gamma) + =\exp\!\bigl[\beta\bigl(W(\gamma)-\Delta F\bigr)\bigr], +\] +where $W$ is the inclusive switching work and $\Delta F$ the equilibrium free-energy difference of the initial and final landscapes (Theorem~\ref{thm:main}). No irreducibility, uniqueness-of-equilibrium, long-window equilibration, or smooth-protocol limit is assumed. The normalization of the trajectory law and its identification with $\exp(tQ)$ are the two enabling results behind this theorem. + +The present paper deliberately focuses on the continuous-time chain shown in the concept figure; the broader contents of the repository are summarized in Section~\ref{sec:artifact}. +\begin{figure}[htbp] +\centering +\[ +\begin{aligned} + \text{generator rates} + &\xrightarrow{\ \text{\small free-simplex sector charts}\ } + \text{fixed-jump-count sector laws}\\ + &\xrightarrow{\ \text{\small tail disappearance, normalization}\ } + \Pp_{T,x}\\ + &\xrightarrow{\ \text{\small terminal and finite-time sampling}\ } + \exp(TQ)\text{ kernels and FDDs}\\ + &\xrightarrow{\ \text{\small window kernels, measurable concatenation}\ } + \text{forward and aligned-reverse global laws}\\ + &\xrightarrow{\ \text{\small Gibbs detailed balance}\ } + \text{Crooks, Jarzynski, second law, work distribution}. +\end{aligned} +\] +\caption{The end-to-end theorem chain. The fixed-initial path law $\Pp_{T,x}$ is constructed from the jump-count sectors (\lean{pathLawFrom}).} +\end{figure} + +\paragraph{Scope and novelty.} +The verified result concerns a finite state space, a finite total time, and finitely many stepwise changes of the energy landscape. Each dynamical window is governed by a constant, single-temperature generator that is reversible with respect to the instantaneous Gibbs distribution, and time reversal acts trivially on the states. The result does not cover smooth calendar-time dependence or a step-to-smooth refinement limit, multiple reservoirs, nonconservative steady-state forcing, odd time-reversal variables, infinite-time path laws, or diffusions. Mechanized Markov-process theory predates this work, including Isabelle/HOL developments and recent Lean infrastructure \parencite{Hoelzl2017,AFPMarkovModels,Marion2025,Ripple2026}; concurrent Lean work also studies consequences of an assumed detailed fluctuation theorem \parencite{PhysicsAIDFT}. Section~\ref{sec:related} gives the detailed positioning. diff --git a/paper/sections/02-mathematical-setting.tex b/paper/sections/02-mathematical-setting.tex new file mode 100644 index 0000000..d5cf838 --- /dev/null +++ b/paper/sections/02-mathematical-setting.tex @@ -0,0 +1,66 @@ +\section{Mathematical setting} +\label{sec:setting} + +Let $\Omega$ be a nonempty finite state space. A finite jump generator is specified by rates +\[ + k(x,y) \ge 0 \qquad (x\ne y), +\] +with escape rate +\[ + \lambda(x)=\sum_{y\ne x} k(x,y) +\] +and conservative generator matrix +\[ + Q(x,y)= + \begin{cases} + k(x,y), & x\ne y,\\ + -\lambda(x), & x=y. + \end{cases} +\] +We use row probability vectors throughout: a distribution $p_0$ evolves as $p_t=p_0e^{tQ}$, solving the master equation $\dot p_t=p_tQ$, so that $Q(x,y)=k(x,y)$ is the rate from $x$ to $y$ and the rows of $Q$ sum to zero. We extend the rate function to all state pairs by setting $k(x,x)=0$; consequently, diagonal terms in the unrestricted sums and products below vanish, so the sector densities and the renewal equation may be written without excluding equal adjacent states. The formal structure \lean{FiniteJumpGenerator} packages the nonnegative rates together with this diagonal convention (\lean{jumpRate_self}), the induced escape rates and real generator, and the reference measures used below. Conservation is proved as the row-sum identity $\sum_y Q(x,y)=0$. + +\subsection{Fixed-jump-count charts} + +An $n$-jump-sector record is represented by a state sequence and a holding-time sequence, +\[ + \gamma=((x_0,\ldots,x_n),(\tau_0,\ldots,\tau_n)). +\] +The final holding interval $\tau_n$ records the no-jump remainder after the last jump. The ambient record type also contains degenerate records, with equal adjacent states or with holding times inconsistent with the horizon; the sector laws below assign such records measure zero, through the diagonal convention $k(x,x)=0$ and the fixed-horizon support theorem, and concentrate almost surely on valid fixed-horizon records. In Lean the type is +\[ + \lean{JumpPath Omega n} + = (\lean{Fin (n+1) -> Omega})\times + (\lean{Fin (n+1) -> NNReal}). +\] +All finite jump counts are assembled into the dependent sum +\[ + \lean{FullPath Omega}=\sum_{n:\mathbb{N}} \lean{JumpPath Omega n}. +\] +The development defines measurable terminal-state, jump-time, and right-continuous trajectory maps on this carrier. The single-window laws and the global pushforward laws of Section~\ref{sec:driven} live on this dependent sum of finite jump records, equipped with measurable right-continuous real-time evaluation maps; the intermediate marked laws of Section~\ref{sec:driven} live on finite collections of \lean{FullPath} records and are mapped onto \lean{FullPath Omega} by measurable concatenation. We do not construct the laws directly on a canonical Skorokhod space of c\`adl\`ag functions. + +For a fixed horizon $T\ge 0$, the holding times should satisfy $\sum_{i=0}^{n}\tau_i=T$. Restricting an ambient $(n+1)$-dimensional product Lebesgue measure to this equality slice would give the zero measure. The formalization therefore uses the free simplex +\[ + \Delta_n=\left\{u\in[0,1]^n:\sum_{i0$, the forward experiment evolves under the constant generator $G_i$ on landscape $E_i$ for time $T_i$ and is quenched $E_i\to E_{i+1}$ at the end of the window; the reverse experiment applies the mirrored quench before the corresponding window. For $M=0$, both protocols degenerate to the equilibrium experiment with no evolution and zero work, and the theorems below hold trivially. + +Let $\Pp_R$ denote the law of the reverse protocol in its own chronology, and let $\Pp_R^{\Theta}$ denote its chronology-aligned image on the common path carrier. For a c\`adl\`ag trajectory $X$ on a horizon $[0,\tau]$ and a kinematic time-reversal involution $\vartheta$, the standard time reversal is \parencite{MaesNetocny2003,SpinneyFord2012} +\[ + (\Theta X)_t=\vartheta X_{(\tau-t)-}\quad(0\le t<\tau), + \qquad + (\Theta X)_\tau=\vartheta X_0 . +\] +In the present work all state variables are even, so $\vartheta=\mathrm{id}$. The left-limit convention is what keeps the reversed trajectory right-continuous: the naive pointwise reversal $t\mapsto X_{\tau-t}$ would fail right continuity at jump times. On a fixed-jump-count chart, the corresponding reversal of finite jump records is (\lean{JumpPath.reverse}) +\begin{equation} +\label{eq:reversal} + \Theta\bigl((x_0,\ldots,x_n),(\tau_0,\ldots,\tau_n)\bigr) + = \bigl((x_n,\ldots,x_0),(\tau_n,\ldots,\tau_0)\bigr), +\end{equation} +which fixes the state assigned at each jump time in accordance with that left-limit convention. This correspondence is itself machine-checked: on an exact-horizon record, the reversed trajectory equals the original trajectory at the mirrored time whenever the mirrored time is not a jump time (\lean{FullPath.trajectory_reverse_eq_mirror}); at each fixed observation time the identity holds almost surely under the constructed fixed-initial law (\lean{pathLawFrom_ae_trajectory_reverse_eq_mirror}); and consequently the joint law of the reversed trajectory at any finite family of times equals the joint law of the original trajectory at the mirrored times (\lean{map_trajectory_reverse_eq_map_mirror}). Because the forward schedule contains the final boundary quench $E_{M-1}\to E_M$ at $t=\tau$, the time-reversed schedule contains the corresponding initial boundary quench $E_M\to E_{M-1}$ at $t=0$. + +In the formal construction, each reverse window path is transformed by $\Theta$ exactly once, before it is stored on the common forward-aligned marked carrier (\lean{reverseWindowKernel}); the marked reverse law is therefore already chronology-aligned, and the global reverse law $\Pp_R^{\Theta}$ is obtained from it by chronological concatenation. In this way $\Pp_R^{\Theta}$ realizes the time-reversed image $\Theta_*\Pp_R$ of the reverse-protocol law: within each window the identification is proved at the level of all finite-dimensional distributions by the mirror theorems above, and the global concatenated laws are additionally matched at the window boundaries almost surely. It is called the aligned reverse law in the formal development, and it is charted in the forward time direction, not in the reverse experiment's own chronology. A single global statement mirroring arbitrary observation times across window seams is not formalized (Section~\ref{sec:limitations}). + +\subsection{Measurable global concatenation} + +The marked representation is convenient for recursive measure construction, but physical work should also be readable on a single real-time trajectory. The function \lean{concatenateWindows} restores chronological order and glues every window chart into one \lean{FullPath}. The seam holding intervals are merged by the lower-level concatenation operation. The formalization proves: + +\begin{itemize}[leftmargin=*] + \item measurability of the global concatenation map; + \item addition of total holding times; + \item preservation of validity over the summed horizon; + \item right-continuous left and right trajectory gluing laws; and + \item recovery of marked boundary states from the global trajectory almost surely. +\end{itemize} + +The global laws are the pushforwards +\[ + \Pp_F^{\mathrm{glob}} + =\Pp_F^{\mathrm{marked}}\circ C^{-1}, + \qquad + \Pp_R^{\Theta} + =\Pp_R^{\Theta,\mathrm{marked}}\circ C^{-1}, +\] +where $C$ is chronological concatenation. Both are probability measures. + +\subsection{Work and detailed balance} + +Let $s_i=\sum_{j0$, and negative $\beta$ may be read as a formal parameter. During each fixed-control window, the time-homogeneous generator $G_i$ obeys equilibrium detailed balance --- equivalently, Gibbs reversibility --- with respect to the Gibbs distribution of the current landscape, +\[ + \pi_i(x)=Z_i^{-1}e^{-\beta E_i(x)}, + \qquad + \pi_i(x)\,k_i(x,y)=\pi_i(y)\,k_i(y,x). +\] +On every edge with nonvanishing rates this is the familiar rate-ratio form +\[ + \log\frac{k_i(x,y)}{k_i(y,x)} + =-\beta\bigl[E_i(y)-E_i(x)\bigr], +\] +while, after cancelling $Z_i$, the unnormalized identity used in Lean is the division-free form that also covers absent edges: +\begin{equation} +\label{eq:gibbs-db} + e^{-\beta E_i(x)} k_i(x,y) + = e^{-\beta E_i(y)} k_i(y,x) + \qquad (x\ne y). +\end{equation} +This division-free form is the hypothesis \lean{FiniteJumpGenerator.IsGibbsDetailedBalance}; the formal development calls it windowwise Gibbs detailed balance. In stochastic-thermodynamic language, condition~\eqref{eq:gibbs-db} is the one-reservoir, energy-only specialization of local detailed balance \parencite{Maes2021}: there is a single equilibrium reservoir, no nonconservative affinity, and no stationary probability current in $\pi_i$; no reservoir decomposition or reservoir-resolved entropy flow is modeled. Detailed balance is a property of the generator $G_i$: it makes $\pi_i$ the stationary reference distribution of the window, and it does not imply that the actual state distribution equals $\pi_i$ during the finite window duration $T_i$. The adjoint time-reversed rates are +\[ + k_i^{\dagger}(x,y)=\frac{\pi_i(y)\,k_i(y,x)}{\pi_i(x)}, +\] +and equilibrium detailed balance states exactly $k_i^{\dagger}=k_i$; this is why the reverse protocol uses the same window generator $G_i$, with the windows traversed in the opposite order. Let +\[ + Z_i=\sum_{x\in\Omega}e^{-\beta E_i(x)}, + \qquad + F_i=-\beta^{-1}\log Z_i, + \qquad + \Delta F=F_M-F_0. +\] +Here $F_M$ is the equilibrium free energy associated with the final landscape $E_M$; the actual forward ensemble need not be equilibrated at the end of the protocol. It is the reverse experiment that prepares the Gibbs distribution of $E_M$, before its initial mirrored quench. + +The physical content of the balance condition can be seen directly at the trajectory level. For a forward trajectory $\gamma$ and its conjugate reverse trajectory, the exponential survival factors of the sector density~\eqref{eq:sector-density} cancel, because the two trajectories visit the same states for the same holding times. Every jump $x\to y$ in window $i$ contributes the rate ratio $\log[k_i(x,y)/k_i(y,x)]=-\beta[E_i(y)-E_i(x)]$. For physical interpretation (heat is not formalized in the development), define the heat absorbed by the system as +\[ + Q_{\mathrm{sys}}(\gamma) + =\sum_{\text{jumps }x^-\to x^+\text{ in window }i} + \bigl[E_i(x^+)-E_i(x^-)\bigr], +\] +so that the first law for this protocol reads $E_M(X_\tau)-E_0(X_0)=W+Q_{\mathrm{sys}}$, while detailed balance sums the rate ratios to $-\beta Q_{\mathrm{sys}}$. The jump contributions therefore telescope against the Gibbs boundary weights: heuristically, +\[ + \log\frac{\dd\Pp_F^{\mathrm{glob}}}{\dd\Pp_R^{\Theta}}(\gamma) + = \log\frac{\pi_0(x_0)}{\pi_M(x_\tau)} + +\sum_{\mathrm{jumps}} + \log\frac{k_i(x^-,x^+)}{k_i(x^+,x^-)} + = \beta\bigl[W(\gamma)-\Delta F\bigr], +\] +since the boundary weights contribute $\log[\pi_0(x_0)/\pi_M(x_\tau)]=\beta[E_M(x_\tau)-E_0(x_0)]-\beta\Delta F$, and the first law converts $E_M(x_\tau)-E_0(x_0)-Q_{\mathrm{sys}}$ into the switching work~\eqref{eq:work}. This is the familiar trajectory-level cancellation of stochastic thermodynamics \parencite{Crooks1999,Seifert2012,Maes2021}; the theorem below is its measure-theoretic realization on the constructed path law, stated without dividing by the probability of an individual trajectory. The path-density proof establishes exactly this identity in division-free form: it first proves a window balance for mixtures of the actual fixed-initial laws, then lifts it through the recursive marked construction, and finally maps it through global concatenation. + +\subsection{Global fluctuation relations} + +For a measure $P$ and a measurable weight $q\ge 0$, the reweighted measure is +\[ + \bigl(P.\operatorname{withDensity}(q)\bigr)(A) + = \int_A q(\gamma)\,P(\mathrm{d}\gamma). +\] +The central result of the development can now be stated as one theorem whose hypotheses are exactly those of \lean{global_crooks_of_gibbsDetailedBalance}. + +\begin{theorem}[Path-space Crooks relation] +\label{thm:main} +Assume: +\begin{enumerate}[label=(\roman*),leftmargin=*,nosep] + \item $\Omega$ is a nonempty finite state space; + \item the protocol has finitely many windows $M$ with durations $T_i\ge 0$; + \item each window carries a finite jump generator $G_i$ satisfying the windowwise Gibbs detailed balance~\eqref{eq:gibbs-db} for its own landscape $E_i$; + \item $\beta\ne 0$; + \item the forward experiment starts from the initial Gibbs state $e^{-\beta E_0}/Z_0$ and the reverse experiment starts from the final Gibbs state $e^{-\beta E_M}/Z_M$; + \item work uses the evolve-then-quench convention~\eqref{eq:work}, and the reverse law is the chronology-aligned pushforward $\Pp_R^{\Theta}$ of the reverse experiment's window records under record reversal~\eqref{eq:reversal} and concatenation. +\end{enumerate} +Then +\begin{equation} +\label{eq:global-crooks} + e^{-\beta W(\gamma)}\,\Pp_F^{\mathrm{glob}}(\dd\gamma) + =e^{-\beta\Delta F}\,\Pp_R^{\Theta}(\dd\gamma). +\end{equation} +Because $W$ has finite range for a finite state space and a finite protocol, the density $e^{-\beta W}$ is bounded and strictly positive, so~\eqref{eq:global-crooks} implies that $\Pp_F^{\mathrm{glob}}$ and $\Pp_R^{\Theta}$ are mutually absolutely continuous, with Radon--Nikodym derivative +\begin{equation} + \log\frac{\dd\Pp_F^{\mathrm{glob}}}{\dd\Pp_R^{\Theta}}(\gamma) + =\beta\bigl(W(\gamma)-\Delta F\bigr) +\end{equation} +almost surely --- a derivative between path measures, not a ratio of probabilities assigned to singleton trajectories. The Lean theorem states the first, division-free measure identity: +\begin{equation} +\label{eq:global-crooks-lean} + \Pp_F^{\mathrm{glob}}.\operatorname{withDensity} + \left(e^{-\beta W}\right) + = e^{-\beta\Delta F}\,\Pp_R^{\Theta}. +\end{equation} +\end{theorem} + +Defining the dissipated work $W_{\mathrm{diss}}=W-\Delta F$, the path-space irreversibility variable is $\Sigma=\beta W_{\mathrm{diss}}$ \parencite{Seifert2012,VandenBroeckEsposito2015}. Jarzynski's equality and the mean-work inequality are respectively the exponential and first-moment consequences of this same path-measure identity. The machine-checked Crooks and Jarzynski identities hold for every $\beta\ne0$; the average-work inequality is stated for $\beta>0$. No irreducibility, uniqueness-of-equilibrium, or long-window equilibration assumption is required. + +For $\beta>0$, averaging the logarithmic density under the forward law gives the standard information-theoretic reading +\[ + D\!\left(\Pp_F^{\mathrm{glob}}\,\middle\|\,\Pp_R^{\Theta}\right) + = \beta\bigl(\langle W\rangle_F-\Delta F\bigr): +\] +the mean dissipated work is the path-space distinguishability of the forward and reverse experiments \parencite{KawaiParrondoVandenBroeck2007,Crooks1999,Seifert2012}. This consequence of~\eqref{eq:global-crooks-lean} is also mechanized: the log-likelihood ratio is identified with $\beta(W-\Delta F)$ forward-almost surely, and the divergence evaluates to the mean dissipated work (\lean{llr_forwardGlobalLaw_reverseGlobalLaw}, \lean{klDiv_forwardGlobalLaw_reverseGlobalLaw}). + +\begin{corollary}[Jarzynski equality] +Under the hypotheses of Theorem~\ref{thm:main}, evaluating~\eqref{eq:global-crooks-lean} on the whole path space yields +\begin{equation} +\label{eq:jarzynski} + \E_F\left[e^{-\beta W}\right]=e^{-\beta\Delta F}. +\end{equation} +\end{corollary} + +\begin{corollary}[Average-work second law] +Under the hypotheses of Theorem~\ref{thm:main} with $\beta>0$, Jensen's inequality and integrability of $W$ give +\begin{equation} +\label{eq:second-law} + \Delta F\le \E_F[W]. +\end{equation} +\end{corollary} + +The development also maps~\eqref{eq:global-crooks-lean} to the work coordinate, and it does so at the level of measures first, consistent with the design decision of Section~\ref{sec:architecture}. Recall that $\Pp_R^{\Theta}$ is charted in the forward chronology, so the aligned work coordinate $W$ of~\eqref{eq:work} is available on it. In the reverse experiment's own chronology, with window boundary times $\tilde s_j$ and trajectory $\tilde X$, the reverse protocol quenches $E_{M-j}\to E_{M-j-1}$ before its $j$-th window, so its intrinsic switching work is +\[ + W_R(\tilde\gamma) + =\sum_{j=0}^{M-1} + \left[ + E_{M-j-1}\bigl(\tilde X_{\tilde s_j}\bigr) + -E_{M-j}\bigl(\tilde X_{\tilde s_j}\bigr) + \right]. +\] +We use the same symbol $W_R$ for the transport of this intrinsic reverse-chronology observable to the aligned carrier. Under record reversal and chronology alignment, it equals the negated aligned coordinate, $W_R=-W$, an identity proved pointwise in the development (\lean{reverseWork_eq_neg}); the law of $W_R$ agrees with the recursively defined marked reverse work. Writing +\[ + \mu_F=W_*\,\Pp_F^{\mathrm{glob}}, + \qquad + \mu_R=(W_R)_*\,\Pp_R^{\Theta}, +\] +the pushforward of~\eqref{eq:global-crooks-lean} is the measure-level Crooks work-distribution relation +\begin{equation} +\label{eq:work-crooks} + \mu_F.\operatorname{withDensity}\bigl(w\mapsto e^{-\beta w}\bigr) + = e^{-\beta\Delta F}\,(-\mathrm{id})_*\,\mu_R +\end{equation} +(\lean{global_work_distribution_crooks_reverseWork_of_gibbsDetailedBalance}). Because $\Omega$ and $M$ are finite, $W$ has finite range, and evaluating~\eqref{eq:work-crooks} on singletons recovers the conventional atomwise statement +\begin{equation} +\label{eq:atom-crooks} + \Pp_F^{\mathrm{glob}}(W=w) + =e^{\beta(w-\Delta F)}\,\Pp_R^{\Theta}(W_R=-w). +\end{equation} +All of these theorems are stated on the global pushforward laws constructed from the generators, rather than on abstract work distributions supplied as assumptions. diff --git a/paper/sections/06-formalization-architecture.tex b/paper/sections/06-formalization-architecture.tex new file mode 100644 index 0000000..bc651c9 --- /dev/null +++ b/paper/sections/06-formalization-architecture.tex @@ -0,0 +1,44 @@ +\section{Formalization architecture} +\label{sec:architecture} + +The proof is intentionally presented as a six-stage spine rather than as a catalogue of every repository feature. Table~\ref{tab:spine} maps each paper-level step to the principal Lean module and declarations. + +\begin{table}[ht] +\centering +\small +\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.07\linewidth}>{\raggedright\arraybackslash}p{0.31\linewidth}>{\raggedright\arraybackslash}p{0.54\linewidth}@{}} +\toprule +Stage & Paper-level role & Principal module and declarations \\ +\midrule +1 & Normalized free-simplex path probability, its finite-mass scaled reference (sector mass $T^n/n!$), and simplex volume & \file{ContinuousTimeJumpSimplex.lean}:\newline \mbox{\lean{Simplex.volume_freeSimplexSet}},\newline \mbox{\lean{Simplex.sum_holdingTimesOfFree}} \\ +\addlinespace +2 & Sector masses, tail disappearance, and normalization & \file{ContinuousTimeJumpFiniteGeneratorPathLaw.lean}:\newline \mbox{\lean{tendsto_arrivalMassFrom}}, \mbox{\lean{tsum_sectorMassFrom}} \\ +\addlinespace +3 & Actual probability measure and terminal-coordinate bridge & \file{ContinuousTimeJumpFiniteGeneratorFullPath.lean}:\newline \mbox{\lean{pathLawFrom}}, \mbox{\lean{instIsProbabilityMeasurePathLawFrom}},\newline \mbox{\lean{pathLawFrom_terminalState_singleton}} \\ +\addlinespace +4 & Matrix-exponential terminal law and Markov semigroup & \file{ContinuousTimeJumpFiniteGeneratorBridge.lean}:\newline \mbox{\lean{pathLawFrom_terminalState_eq_exp_generator}},\newline \mbox{\lean{transitionKernel_add}} \\ +\addlinespace +5 & Finite-dimensional distributions & \file{ContinuousTimeJumpFiniteDimensional.lean}:\newline \mbox{\lean{pathLawFrom_finiteDimensional_eq}},\newline {\footnotesize\mbox{\lean{pathLawFrom_sampleAt_real_singleton_eq_exp_product}}} \\ +\addlinespace +6 & Global driven path law and fluctuation relations & \file{ContinuousTimeJumpDrivenConcat.lean}, \file{ContinuousTimeJumpDrivenGlobalLaw.lean}, \file{ContinuousTimeJumpDrivenGlobalCrooks.lean}:\newline \mbox{\lean{concatenateWindows}}, \mbox{\lean{forwardGlobalLaw}},\newline \mbox{\lean{global_crooks_of_gibbsDetailedBalance}},\newline \mbox{\lean{global_jarzynski_of_gibbsDetailedBalance}},\newline \mbox{\lean{global_second_law_of_gibbsDetailedBalance}},\newline {\scriptsize\lean{global_work_distribution_crooks_reverseWork_of_gibbsDetailedBalance}} \\ +\bottomrule +\end{tabular} +\caption{The paper theorem spine. All modules live under \file{CrooksJarzynski/}.} +\label{tab:spine} +\end{table} + +Three design choices are especially important. + +\paragraph{Library conventions at the semigroup bridge.} +Mathlib writes kernel composition so that the rightmost kernel acts first; this accounts for the formal order in $K_{S+T}=K_T\circ K_S$. Path-law masses live in the extended nonnegative reals, while matrix-exponential entries are real, so the bridge theorem applies the \lean{toReal} coercion to the finite singleton mass before comparing it with $\exp(TQ)(x,y)$. + +\paragraph{Measure identities rather than path-probability ratios.} +The abstract relation is an equality of measures after \lean{withDensity}. This avoids division by zero and lets the same API support discrete, continuous, and pushed-forward work laws. + +\paragraph{Explicit bridges between arithmetic and measures.} +Sector sums, renewal functions, and matrix entries are useful intermediate objects, but every headline theorem is phrased against the constructed path law or one of its pushforwards. Dedicated bridge lemmas prevent an accidental gap between a numerical calculation and a statement about the probability measure. + +\paragraph{Marked construction before global projection.} +Window marks retain enough structure to prove boundary matching and windowwise balance. Only after those facts are available are the marks measurably concatenated into a global path. This separates recursive probability construction from real-time observation while proving that their work observables agree almost surely. + +The implementation uses \Lean\ \parencite{Moura2021}, Mathlib \parencite{Mathlib2020}, and Physlib \parencite{Physlib}. The snapshot underlying this draft pins Lean and Mathlib to version 4.32.0 and pins Physlib by commit. The CI workflow builds the project, scans the project sources for proof placeholders and explicit axiom or constant declarations, and audits the kernel axioms of selected headline theorems. The accepted foundational axioms are the standard \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound} used by the Lean/Mathlib environment. diff --git a/paper/sections/07-examples.tex b/paper/sections/07-examples.tex new file mode 100644 index 0000000..3086a9c --- /dev/null +++ b/paper/sections/07-examples.tex @@ -0,0 +1,93 @@ +\section{Examples and physical interpretation} +\label{sec:examples} + +The repository contains several concrete instances that exercise distinct parts of the general construction. + +\paragraph{Symmetric two-state chain.} +For the unit-rate alternating chain, the $n$-jump sector has mass $e^{-T}T^n/n!$. The sector masses sum to one, the jump-count law is Poisson, and the terminal distribution is the parity-filtered row of $\exp(TQ)$. This example checks normalization and the semigroup bridge against an explicit calculation. + +\paragraph{Asymmetric reversible two-state quench.} +In units where $k_{\mathrm B}T=1$ (so $\beta=1$), on states $\{0,1\}$, take +\[ + E_0(0)=0,\qquad E_0(1)=-\log 2, + \qquad E_1(0)=E_1(1)=-\log 3, +\] +with rates $k(0,1)=2$ and $k(1,0)=1$. The partition functions are $Z_0=3$ and $Z_1=6$, hence $\Delta F=-\log 2$. The initial Gibbs law is $(1/3,2/3)$, and it is stationary under the rates $k(0,1)=2$, $k(1,0)=1$. Because the only energy switch occurs after the dynamical window, the work distribution is independent of the window duration: +\[ + \Pp_F(W=-\log 3)=\frac13, + \qquad + \Pp_F\left(W=-\log\frac32\right)=\frac23. +\] +Hence +\[ + \left\langle e^{-W}\right\rangle_F + =\frac13\cdot3+\frac23\cdot\frac32 + =2=e^{-\Delta F}, + \qquad + \langle W\rangle_F-\Delta F + =\frac13\log\frac{32}{27}>0. +\] +The final landscape is flat, so the reverse experiment starts from the uniform Gibbs distribution, and its initial mirrored quench gives +\[ + \Pp_R(W_R=\log 3)=\frac12, + \qquad + \Pp_R\!\left(W_R=\log\frac32\right)=\frac12. +\] +The atomwise Crooks relation~\eqref{eq:atom-crooks} can therefore be checked value by value: +\[ + \frac{\Pp_F(W=-\log 3)}{\Pp_R(W_R=\log 3)} + =\frac{1/3}{1/2}=\frac23 + =e^{-\log 3-\Delta F}, + \qquad + \frac{\Pp_F\bigl(W=-\log\tfrac32\bigr)}{\Pp_R\bigl(W_R=\log\tfrac32\bigr)} + =\frac{2/3}{1/2}=\frac43 + =e^{-\log\frac32-\Delta F}, +\] +so the example checks the path-to-work Crooks sign conventions directly, in addition to Jarzynski's equality. The common offset $-\log 3$ in the final landscape is an energy-gauge choice: adding $+\log 3$ to both final-state energies shifts every value of $W$ and $\Delta F$ by the same amount while leaving the dissipated work $W-\Delta F$, the Crooks exponent, and Jarzynski's equality unchanged. In the shifted gauge $E_1=(0,0)$, the forward work values are $0$ and $\log 2$ with probabilities $1/3$ and $2/3$, and $\Delta F=\log\frac32$. This one-window example is thus a sign-convention test: a stationary Gibbs state followed by a single quench, rather than a nontrivial finite-time relaxation. The formalization obtains the path-space Crooks relation and its work-distribution corollary for this model, together with an entropy-production integral fluctuation theorem, and recovers the model as a one-window instance of the general driven construction. + +\paragraph{Branching and history-dependent work.} +A three-state Y-shaped chain uses +\[ + Q= + \begin{pmatrix} + -2 & 1 & 1\\ + 1 &-1 & 0\\ + 1 & 0 &-1 + \end{pmatrix}, + \qquad 1\leftrightarrow0\leftrightarrow2. +\] +This is the smallest reversible network with a genuine branching choice: from the hub state $0$, a jump can reach either leaf, so the chain is not a telegraph process, and its symmetric rates make the uniform distribution stationary. The branching at state $0$ is why jump-count parity arguments from the two-state alternating chain do not apply; this generator validates the general terminal-law theorem beyond that special case. + +A separate two-window three-state protocol on the same Y-shaped network is fully specified as follows: energy landscapes +\[ + (0,0,0)\longrightarrow(0,\log 2,0)\longrightarrow(0,0,0) +\] +at inverse temperature $\beta=1$; initial distribution the uniform Gibbs state of the flat landscape; arbitrary durations $T_0,T_1>0$; first-window generator the symmetric Y-shaped generator above, with unit rates on the edges $0\leftrightarrow1$ and $0\leftrightarrow2$; and second-window generator identical except that the rate out of the raised state is doubled, $k(1,0)=2$: the rate ratio compensates the Gibbs weight $e^{-\log 2}=1/2$ of the raised state, which is detailed balance~\eqref{eq:gibbs-db} in concrete form. Here $0\to1\to0$ denotes the boundary-state triple $(X_{s_0},X_{s_1},X_{s_2})$, not the complete sequence of microscopic jumps. The resting history $0\to0\to0$ has $W=0$. The history $0\to1\to0$ has $W=\log 2$, because the first switch raises state $1$ while the second switch occurs after the process has returned to state $0$. Both histories have the same endpoint pair $(0,0)$, and both have positive probability for positive window durations (\lean{work_zero_same_endpoints_event_pos}, \lean{work_log_two_same_endpoints_event_pos}). Consequently, the work is not determined almost surely by the overall initial and final states (\lean{work_not_ae_initialFinalFunction}): the intermediate window-boundary history is essential, even though the work observable~\eqref{eq:work} itself reads only window-boundary states. + +\paragraph{Endpoint data do not determine interior observations.} +Retaining complete window paths serves a strictly stronger purpose than computing work: constructing and observing a single global real-time trajectory and proving path-level pushforward identities. For the unit-rate symmetric two-state chain, the exact transition probabilities are +\[ + p_{00}(t)=\frac{1+e^{-2t}}{2}, + \qquad + p_{01}(t)=\frac{1-e^{-2t}}{2}, +\] +with $p_{10}=p_{01}$ and $p_{11}=p_{00}$. For $T>0$, under the law started from $X_0=0$, the two relevant joint masses are +\[ + \Pp_{T,0}(X_{T/2}=0,\,X_T=0) + =p_{00}(T/2)^2>0, +\] +and +\[ + \Pp_{T,0}(X_{T/2}=1,\,X_T=0) + =p_{01}(T/2)\,p_{10}(T/2)>0. +\] +Conditioning on the complete endpoint pair therefore leaves the midpoint genuinely random: +\[ + 0< + \Pp\bigl(X_{T/2}=1\,\big|\,X_0=0,\,X_T=0\bigr) + =\frac{p_{01}(T/2)^2}{p_{00}(T)} + <1 . +\] +These are the concrete finite-dimensional atoms behind the interior-time theorem. For $T>0$, within the endpoint event $(X_0,X_T)=(0,0)$, both midpoint values occur with positive probability, so the midpoint state is not almost surely equal to any measurable function of the endpoint pair (\lean{trajectory_interior_not_ae_endpointFunction}). Endpoint-only records are therefore insufficient for general path-level observables; the present construction retains complete window paths so that the global real-time trajectory and its finite-time observations remain available. + +Together these examples illustrate normalization, branching, physical parameterization, work sign conventions, and the distinction between endpoint and path information. diff --git a/paper/sections/08-related-work.tex b/paper/sections/08-related-work.tex new file mode 100644 index 0000000..9086f40 --- /dev/null +++ b/paper/sections/08-related-work.tex @@ -0,0 +1,24 @@ +\section{Related work} +\label{sec:related} + +\subsection{Stochastic thermodynamics and Markov jump processes} + +The fluctuation relations formalized here are classical. Jarzynski established the nonequilibrium work equality and derived it in a master-equation formalism \parencite{Jarzynski1997PRL,Jarzynski1997PRE}. Crooks related forward and reverse path probabilities for microscopically reversible Markovian dynamics and derived both work and free-energy relations \parencite{Crooks1998,Crooks1999,Crooks2000}. Path-space formulations of entropy production for Markov processes were developed by Lebowitz and Spohn, Maes and Neto\v{c}n\'y, and Seifert \parencite{LebowitzSpohn1999,MaesNetocny2003,Seifert2005,MaesNetocnyWynants2008}. Standard treatments relate trajectory-level work, entropy production, and fluctuation theorems \parencite{Seifert2012,VandenBroeckEsposito2015}. Time-dependent finite-state jump processes and detailed fluctuation theorems are standard subjects in stochastic thermodynamics \parencite{ShargelChou2009,RaoEsposito2018,PelitiPigolotti2021}; local detailed balance and its physical scope are reviewed by \textcite{Maes2021}. Our contribution is not a new fluctuation identity, but a machine-checked construction connecting the identities to explicitly constructed path measures. + +\subsection{Continuous-time Markov-chain path laws} + +The embedded jump chain, exponential holding times, explosion theory, Kolmogorov equations, and $P_t=\exp(tQ)$ are standard \parencite{Norris1997}. Explicit path densities on disjoint unions of finite jump records combine jump-rate factors with integrated escape rates \parencite{RaoTeh2013}. The free-simplex chart and the transition-matrix product are therefore not claimed as new mathematics. The formal contribution is that the normalized sector sum is an actual path law whose terminal and finite-dimensional pushforwards are identified with the matrix-exponential kernels, and that the same law is then used as the window dynamics of a physical driven protocol. + +\subsection{Mechanized probability and CTMCs} + +Mechanized Markov-process theory predates this work. H\"olzl constructed discrete-time Markov processes and jump-and-hold continuous-time chains in Isabelle/HOL, proving the Markov property, a transition semigroup, and a backward equation; the current Archive of Formal Proofs session (in its \file{Continuous_Time_Markov_Chain} theory) also contains an almost-sure non-explosion result under bounded escape rates \parencite{Hoelzl2017,AFPMarkovModels}. In Lean, Marion formalized the Ionescu--Tulcea theorem in Mathlib, providing general trajectory-measure infrastructure \parencite{Marion2025}. + +The closest Lean CTMC comparison is Ripple, which develops finite-state Q-matrices, exponential holding times, matrix-exponential transition probabilities, a canonical Ionescu--Tulcea jump-hold law, and conditional non-explosion results for an infinite record construction \parencite{Ripple2026}. Our work does not claim the first Lean CTMC or jump-hold law. In the Ripple snapshot reviewed for this paper, we did not identify a theorem equating the terminal pushforward of its canonical law with its matrix-exponential transition API, finite-dimensional pushforward identifications, or a stochastic-thermodynamic driven layer. This is a snapshot-specific search result, not a proof of absence. + +\subsection{Mechanized fluctuation relations and physics} + +Lean has been applied to chemical physics, equilibrium thermodynamics, and canonical ensembles through LeanChemicalTheories and Physlib \parencite{Bobbin2024,Physlib}. Concurrently, the PhysicsAI DFT moment-body development formalizes the detailed fluctuation theorem as a measure identity and derives the integral fluctuation theorem, second-law and moment consequences, and finite-support Crooks pairs \parencite{PhysicsAIDFT}. That development assumes a DFT law and studies its consequences. The present work instead constructs forward and reverse laws from finite-state generators and windowwise Gibbs detailed balance. The two projects are therefore complementary: one analyzes distributions satisfying a fluctuation symmetry, while the other derives the physical symmetry on global path measures built from explicit dynamics. + +\subsection{Positioning statement} + +To our knowledge, among the public Lean~4 and Mathlib artifacts reviewed at the fixed snapshots recorded in the bibliography (search completed on 26 August 2026 and quality-checked on 27 August 2026), we did not identify a development connecting all of the following in one machine-checked construction: normalized fixed-horizon path measures for finite-state jump generators, disappearance of the finite-horizon jump-count tail, terminal and finite-dimensional identification with the matrix-exponential semigroup, measurable concatenation of finitely many piecewise-constant protocol windows, and global Crooks--Jarzynski work relations. This statement is deliberately limited to the reviewed public artifacts and snapshots. It is not a priority claim over all theorem provers, and none of the underlying physical laws or standard CTMC identities is claimed as new. diff --git a/paper/sections/09-limitations.tex b/paper/sections/09-limitations.tex new file mode 100644 index 0000000..65acdbd --- /dev/null +++ b/paper/sections/09-limitations.tex @@ -0,0 +1,17 @@ +\section{Limitations and future work} +\label{sec:limitations} + +The fully connected continuous-time result has a deliberately narrow scope. + +\begin{itemize}[leftmargin=*] + \item The state space is finite. Countably infinite and general measurable state spaces are not covered by the continuous-time generator-to-path-law bridge. + \item The horizon is finite, and non-explosion is proved as disappearance of the finite-horizon jump-count tail. The project does not construct a single infinite-time path law for the general generator. + \item Driving consists of finitely many piecewise-constant windows. General calendar-time-dependent rates with integrated hazards are not formalized. + \item Diffusions, Langevin dynamics, stochastic differential equations, and their path measures are outside the present development. + \item Models with odd variables, magnetic fields, or a nontrivial state-space time-reversal involution are outside the present scope \parencite{SpinneyFord2012}. + \item Heat and a trajectory-level first law are not formalized; Section~\ref{sec:driven} records only their physical interpretation relative to the implemented switching-work convention. + \item The reverse dynamics and windowwise detailed-balance hypotheses are supplied in the modeled protocol; reverse-kernel existence by disintegration is not a theorem of the continuous-time layer. + \item Record reversal is identified with the c\`adl\`ag time mirror pointwise, almost surely at fixed times, and for windowwise finite-dimensional distributions; a single global mirror statement for arbitrary observation times across window seams is not formalized. +\end{itemize} + +The immediate priority is to archive the present finite-state result under a versioned repository snapshot with a persistent identifier. Subsequent work may address countable state spaces, genuinely time-inhomogeneous hazards, and diffusion limits. diff --git a/paper/sections/10-artifact.tex b/paper/sections/10-artifact.tex new file mode 100644 index 0000000..556c121 --- /dev/null +++ b/paper/sections/10-artifact.tex @@ -0,0 +1,16 @@ +\section{Artifact and reproducibility} +\label{sec:artifact} + +The core formalization described in Sections~\ref{sec:setting}--\ref{sec:driven} is based on the repository at commit \artifactbase, on the branch from which this manuscript is built. The manuscript source, bibliography, reader-facing related-work review, theorem map, artifact guide, and the interior-time theorem of Section~\ref{sec:examples} are contained in the artifact commit from which this PDF is built; that commit extends \artifactbase{} and lives in the same repository. A release version should replace both commit references with a single versioned artifact tag and archival DOI, so that one checkout reproduces every Lean declaration cited here together with this manuscript. + +Beyond the continuous-time chain presented in this paper, the repository also contains a broader discrete-time measure-theoretic development, non-atomic Gaussian and Metropolis--Hastings examples, two-state calculations, and a refinement theorem relating two discrete work conventions. Those components support and test the library but are not part of the claims of this paper. + +The principal verification commands are: +\begin{verbatim} +lake exe cache get +lake build +lake env lean CrooksJarzynski/AxiomAudit.lean +lake env lean CrooksJarzynski/AxiomAuditDriven.lean +\end{verbatim} +The project is pinned by \file{lean-toolchain}, \file{lakefile.lean}, and \file{lake-manifest.json}. A separate continuous-integration workflow builds this manuscript with \lean{latexmk} and \lean{biber} in a TeX~Live container and publishes the PDF as a build artifact; the release version should pin the container image by digest. The detailed paper-to-declaration map is in \file{FORMALIZATION.md}; driven-layer design notes are in \file{DRIVEN_PROTOCOL.md}; and \file{ARTIFACT.md} gives a reviewer-oriented route through the six-stage theorem spine. + diff --git a/paper/sections/11-conclusion.tex b/paper/sections/11-conclusion.tex new file mode 100644 index 0000000..bbd55ab --- /dev/null +++ b/paper/sections/11-conclusion.tex @@ -0,0 +1,6 @@ +\section{Conclusion} + +We have presented a Lean~4 construction that closes the chain from finite-state jump generators to global stochastic-thermodynamic fluctuation relations. Explicit fixed-horizon sectors are normalized into a probability measure; the actual terminal and finite-dimensional pushforwards of that measure are identified with the matrix-exponential semigroup; complete window paths are concatenated into global real-time trajectories; and windowwise Gibbs detailed balance yields Crooks, Jarzynski, work-distribution, and average-work second-law theorems on those global laws. + +The formalization does not make classical physics new. Its contribution is to make the interfaces between standard pieces explicit, typed, measurable, normalized, and machine checked. Those interfaces---between sector arithmetic and path measures, path measures and semigroups, marked windows and global trajectories, and dynamics and fluctuation identities---are the central result. +