AI referee report

The statistical experiment is not coherently specified in the manuscript. The model-class tuple contains “L(O_T),” an observed-data law, while the Markov, sequential-ignorability, and stationary-start restrictions are statements about the latent full trajectory. Later the appendix separately introduces a full law and observation map, but those objects are needed to understand the model class itself.

The presentation-level definition “Behavior and target stationary joint-state laws” defines P_p as a Markov kernel and d_p as its stationary law before b and e have been required to be probability vectors and before contraction has supplied existence and uniqueness. For a raw policy carrier, P_p need not yet be stochastic, so the definition is logically premature as written.

The appendix reproduces lengthy, mechanically structured proof transcripts whose local bookkeeping overwhelms the econometric argument. The central ideas—radius-sensitive bias, window covariance control, terminal-depth filtering, KL calibration, and two-point reduction—are difficult to recover, despite the formal correctness of the statements.

The sentence “Cref{obj:thm:uniform-overlap-frontier} gives a single observable estimator” can suggest one estimator independent of the radius, whereas the displayed estimator uses the supplied value of C through its history depth.

The section initially reads like an application of the minimax theory, while the crucial fact that the construction certifies four structural constants and a bias diagnostic—but not the complete model-class predicate or a theorem-level rate application—appears much later. The extensive interval-certificate detail is also disproportionate to the example's interpretive role.

The exact reconstruction of the Hu–Wager hard instance, including the asserted stationary terminal masses and their ratio, is central to the novelty claim but is attributed only broadly to their Theorem 3.1. It is unclear whether those formulas are stated there or derived by the present authors from the construction.

The sentence “It keeps the single stationary trajectory, known memoryless policies, bounded rewards, finite but cardinality-unrestricted latent state, and no proxy-informativeness or emission-rank assumptions” frames the contribution partly through absent assumptions outside a limitations section, contrary to the affirmative contribution contract.

At first use, T and C appear in formulas without plain-language appositives identifying them as the trajectory horizon and stationary-overlap constant. This violates the first-use gloss requirement even though later prose explains them.

The notation alternates among θ(K,e), θ(M), and θ_m, and among E_M, E_obs, and expectations under explicitly named observed laws. Although local explanations are sometimes supplied, the changes obscure which law and model representation are in force.

The manuscript explains the frontier repeatedly in prose but provides no compact visual or table showing the unit, local, and fixed-radius regimes, the governing term, and the corresponding PHIW depth. This makes the main contribution harder to absorb than necessary.

The title footnote says that the appendix records the artifact commit, but the verification note lists the Lean toolchain and mathlib revision without giving the paper artifact commit from the verification contract.

The shrinking-frontier theorem labels t_0 and ζ as “Fixed smoothness,” although they are introduced elsewhere as mixing and log-overlap scales.

The sentence “It belongs to the same verified library and compile under the same toolchain” has a subject–verb agreement error.