The core lemma: for each fixed k, the a.s.-eventual limsup of the greedy bit-rate is at most the k-th conditional tail entropy in bits.

This is the per-k Ziv bound: combining the achievability composition ziv_achievability_composition (the c·log c ≤ negLogQk + o(n) brick) with the AEP negLogQk_div_tendsto_condEntropyTail and the deterministic overhead-vanishing c = O(n/log n), the per-symbol greedy rate is dominated by negLogQk/(log 2 · n) → H_k/log 2.

Diagonalizing over k (taking the infimum), the a.s.-eventual limsup of the greedy bit-rate is at most the bit entropy rate.

From Lemma 1 (ziv_aseventual_le_condEntropyTail_bits) for all k (countable intersection) plus the limit conditionalEntropyTail → entropyRate (entropyRate_eq_lim_condEntropy), rescaled by /Real.log 2. The LHS is a k-independent constant, so le_of_tendsto closes it.

The a.s.-eventual Ziv comparison: the limsup of the greedy bit-rate is at most the limsup of blockLogAvg₂.

The achievability crux (Cover–Thomas): combining the Ziv product bound c·log c ≤ 8·log(|α|+1)·n with the length-grouping overhead control c = O(n/log n) and the -log Pₙ = n·blockLogAvg identity, the greedy bit-rate is asymptotically dominated by blockLogAvg₂. Stated as an a.s.-eventual limsup comparison (the per-block form is FALSE, counterexample a^16).

The Ziv→AEP connection is supplied by the composition ziv_achievability_composition (c·log c ≤ negLogQk + o(n)) plus the AEP negLogQk_div_tendsto_condEntropyTail, assembled in ziv_aseventual_le_condEntropyTail_bits.

@audit:ok (non-circular, non-bundled (signature is (μ, p) + [IsProbabilityMeasure μ] regularity only), non-degenerate, sufficiency TRUE-as-framed (Cover–Thomas; per-block form correctly avoided; degenerate entropyRate = 0 boundary stays alive)).

The almost-sure Ziv-inequality achievability upper bound for the longest-prefix-match greedy parser: for a stationary ergodic source p the per-symbol length of the greedy LZ78 parse lz78GreedyEncodingLength is, almost surely, asymptotically at most the bit entropy rate:

limsup_n (1/n) · lz78GreedyEncodingLength(X^n) ≤ entropyRate₂ μ p   a.s.

This is the achievability (upper-bound) half of LZ78 asymptotic optimality (Cover–Thomas), i.e. the a.s.-eventual Ziv inequality limsup (c·log₂ c / n) ≤ H₂ combined with the SMB upper bound.

Units: the encoding length is a base-2 code length (bitLength uses Nat.log 2), so the per-symbol rate lz/n is in bits and the correct RHS is the bit entropy rate entropyRate₂ = entropyRate / Real.log 2, the unit correction documented in ZivEntropyBridge.lean ("Base-2 (bit) layer"). Against the nat-unit entropyRate the bound is false already on a uniform i.i.d. source on A ≥ 2 symbols, where the LZ78-optimal bit-rate limit is log₂ A = entropyRate₂ exactly, so against the bit target the inequality holds with equality in the limit; on the degenerate entropyRate = 0 boundary it reads limsup ≤ 0 with entropyRate₂ = 0.

lz78GreedyEncodingLength charges c · bitLength c |α| against the distinct phrase count c = (lz78PhraseStrings (List.ofFn x)).length.

The proof assembles the two halves of the achievability sandwich:

• shannon_mcmillan_breiman₂ (SMB in bits) — gives Tendsto blockLogAvg₂ → entropyRate₂ a.s., hence limsup blockLogAvg₂ = entropyRate₂ (Filter.Tendsto.limsup_eq);
• ziv_aseventual_le_blockLogAvg₂ (the a.s.-eventual Ziv comparison) — gives limsup (lz/n) ≤ limsup blockLogAvg₂ a.s.

Behind the second half, the Ziv→AEP connection — the variable-depth tree-node AEP linking the combinatorial c · log c to the probabilistic -log Pₙ — is ziv_achievability_composition (c · log c ≤ negLogQk + o(n)) plus the AEP negLogQk_div_tendsto_condEntropyTail, assembled per-k in ziv_aseventual_le_condEntropyTail_bits and taken over all k in ziv_aseventual_le_entropyRate₂, on top of the combinatorial core c · log c ≤ K · n, c = O(n / log n).

@audit:ok (non-circular, non-bundled (signature is (μ, p) + [IsProbabilityMeasure μ] regularity only), non-degenerate, sufficiency TRUE-as-framed; degenerate entropyRate = 0 boundary reads limsup ≤ 0 and stays alive).

LZ78 asymptotic optimality for the concrete greedy parser lz78GreedyEncodingLength (Cover–Thomas). For a stationary ergodic source p : ErgodicProcess μ α on a finite alphabet α, the per-symbol output length of the longest-prefix-match greedy LZ78 parse converges almost surely to the bit entropy rate:

lim_{n → ∞} (1/n) · lz78GreedyEncodingLength(X^n) = entropyRate₂ μ p   a.s.

The convergence target is the bit entropy rate entropyRate₂ = entropyRate / Real.log 2, not the nat-unit entropyRate, because the encoding length is a base-2 code length (lz78GreedyEncodingLength = c · bitLength c |α|, bitLength uses Nat.log 2). Against the nat-unit target the headline would be false on a uniform i.i.d. source; against the bit target it is true-as-framed, since on a uniform i.i.d. source on A symbols the bit-rate limit is log₂ A = entropyRate₂ exactly, and on the degenerate entropyRate = 0 boundary the target is entropyRate₂ = 0.

@audit:ok (non-circular, non-bundled (signature is (μ, p) + [IsProbabilityMeasure μ] only; both IsBoundedUnder witnesses + both sandwich halves are constructed internally), non-degenerate, sufficiency TRUE-as-framed (bit entropyRate₂ target, closed by the tendsto_of_le_liminf_of_limsup_le squeeze via lz78_asymptotic_optimality)).