Math and Theory

A three-state thermal counterexample to a heat-current kurtosis conjecture

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

Problem and result

Problem
Ptaszyński's heat-current kurtosis bound C₄/C₂ ≥ 0 for thermal Markov systems
Posed in
Ptaszyński, Physical Review E 106, 024119 (2022), Eq. (19)
Status
Counterexample
Result
An explicit three-state, two-bath thermal rate model with local detailed balance has spectral heat-cumulant ratio C₄/C₂ = −3470947982622836/176627429595846691 < 0, contradicting Eq. (19) in its tilted-generator form.

Abstract

A three-state model with two positive-temperature baths satisfies local detailed balance and has positive total off-diagonal transition rates. Its dominant tilted-generator eigenvalue has fourth-to-second derivative ratio −3470947982622836/176627429595846691. This refutes the thermal nonnegativity proposal in its finite spectral formulation. The proof constructs a smooth local eigenvalue branch, proves strict dominance over distinct complex eigenvalues, and calculates the exact derivatives.

Details

Year
2026
Discipline
Mathematical physics
Area
Stochastic thermodynamics
Subject
Stochastic thermodynamics
Result type
Exact finite spectral counterexample
Formal proof
Standalone Lean package
Family
thermal-kurtosis-counterexample
Keywords
stochastic thermodynamics, heat current, full counting statistics, kurtosis, Markov jump processes, counterexample

Statement and scope

Result summary. A three-state two-temperature thermal rate model satisfies local detailed balance and has an exact negative fourth-to-second cold-heat spectral cumulant ratio. Lean checks the finite matrices, complex spectrum, a smooth locally dominant eigenvalue branch, and the exact derivative ratio. It does not formalize the stochastic long-time identification theorem.

Formal scope. The standalone package uses Lean 4.19.0. It does not formalize the stochastic long-time theorem that identifies the eigenvalue branch with a cumulant generating function. The witness does not refute the separate skewness conjecture or establish a minimal number of states.

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 304 KB
PDF on GitHub
papers/physics/thermal-kurtosis-counterexample/report.pdf
LaTeX source
papers/physics/thermal-kurtosis-counterexample/report.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/thermal-kurtosis-counterexample/ 1 Lean file
Lean sources

Reproduce

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

Reproduce the Lean check

git clone --depth 1 --branch v4.19.0 https://github.com/leanprover-community/mathlib4.git mathlib4
git -C mathlib4 rev-parse HEAD

Reproduce the Lean check

lake env lean /absolute/path/to/ThermalKurtosis.lean

Reproduce the Lean check

bash /absolute/path/to/verify.sh "$PWD"

Independent arithmetic check

python3 model_check.py
python3 test_verifiers.py

The same file gives further commands.

README
papers/physics/thermal-kurtosis-counterexample/README.md
Verification record
papers/physics/thermal-kurtosis-counterexample/VERIFICATION.md
Related work
papers/physics/thermal-kurtosis-counterexample/RELATED_WORK.md
Repository guide
verification/README.md
Unfinished proofs
UNFINISHED.md

Source and prior work

Original problem. Ptaszyński, Physical Review E 106, 024119 (2022), Eq. (19). The finite thermal spectral model is specified in Eqs. (63)–(70).

Prior work. A Zenodo record (10.5281/zenodo.23689958), created on 27 October 2026 at 12:29 UTC, refutes the signs of both C₃/C₁ and C₄/C₂; my first commit of this result is about six and a half hours earlier. No priority is claimed. Priority and novelty record.

Questions and answers

Is Ptaszyński's heat-current kurtosis conjecture true?

Not in the finite tilted-generator formulation of Phys. Rev. E 106, 024119 (2022): this preprint gives a three-state, two-temperature model with local detailed balance whose spectral ratio is C₄/C₂ = −3470947982622836/176627429595846691. It does not refute the separate skewness conjecture, Eq. (20), and gives no minimal-state result or optimal negative bound.

Were negative fourth cumulants of currents known before?

Yes. Negative fourth cumulants of general driven Markov currents (for example Gerry and Segal, 2023) and three-level thermal models (Segal, 2018) are prior work; the contribution here is an explicit thermal witness with two positive-temperature baths satisfying local detailed balance.

Is the proof formally verified?

Lean 4 verifies the finite matrices, local detailed balance, the complex spectrum, a smooth strictly dominant eigenvalue branch and its exact derivatives. It does not formalize the standard long-time stochastic theorem that identifies this branch with the cumulant generating function.

Has anyone else refuted this kurtosis sign conjecture?

Yes. A Zenodo record (10.5281/zenodo.23689958), created on 27 October 2026 at 12:29 UTC, gives three-state counterexamples to the signs of both C₃/C₁ and C₄/C₂ with both ratios unbounded below. This result was first committed here about six and a half hours earlier; no priority is claimed.

Cite

Citation file papers/physics/thermal-kurtosis-counterexample/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{Goyal2026ThermalKurtosis,
  author = {Goyal, Dev D.},
  title = {A three-state thermal counterexample to a heat-current kurtosis conjecture},
  year = {2026},
  month = oct,
  howpublished = {Preprint},
  version = {1.0.0},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/thermal-kurtosis-counterexample},
  note = {Preprint}
}

↑ ↓ move · Enter open · Esc close