Sanov-Cramer in infinite dimensions: a Chentsov uniqueness theorem on directed measure spaces

Every nondegenerate Markov-monotone Riemannian metric on a finite probability simplex equals a positive scalar multiple of the Fisherinformation metric — this is the classical Chentsov uniqueness theorem, proved by Čencov. Campbell later extended the characterization to the positive cone of non-normalized measures. We extend the theorem to the infinite-dimensional, directed-cylinder setting in which the base space is Polish and the metric is a cylinder-compatible Markov-monotone Riemannian metric on the space of probability measures: every finite-cylinder shadow equals the samenonnegative scalar multiple of the Fisher metric, and the scalar is forced constant across cylinders by the compatibility of the directed measurable extension. Under the nondegenerate Riemannian normalization this scalar is strictly positive. This is the directed finite-shadow form of the infinite-dimensional extension: the finite scalar survives the inverse-limit passage while the hypotheses remain classical, commutative, and cylinder-based. The proof factors through three ingredients formalized in Lean~4: the finite-partition Chentsov theorem on each cylinder shadow; the partition-coarsening Data-Processing Inequality for KL divergence; and the cylinder-compatible inverse-limit construction over the directed system of finite measurable partitions. We complement the theorem with its large-deviation reading: the Sanov rate function on empirical measures is the Hessian of the negative log-partition, and the Cram\'er rate function on empirical means is its Legendre dual, with the Fenchel--Young identity reading as the Bregman--Pythagorean equality at conjugate saturation. The Sanov--Cram\'er Fenchel--Legendre duality bundle packages this operationally. We also state the precise boundary at which the theorem fails: in the quantum setting, the Petz~\cite{petz-1996} family ofoperator-monotone metrics on density matrices does \emph{not} collapse to a single scalar, so the classical hypothesis (scalar measures on a Polish base) is sharp. The new formal claims in this paper are backed by Lean~4 anchors, while classical inputs such as Petz's classification are cited as literature; per-theorem \texttt{\textbackslash{}formalref} pointers identify the source files in the public FrogBird repository. \keywords{Chentsov uniqueness \and Fisher information metric \and information geometry \and Markov monotonicity \and Sanov theorem \and Cram\'er theorem \and Fenchel--Legendre duality \and Bregman divergence \and Pythagorean theorem \and Polish space \and cylinder algebra \and Data-Processing Inequality\and Petz monotone metric \and Lean 4.}