Invariant, reversible and convergent are different claims

Markov Chain Monte Carlo · natural-language: L1 (author-assigned; calibration pending)

Why this difficulty?

Distinguish three standard finite-chain definitions and keep the Markov normalization explicit.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

No aligned Lean view is admitted for the row-vector/matrix formulation, detailed-balance-to-invariance summation under stochastic normalization, event-TV convergence definition, or identity-matrix illustration. No irreducibility, aperiodicity, rate or general-state ergodic theorem is certified.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

P is a finite row-stochastic transition matrix: \(P(x,y)\ge 0\) and \(Σ_{y}\) \(P(x,y)=1\). \(π\) and \(ρ\) are probability row vectors. Use total variation when discussing convergence.

Natural-language question

Write the identities defining invariance and detailed balance for \(π\). State what convergence from \(ρ\) means in this setting. Which identity controls one step started exactly in \(π\), and why is that not the definition of convergence from an arbitrary start?

Reference mathematical proof

Invariance is \(πP=π\), or \(Σ_{x}\) \(π(x)P(x,y)=π(y)\) for each y. Starting exactly in \(π\) therefore gives the same law after one step.
Detailed balance is \(π(x)P(x,y)=π(y)P(y,x)\) for every x,y. Summing over x and using the row sum of P at y yields invariance; the stochastic normalization is part of that deduction.
Convergence from \(ρ\) is \[\operatorname{TV}(\rho P^t,\pi)\longrightarrow0\quad(t\to\infty).\] It concerns an entire sequence of laws from the specified start, not just the identity \(πP=π\).
For the identity matrix P, every \(π\) is invariant and reversible, but \(ρP^t=ρ\) for all t. If \(ρ\ne π\), convergence to \(π\) fails. Thus one-step invariance is not a definition of general-start convergence.

Formal support and missing Lean alignment

The local atomic-balance result supports the reversibility notion. The finite-matrix definition comparison and identity-kernel example have no admitted aligned Lean view here.

Assessment rubric · 4 points

States \(πP=π\) with the correct one-step meaning. (1 point)
States pairwise detailed balance and retains row-stochastic normalization. (1 point)
Defines convergence from \(ρ\) as a limit of its time-t output laws in the given metric. (1 point)
Does not substitute invariance or reversibility for an arbitrary-start convergence statement. (1 point)

Lean view: not yet aligned

The local atomic-balance result supports the reversibility notion. The finite-matrix definition comparison and identity-kernel example have no admitted aligned Lean view here.

This support theorem does not certify the complete QA or its explanatory counterexamples.

What this does—and does not—verify

No irreducibility, aperiodicity, mixing-rate theorem or general-state-space ergodic theorem is proved.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original finite-chain terminology exercise with an elementary identity-matrix illustration.

Exact local source and full context · Locate the owning module (declaration not yet indexed in this graph)

AutoSamplingTheory.TechnicalLemmas.Probability.KernelReversibility.isReversible_of_singleton_balance

ASTIS formal support (not an equivalent QA)

Mathlib facts / definitions

Binding SHA-256: 8b10bef6bc3088ea8188089bb960aed747ddeded576261956464483947b6db38