# Verification report for the Eulerian moving target bound

Author: Alper Ferudun, Mercury Software GmbH. Version 1.0, 6 October 2026.

## Accepted mathematical scope

For the half-lazy simple walk on every connected loopless Eulerian directed
multigraph, every preassigned target trajectory has expected hitting time
at most t_unif(1/4)+10m(n-1)=O(mn), uniformly over initial vertices.
The proof also gives an exponential survival bound and extends to independent
random targets. It completes the logarithm-removal question following
Corollary 2.3 of Boczkowski, Peres and Sousi.

A separate simple nonreversible 18-vertex, 51-arc example has fixed-target
expectation 936>918. It refutes coefficient one only in the arbitrary
deterministic-target interpretation. It is not a counterexample for two
independent copies. The ambiguous full AIM Problem 3.1 is not marked solved.

## Analytic proof and self-audit

Eulerian balance gives stationary measure d(x)/m. The energy identity and
simple underlying paths yield a point Dirichlet constant 1/[4m(n-1)].
Jensen's inequality and half-laziness bound the norm of each killed step
P D_a by the square root of one minus that constant, without reversibility.
Products of these operators control arbitrary target sequences.

The burn-in argument uses an unnormalized killed subprobability dominated
by the unconditioned mixed law; it does not assume the conditional survivor
law is mixed. Summing the geometric tail proves integrability and the
displayed constant. The O(mn) uniform-mixing theorem is imported from
Boczkowski, Peres and Sousi. The killed-operator method is credited to
prior work including Oliveira and Peres.

For the explicit counterexample, all first-step equations are verified by
the displayed potential. Detailed self-audit found no mathematical gap within
the stated scope. This is not independent peer review or formal verification.

## Exact regression evidence

The standard-library checkers use fractions.Fraction and explicit validation,
not floating-point tolerances or optimization-removable assertions.
Normal and optimized runs both passed:

- 44 Eulerian fixtures and 204 rational positive-semidefiniteness checks.
- 2,448 energy-vector checks and 34,520 target trajectories.
- 824 comparisons with literal path enumeration.
- 204 burn-in domination checks and 1,632 warm-tail checks.
- Four negative controls for nonlazy contraction, nonlazy evasion,
  coupled targets and incorrect uniform stationarity.
- Exact rational solution of the 17 hitting-time equations of the
  18-vertex witness, matching all 18 displayed potential values.

Reproduction commands are in README_submission.md and reports are in
reproducibility/checks/. These finite tests support the algebra and conventions
but do not establish the infinite-family theorem.

## Presentation and limitations

The five-page manuscript compiled successfully in the native editor and
was exported with Tectonic without TeX warnings. Every final page was
visually inspected. Author-only heading, affiliation/contact footnote,
in-prose AI disclosure, readable formulas and complete references were checked.

AI assistance supported exploration, drafting and reproducibility checks;
the author remains responsible for the claims. The preprint is unrefereed.
Novelty and priority are not certified by the bounded literature search.
Third-party publications are cited but not included in the source archive.