The k-Markov conditional-kernel mass at the last index of a Fin (n+1)-tuple. For n ≤ k: uses the full prefix Fin.init y : Fin n → α and the kernel condDistrib (obs n) (blockRV n) μ. For n > k: uses the last k symbols of the prefix (a window indexed n-k+j) and the kernel condDistrib (obs k) (blockRV k) μ.

The k-Markov joint mass of a path y : Fin n → α, defined recursively as the product of markovFactors along the path. When evaluated at y = blockRV n ω, this equals (a.s.) exp(-negLogQk μ p k n ω).

Per-state, markovFactor μ p k n is a genuine probability distribution over the next symbol: summing over all continuations a : α of a fixed prefix z gives exactly 1. This holds because markovFactor is a condDistrib kernel singleton mass and condDistrib is an IsMarkovKernel (so kernel z univ = 1). It is the enabler for the correct-direction conditional log-sum (the per-step factor of the k-Markov measure is a bona-fide sub-distribution that telescopes to qkSingleton).

The k-Markov conditional mass of a length-ℓ continuation w : Fin ℓ → α extending a fixed prefix z : Fin start → α, defined as the product of markovFactors at the absolute positions start, start+1, …, start+ℓ-1. The tuple fed to each markovFactor (start+m) is the combined prefix Fin.append z (init…w) recast to Fin ((start+m)+1) → α. At ℓ = 0 this is 1; the recursion peels the last symbol of w via Fin.init, matching qkSingleton's chain-rule structure so the product telescopes to qkSingleton (start+ℓ) / qkSingleton start.

Conditional product sub-distribution from a fixed prefix: for any prefix z : Fin start → α, the k-Markov conditional masses of all length-ℓ continuations sum to at most 1. The non-empty-start generalization of sum_qkSingleton_le_one (which is the start = 0 case): same induction on ℓ, each step reindexing via Fin.snocEquiv and collapsing the inner symbol sum with markovFactor_sum_eq_one (which holds for an arbitrary prefix, hence works from a non-empty start). This is the per-fixed-context sub-distribution the conditional Ziv (k-state, length) grouping instantiates.

Per-state sub-distribution: summing markovFactor μ p k n over any finite subset T of continuations is at most 1 (subset sum ≤ full sum = 1). This is the building block that the conditional Ziv grouping instantiates: a restricted set of continuations carries at most the full conditional probability mass.

Position invariance of markovFactor (the n > k branch). For n₁, n₂ > k, markovFactor μ p k n depends only on the last k + 1 symbols of its argument (the k-symbol window plus the last symbol), not on the absolute position n. This is the foundation of the conditional Ziv (k-state, length) grouping: the conditional mass of a phrase depends only on its trailing k-state, so phrases sharing a k-state may be grouped regardless of where they occur. The n > k branch of markovFactor uses the fixed kernel condDistrib (obs k) (blockRV k) μ, whose argument is the window and whose singleton set is the last symbol; both agree across n₁, n₂ under the window/last hypotheses, so the two factors are equal.

The k-Markov conditional masses started from a fixed k-state s : Fin k → α. This is condQk specialized to start = k: the per-k-state conditional product sub-distribution that the (k-state, length) Ziv grouping instantiates.

The per-k-state conditional masses sum to at most 1: the start = k specialization of condQk_sum_le_one.

∑_y qkSingleton k n y ≤ 1: the inductive product is bounded by 1 because each inner sum ∑_a (condDistrib ...){a} = 1 by IsMarkovKernel.

A.s. positivity of every per-position markovFactor evaluated at the block random variable: for a probability-preserving stationary process, a.s. (in ω) the real-valued Markov factor markovFactor μ p k i (blockRV (i+1) ω) is strictly positive at every position i. This is the a.s. positivity input that the LZ78 threading tiling discharges (the per-phrase hposfac precondition of negLogQk_phrase_threading). It follows from cond_singleton_pos_ae (the conditional kernel singleton mass is a.s. positive): for i ≤ k directly, and for k < i via the measure-preserving shift T^[i-k].

@audit:ok

A.s., qkSingleton μ p k n (blockRV n ω) equals ofReal (exp (-negLogQk μ p k n ω)). This is the numerator half of MRatioUp_eq_ofReal_exp.

A.s. equivalence between the MRatioUp ratio form and the exp-of-difference form used by downstream lemmas (MRatioUp_le_sq_eventually, blockLogAvg_le_negLogQk_plus_error).

Upward likelihood ratio: exp(n · blockLogAvg - negLogQk) lifted to ENNReal.

Markov inequality input: the upward ratio integrates to at most 1.

Proof:

1. Bridge MRatioUp to the ratio form qkSingleton k n (blockRV n ω) / P_n {blockRV n ω} a.s. via MRatioUp_eq_ofReal_exp.
2. Push forward through blockRV n using lintegral_map, then lintegral_fintype over the finite alphabet: ∑_y qkSingleton k n y / P_n {y} * P_n {y}.
3. (a / b) * b ≤ a (unconditional in ENNReal): bound the sum by ∑_y qkSingleton k n y.
4. Apply sum_qkSingleton_le_one.

Borel–Cantelli consequence: the upward ratio is eventually bounded by n² a.s.