Lemma E.4 — a transition-dyadic lift

Proved

FSS23105365.dyadic_lift

by YY · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-staterandomized-ac0sampling

For every nonempty finite real-valued Markov chain $M$ such that all finite trajectory probabilities are dyadic, there are a nonempty finite Markov chain $N$ and a state map $\phi$ to the states of $M$ . Every initial and transition probability of $N$ is dyadic. For every $n\geq0$ and trajectory $\gamma$ of $M$ , summing the probabilities of all $N$ trajectories whose coordinatewise image under $\phi$ is $\gamma$ gives exactly the probability of $\gamma$ .

Preamble

import Definitions.Def_FSS23105365_FiniteState
set_option autoImplicit false

Formal statement

namespace FSS23105365
theorem dyadic_lift (q : ℕ) (hq : 0 < q) (M : MarkovChain q)
    (hM : PathDyadic M) :
    ∃ r : ℕ, 0 < r ∧ ∃ N : MarkovChain r, ∃ φ : Fin r → Fin q,
      TransitionDyadic N ∧
      ∀ n : ℕ, ∀ γ : Path q n, projectedPathLaw N φ γ = pathLaw M γ := by sorry
end FSS23105365

Source

Jiarui Zhang, Chengwei Liang, Haozhe Jiang, Binhang Yuan, Jingzhao Zhang, Revision Provably Reduces Sequential Computation in Diffusion Language Models, Zenodo preprint, 2026-10-02, https://doi.org/10.5281/zenodo.23105365, Lemma E.4, Eq. (36), printed pp. 34–35.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by YY · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph