Theorem E.1 — exact regular-language pair sampling

Proved

FSS23105365.pair_sampling

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

finite-staterandomized-ac0sampling

For every binary DFA $A$ with $q$ states, there are natural constants $D,C,k$ such that for every $n\geq0$ , a Boolean circuit supplied with exactly $n$ fair bits outputs $(X,A(X))$ exactly, where $X$ is uniform on $\{0,1\}^n$ . Its depth is at most $D$ and its size is at most $C(n+1)^k$ . The extra output bit is the accepting-state indicator; acceptance membership need not be in $\mathrm{AC}^0$ .

Preamble

import Definitions.Def_FSS23105365_FiniteState
set_option autoImplicit false

Formal statement

namespace FSS23105365
theorem pair_sampling (q : ℕ) (A : BinaryDFA q) :
    ∃ D C k : ℕ, ∀ n : ℕ, ∃ S : Circuit (Option (Fin n)),
      S.randomBits = n ∧ S.depth ≤ D ∧ S.size ≤ C * (n + 1) ^ k ∧
      ExactLaw S pairOutcomeEncode (pairLaw A) := 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, Theorem E.1, printed p. 33; seed bound in Appendix E.1 and Proposition 3.2.

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