IndisputableMonolith.YM.Dobrushin
The module supplies a minimal interface for Markov kernels focused on overlap computations inside the YM component of the Recognition framework. It introduces the core types and basic nonnegativity and normalization properties required to bound total variation distances between transition kernels. Researchers analyzing contraction rates or mixing times in discrete Markov processes would reference these definitions as the starting point for Dobrushin-style estimates. The module contains only type declarations and elementary lemmas, with no deep
claimA Markov kernel is a map $K: X → (X → [0,1])$ such that for each $x$ the function $y ↦ K(x,y)$ is a probability measure. The overlap between two kernels $K_1,K_2$ is defined by $overlap(K_1,K_2) = inf_{x} ∑_y min(K_1(x,y),K_2(x,y))$. The row function extracts the probability vector for a fixed state.
background
The module sits inside the YM.Dobrushin submodule and imports only Mathlib. It defines the abstract MarkovKernel type together with the auxiliary functions row, overlap, overlap_nonneg and overlap_le_one. These objects formalize the minimal data needed to apply Dobrushin’s contraction coefficient to total-variation distances. The setting is discrete-state Markov chains; no measure-theoretic or continuous-state machinery is introduced.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The interface supplies the basic objects that later lemmas (TVContractionMarkov, tv_contraction_from_overlap_lb, markovOfMatrix) rely on to obtain contraction bounds. It therefore feeds the chain of results that embed Dobrushin-type estimates into the larger Recognition Science treatment of mixing and stability.
scope and limits
- Does not supply concrete transition matrices or probability measures.
- Does not prove any contraction or mixing-time theorems.
- Does not treat continuous or infinite state spaces.
- Does not import or depend on any Recognition Science physics axioms.