Papers With

← All papers
First page of What the occupation law of a finite Markov chain determines: time reversal and principal minors

What the occupation law of a finite Markov chain determines: time reversal and principal minors

Arjun Pemmasani

math.PR Nov 10, 2026 · v1 math.RA
formalization mathlib probability algebra
Read PDF arXiv abstract Code
TL;DR
Finite and algebraic proof steps are formalized in Lean 4 with Mathlib in ancillary files, assuming a Perron–Frobenius null-vector hypothesis; the Lean code was AI-generated.
Abstract
What does the occupation law of a finite Markov chain determine about its generator $Q$? From the stationary start, the law of the occupation times at one time determines $Q$ exactly up to time reversal and reversals of memoryless blocks, the sets of states that are all left at one rate with one landing law and are entered in proportion to the stationary law. These reversals commute and give exactly $2^k$ generators, with $k$ read off a tree of memoryless blocks. This leaves only time reversal when $Q$ has no rank-one cut, when there are at most 4 states, and generically. The law at one time determines the law at every time, and a generic start determines $Q$. A renewal block is a set of states that is left at the same rates from each of its states, is entered with one law, and is charged by the start in proportion to that law. From every start the law determines $Q$ exactly up to lumped reversals, which lump disjoint renewal blocks to single states and reverse a memoryless block of the lumped chain. We also find every start that hides time reversal. At the scale of large deviations, the functional of Donsker and Varadhan determines exactly the principal minors of $-Q$.
Problem

The paper asks what the law of the occupation times of a finite continuous-time Markov chain determines about its generator Q, both exactly and at the large-deviation scale given by the Donsker–Varadhan functional.

Approach

Occupation laws are reduced to the rational function μ(diag x − Q)^{-1}1. Irreducibility of multiaffine determinant polynomials (Al Ahmadieh, Hartfiel–Loewy) and Loewy's theorem on principal minors, applied to a generator bordered by the start, are used to characterize the generators with equal laws. Explicit examples are checked in exact arithmetic with Python scripts. Finite and algebraic steps are formalized in Lean 4 with Mathlib, with the Perron–Frobenius positive null vector taken as a hypothesis.

Results

From the stationary start, one-time occupation law determines Q up to (Z/2)^k, generated by time reversal and commuting reversals of memoryless blocks; generically only time reversal remains. From any start, Q is determined up to lumped reversals, and the Donsker–Varadhan functional determines exactly the principal minors of −Q.

ObservationWhat it determinesSource
the pathQ
law of O(T) at one T, start μ without renewal blocksQ if μ≠π; Q up to time reversal if μ=πThm. B
law of O(T) at one T, stationary startQ up to (Z/2)^k (time reversal and memoryless-block reversals)Thm. A
law of O(T) at one T, any start μQ up to lumped reversalsThm. B
functional J_Vprincipal minors of −QProp. 1.1
What observations of a finite irreducible chain determine about its generator