overlap
plain-language theorem explainer
Row overlap for Markov kernels is defined as the sum over targets of the minimum probability mass assigned by each of two source states. Analysts of contraction rates in stochastic processes cite it when establishing Dobrushin-type bounds on total variation. The definition is realized directly as a summation of pointwise minima on the kernel matrix.
Claim. For a Markov kernel $K$ on a finite type $ι$, the overlap between rows $i$ and $i'$ is $∑_j min(K.P(i,j), K.P(i',j))$, where $K.P$ is nonnegative and each row sums to one.
background
MarkovKernel is the structure that equips a finite type $ι$ with a matrix $P : ι → ι → ℝ$ obeying non-negativity for all entries and unit row sums. The overlap function then extracts a scalar in [0,1] that measures shared probability mass between any pair of rows. This construction appears in the Dobrushin module to support contraction arguments that feed into mixing derivations and modal geometry results.
proof idea
The declaration consists of a single-line definition that sums the minimum of the corresponding entries from the two rows of the kernel probability matrix.
why it matters
It supplies the quantitative overlap primitive used by the $V_{cb}$ derivation in MixingDerivation, where edge-dual ratios yield the Cabibbo element as 1/24. The same quantity appears in the unification of mock theta orders and congruence primes via the Q3 bridge, and in the modal Nyquist theorem that enforces a one-tick resolution limit. Within Recognition Science it supports the transition from the forcing chain to concrete mixing bounds that respect the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.