The trailing k-state of the infinite trajectory just before absolute position N (i.e. the symbols at positions N-k, …, N-1), read off blockRV. This is the k-state s : Fin k → α that conditions a phrase starting at position N. Defined via obs so it is position-coherent with blockRV (blockRV m ω j = obs j ω for any m).

Gateway atom (single-factor position correspondence). Let a phrase start at absolute position N with k ≤ N, and consider its offset m. The per-position factor entering negLogQk at the absolute position N + m, markovFactor μ p k (N+m) (blockRV (N+m+1) ω), equals the factor entering the conditional product condQk started from the trailing k-state s = windowState p k N ω, namely markovFactor μ p k (k+m) t for the condQk-shaped tuple t = Fin.append s w ∘ Fin.cast whose continuation w matches the block on the phrase window.

Both positions N+m and k+m exceed k once m ≥ 1 (and the m = 0 case reduces both branches to the full-prefix kernel condDistrib (obs k) (blockRV k)), so markovFactor_eq_of_window_eq applies after checking the window/last coincidence. This is the linchpin of the whole threading decomposition.

For an absolute position i > k, the per-step k-Markov approximation term pmfLogCondMarkov μ p k i ω (entering negLogQk) is exactly the negative log of the markovFactor read off the block: `pmfLogCondMarkov μ p k i ω =

• log (markovFactor μ p k i (blockRV (i+1) ω)).toReal. This is the deterministic bridge identifying each negLogQkterm with amarkovFactor, the form the gateway atom markovFactor_blockRV_eq_window` rewrites.

Product form of condQk along a block segment. When the continuation Z matches the block on the phrase window (Z j = obs (N+j) ω) and the trailing k-state s is windowState p k N ω, the conditional product condQk μ p k k s ℓ Z equals the product of the absolute-position markovFactors over the phrase positions N, …, N+ℓ-1. Proved by induction on ℓ using the gateway atom markovFactor_blockRV_eq_window at each peeled factor (the condQk recursion peels the offset-ℓ factor; the gateway atom rewrites the relative-position factor to the absolute one).

Per-phrase segment identity. A phrase of length ℓ starting at absolute position N > k contributes, to negLogQk μ p k (N+ℓ) ω, exactly the negative log of the per-k-state conditional product condQkState μ p k s ℓ Z of the phrase content Z, where s is the trailing k-state at N. Concretely:

∑_{m<ℓ} pmfLogCondMarkov μ p k (N+m) ω = - log (condQkState μ p k s ℓ Z).toReal,

i.e. the block of factors of negLogQk over the phrase positions telescopes to a single condQkState entry. This is the per-phrase atom the (k-state, length) grouping consumes; it follows from the single-factor correspondence markovFactor_blockRV_eq_window applied position-by-position, plus the recursive shape shared by negLogQk and condQk (both products / sums of the same markovFactors).

The positivity hypothesis hposfac (each per-position markovFactor is > 0) is a regularity precondition: it is cond_singleton_pos_ae along the phrase positions, and is needed only to move -log through the product. Proved from markovFactor_blockRV_eq_window and condQk_eq_prod_markovFactor.

Per-phrase positivity. When each per-position markovFactor along a phrase window [N, N+ℓ) is > 0 (the cond_singleton_pos_ae regularity input), the per-k-state conditional product condQkState μ p k s ℓ Z of the phrase content is > 0 (in toReal). It is the product of those positive factors (condQk_eq_prod_markovFactor + ENNReal.toReal_prod), needed to supply the hpos input of condState_grouping_bound_mean.

Telescoping of an Ico over a monotone partition. For a monotone M : ℕ → ℕ (M i ≤ M (i+1)) and any g : ℕ → β valued in an additive commutative monoid, the interval [M 0, M c) splits as the sum over j < c of the consecutive pieces [M j, M (j+1)). Pure Finset bookkeeping (induction on c via Finset.sum_Ico_consecutive); used to turn the LZ tiling into the per-phrase sum.

Threading decomposition. Given an explicit tiling of a prefix [0, e) of the block [0, n) into a leading boundary [0, N 0) and c phrase segments [N j, N (j+1)) (encoded by a monotone N : Fin (c+1) → ℕ, N 0 = b the leading-boundary length, N (Fin.last c) = e ≤ n the parse-covered length, and each phrase start > k), plus a trailing boundary [e, n) for the unfinished tail, the k-Markov negative log-likelihood negLogQk μ p k n ω splits as the leading-boundary contribution over [0, b), plus the sum over phrases of the per-phrase conditional contributions - log (condQkState μ p k sⱼ ℓⱼ Zⱼ).toReal (supplied by negLogQk_segment_eq_condQkState), plus the trailing-boundary contribution over [e, n).

The tiling hypotheses (hNb leading-boundary start, hNe parse-covered length, hen the ≤-slack, hmono strict monotonicity giving a contiguous partition of [b, e), hstart each phrase start > k) record the position bookkeeping of the LZ parse: the plain combinatorial structure of lz78PhraseStrings. The positivity input hposfac (each per-position markovFactor along a phrase is > 0) is the regularity precondition of negLogQk_segment_eq_condQkState, needed only to move -log through the product; it is cond_singleton_pos_ae along the phrase positions.

Proof: the negLogQk sum over [0, n) is split into [0, b) ∪ [b, e) ∪ [e, n); the middle [b, e) = [N 0, N (last c)) is telescoped over the partition by sum_Ico_telescope_of_monotone, each piece is reindexed to a phrase-local sum by Finset.sum_Ico_eq_sum_range, and the per-phrase sum is discharged by negLogQk_segment_eq_condQkState. The trailing [e, n) remains as the unfinished-tail boundary term.

The tiling itself is produced from the greedy parse by lz78_block_tiling below, whose cumulative-position function rests on the reconstruction invariant lz78PhraseStrings_flatten_prefix (the parse phrases concatenate to a prefix of the input).

The conclusion is an exact equality assembled by interval-split + telescope + the factor correspondence; hstart, hmono, hposfac and the trailing-boundary hypotheses are partition / positivity regularity. @audit:ok (non-circular, non-bundled, sorryAx-free).

Tiling materialization from the LZ parse (a.s. threading input). For the block blockRV n ω, the greedy longest-prefix parse lz78PhraseStrings (List.ofFn (fun i => blockRV n ω i)) yields, a.s. in ω, the absolute-position tiling consumed by negLogQk_phrase_threading: a leading boundary length b, a phrase count c, a parse-covered length e ≤ n, the absorbed-count bAbsorbed, and the cumulative-position function N : Fin (c+1) → ℕ with N 0 = b, N (last c) = e, the partition [b, e) strictly monotone (hmono), every phrase start > k (hstart, leading phrases below position k absorbed into the boundary), and the per-position positivity hposfac. Composing with negLogQk_phrase_threading threads negLogQk over the parse.

Three facts shape this signature:

• A.s., not per-ω. The per-position positivity hposfac cannot hold for all ω — markovFactor's positivity comes only from cond_singleton_pos_ae, an a.s. statement. So the whole tiling is an ∀ᵐ ω ∂μ, ∃ …; positivity is then discharged by markovFactor_blockRV_pos_ae. The downstream limsup argument is a.s. anyway, so an a.s. threading identity is the correct shape.
• bAbsorbed ≤ k + 1, not ≤ k. When the leading phrases all have length 1, the least index whose cumulative length exceeds k is k + 1; the cumulative length increases by ≥ 1 per phrase, so at most k + 1 phrases fit below position k.
• Phrase content coherence is unnecessary. negLogQk_phrase_threading reads phrase content directly as fun m => obs (N j.castSucc + m) ω; it never references the parse phrase strings' content, only the cumulative-length positions. So the tiling needs only the phrase lengths (via lz78_parse_tiling_positions), not a List.flatten-content-indexing chain.

The deterministic position tiling (lz78_parse_tiling_positions, GreedyLongestPrefix.lean) supplies b c e bAbsorbed N and the length-only conjuncts (monotonicity, hstart, e ≤ n, the parse-anchored count, and bAbsorbed ≤ k + 1); markovFactor_blockRV_pos_ae (SMB/AlgoetCover/MarkovLikelihoodRatio.lean) supplies the a.s. per-position positivity, and the body assembles the two.

The non-vacuity anchor. The plain existence of some tiling is vacuously true (c = 0, empty partition), so the content is encoded by anchoring the tiling to the parse: the phrase count c is the distinct-phrase count of the parse minus the leading phrases absorbed below position k, pinned by c + bAbsorbed = parseCount with the absorbed-count bAbsorbed ≤ k + 1. For a long block whose parse has parseCount > k phrases this forces c > 0, so the empty-tiling escape is unavailable.

The boundary-length bounds (supplied, for the downstream limsup discharge). The threading identity (negLogQk_phrase_threading) leaves the leading-boundary sum over [0, b) and the trailing-tail sum over [e, n) as additive terms; the downstream limsup discharge needs b / n → 0 and (n - e) / n → 0 to vanish those boundary contributions. This signature carries b ≤ k + Lmax and n - e ≤ Lmax with Lmax the longest phrase length (from lz78_parse_tiling_positions): the leading boundary is one phrase past the ≤ k absorbed prefix, and the un-emitted trailing tail is one dictionary phrase or empty (lz78PhraseStrings_flatten_tail_mem). Making those boundary terms vanish additionally needs Lmax = o(n) a.s. (the longest LZ78 phrase grows sublinearly), which belongs to the downstream achievability argument rather than to this tiling atom; the present lemma supplies the a.s. threading mechanism, the non-vacuity anchor and the boundary-length bounds.

@audit:ok (non-circular, non-bundled — only [IsProbabilityMeasure μ] regularity, and the existential's conjuncts, including the slice/content one ∀ j, (lz78PhraseStrings …)[bAbsorbed+j]? = some (slice), are all discharged from lz78_parse_tiling_positions and markovFactor_blockRV_pos_ae, with no new input hypothesis or *Hypothesis predicate; non-vacuous — the parse-anchored conjunct c + bAbsorbed = parseCount together with bAbsorbed ≤ k + 1 forces c > 0 once parseCount > k + 1, so the empty-tiling escape is closed.)

The tiling-hypothesis-free a.s. threading identity for negLogQk, with arguments μ, p, k, n only. It is obtained by feeding the parse tiling produced a.s. by lz78_block_tiling into the per-phrase decomposition negLogQk_phrase_threading: the tiling supplies the partition N, the boundary lengths, the parse-anchored phrase count, and the per-position positivity, which negLogQk_phrase_threading consumes to yield the exact negLogQk = (leading boundary) + (per-phrase sum) + (trailing tail) equality.

All of the tiling's structural/counting/boundary conjuncts are carried forward (the downstream (k-state, length)-grouping / limsup discharge needs the phrase count c, the non-vacuity anchor c + bAbsorbed = parseCount, and the boundary-length bounds n - e ≤ Lmax, b ≤ k + Lmax); the per-position positivity hposfac is consumed internally both to derive the equality and to produce the per-phrase positivity conjunct 0 < (condQkState …).toReal (via condQkState_pos_of_markovFactor_pos). The output also carries the slice/content correspondence conjunct (from lz78_block_tiling). This is the bridge consumed by the (k-state, length) grouping / limsup discharge.

@audit:ok (non-circular, non-bundled — only [IsProbabilityMeasure μ] regularity input

• produces the existential, no *Hypothesis predicate; both the slice/content correspondence and per-phrase positivity conjuncts are discharged from lz78_block_tiling's hslice and the per-position hposfac respectively).