A sharp universal skewness bound for unicyclic currents

Dev D. Goyal

A sharp universal skewness bound for unicyclic currents

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Ptaszyński's conjectured interval −1/16 ≤ C₃/C₁ ≤ 1 for unicyclic Markov currents
Posed in: K. Ptaszyński, Phys. Rev. E 106, 024119 (2022), Eq. (21)
Status: Proved
Result: For the net crossing count of a marked edge on every finite bidirectional Markov ring with n ≥ 3 states, positive rates and unequal forward and reverse rate products, −1/16 ≤ C₃/C₁ ≤ 1, and both constants are sharp.

Abstract

The net marked-edge current on every finite bidirectional Markov ring with at least three states, positive rates and unequal forward and reverse rate products satisfies −1/16 ≤ C₃/C₁ ≤ 1. The two-channel two-state case has the stronger interval [1/4,1]. This ratio is not standardized skewness.

Details

Year: 2026
Discipline: Mathematical physics
Area: Stochastic thermodynamics
Subject: Stochastic thermodynamics
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: unicyclic-skewness
Keywords: stochastic thermodynamics, current fluctuations, skewness, Markov rings, unicyclic networks, cumulants

Statement and scope

Formal scope. The interval for actual tilted-matrix derivatives and a local branch is formalized. Identification with long-time stochastic cumulants and sharpness have conventional proofs. Lean does not construct a continuous-time sample-path probability space or a separate optimizing-sequence theorem.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 369 KB
PDF on GitHub: papers/physics/unicyclic-skewness/manuscript.pdf
LaTeX source: papers/physics/unicyclic-skewness/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/physics/unicyclic-skewness/

Lean project

papers/physics/unicyclic-skewness/proof/ 34 Lean files

Lakefile

papers/physics/unicyclic-skewness/proof/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

proof/AllResults.lean

Reproduce

The commands below are quoted from papers/physics/unicyclic-skewness/README.md, which gives their context and working directory.

Read and reproduce

unicyclic_output="$(mktemp -d)"
python3 verify.py --mathlib /path/to/mathlib4 \
  --lean-bin /path/to/lean-4.19.0-linux/bin --output "$unicyclic_output"
python3 check_certificate.py

README: papers/physics/unicyclic-skewness/README.md
Verification record: papers/physics/unicyclic-skewness/VERIFICATION.md
Formalization notes: papers/physics/unicyclic-skewness/FORMALIZATION.md
Authorship: papers/physics/unicyclic-skewness/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. The Omega Institute's public repository records the minimum skewness for unidirectional cycles, with infimum −1/16, committed on 26 October 2026 (issue #22468). The bidirectional two-sided interval here is a different question. Priority and novelty record.

Source. Prior results and source-comparison limits are stated in the manuscript. Historical priority is not certified.

Questions and answers

Is Ptaszyński's skewness conjecture for unicyclic currents proved?

This preprint proves the interval −1/16 ≤ C₃/C₁ ≤ 1 proposed in Eq. (21) of Ptaszyński (2022) for the net crossing count of one edge of a bidirectional Markov ring with at least three states, strictly positive rates and nonzero affinity, and shows that both constants are sharp. It does not settle that paper's separate kurtosis, joint-cumulant or fixed-ring-size questions, and C₃/C₁ is a ratio of cumulants per unit time, not standardized skewness.

Is the proof formally verified?

Lean 4 verifies the interval for the derivatives of the actual tilted-generator eigenvalue branch, including existence of that local branch. The identification of these derivatives with long-time stochastic cumulants and the sharpness argument are conventional proofs in the manuscript and are not formalized.

What earlier results does the proof rely on?

The positive midpoint spectrum is due to Pietzonka, Barato and Seifert, the thermodynamic uncertainty relation is established prior work, and the extremizing family was already identified by Ptaszyński. The new ingredient is an exact two-variable polynomial inequality certified with integer coefficients; bibliographic priority is not established.

Was any part of this bound proved earlier?

The unidirectional special case of the lower side was proved earlier: the Omega Institute's public repository records the exact minimum skewness for unidirectional cycles, with infimum −1/16, committed on 26 October 2026 (issue #22468). The bidirectional two-sided interval here is a different question.

Cite

Citation file papers/physics/unicyclic-skewness/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026unicyclicskewness,
  author = {Goyal, Dev D.},
  title = {A Sharp Universal Skewness Bound for Unicyclic Currents},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory}
}