overlap_nonneg
plain-language theorem explainer
The lemma establishes non-negativity of the row overlap for any Markov kernel on a finite state space. Researchers deriving Dobrushin contraction coefficients for total-variation bounds would cite this fact as a prerequisite. The argument first verifies pointwise non-negativity of each minimum term from the kernel nonnegativity fields, then invokes non-negativity of the finite sum over the universe before simplifying with the overlap definition.
Claim. Let $K$ be a Markov kernel on a finite set, so that $K(i,j)geq 0$ for all states $i,j$ and each row sums to one. Then for any states $i,i'$ the overlap satisfies $0leq sum_j min(K(i,j),K(i',j))$.
background
The MarkovKernel structure supplies a transition matrix $P$ together with the axioms that every entry is non-negative and every row sums to one. The overlap is the sum over target states of the pointwise minimum between two source rows; this quantity lies in the unit interval by construction. The lemma appears inside the Dobrushin module, whose purpose is to develop contraction estimates for Markov operators that later feed into Recognition Science forcing-chain arguments.
proof idea
The term-mode proof first constructs a pointwise lower bound: for each $j$ the minimum of the two kernel entries is non-negative by the min_nonneg lemma applied to the two nonnegativity hypotheses. It then lifts this to the full sum by applying sum_nonneg over the finite universe. The final simpa tactic unfolds the overlap definition to finish the argument.
why it matters
This positivity statement is a prerequisite for the contraction inequalities developed in the same module, including TVContractionMarkov and tv_contraction_from_overlap_lb. In the broader Recognition Science setting it supplies the measure-theoretic foundation needed to control the Dobrushin coefficient, which in turn supports extraction of the eight-tick octave and the emergence of three spatial dimensions from the T0-T8 forcing chain. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.