The per-symbol negative log-likelihood in bits, blockLogAvg / Real.log 2.

The base-2 (bit) version of blockLogAvg. SMB (shannon_mcmillan_breiman) converges blockLogAvg → entropyRate in nats; dividing through by Real.log 2 gives the bit-unit version converging to entropyRate₂, the unit that matches the base-2 LZ78 bit-rate lz78GreedyEncodingLength/n.

The Shannon–McMillan–Breiman theorem in bits: blockLogAvg₂ converges a.s. to entropyRate₂.

Obtained from shannon_mcmillan_breiman (nat units) by dividing the convergence through by Real.log 2: this is the unit rescaling entropyRate / Real.log 2 = entropyRate₂, not new ergodic content.

Both defs unfold to … / Real.log 2, so the rescaling is Tendsto.div_const (Real.log 2) followed by simpa [blockLogAvg₂, entropyRate₂].

@audit:ok

Factorial-power decay c! · 2^c ≤ (c+1)^c (real form). The per-c structure-Kraft term c!/(c+1)^c is geometrically small. Proved by induction; the step uses Bernoulli 2·(c+1)^(c+1) ≤ (c+2)^(c+1).

Bit-length decay (nat form) 2^{bitLength c a} ≥ (c+1)·a. The per-phrase bit cost is large enough that 2^{-bitLength} collapses the dictionary-size and alphabet-size factors. From Nat.lt_pow_succ_log_self: m + 1 ≤ 2·2^{log₂ m}.

The dependent function type assigning each phrase position j : Fin c a parent index in Fin (j+1) (one of the j earlier phrases or the empty prefix) has exactly c! elements.

The fiber-cardinality count is bounded by the parent-data target (nat form): the map sending x (in the c-phrase fiber) to its parent indices, phrase symbols, and tail index is injective, so the fiber injects into ((j : Fin c) → Fin (j+1)) × (Fin c → α) × Fin (c+1), whose cardinality is c! · |α|^c · (c+1). Injectivity uses the parent-extension invariant lz78PhraseStrings_dropLast_earlier (each phrase's dropLast is an earlier phrase or empty) to reconstruct the phrase list by strong induction on the position, and lz78PhraseStrings_flatten_prefix + List.ofFn_injective to recover x from the phrase list and tail.

The number of n-tuples x : Fin n → α whose greedy parse emits exactly c distinct phrases is bounded by (n + 1) · c! · |α|^c. This is the combinatorial counting fact behind the polynomial Kraft bound lz78_block_kraft_poly: the map x ↦ (lz78PhraseStrings (List.ofFn x), tail) is injective (lz78PhraseStrings_flatten_prefix reconstructs List.ofFn x, and List.ofFn_injective), and the parent-extension dictionary structure (lz78PhraseStrings_dropLast_earlier: each phrase's dropLast is an earlier entry or empty) makes the j-th phrase one of the j earlier entries (or the empty prefix) extended by one symbol, giving ≤ c! · |α|^c valid phrase-lists; the unfinished tail (lz78PhraseStrings_flatten_tail_mem, a dictionary member or empty) contributes a multiplicity ≤ c + 1 ≤ n + 1 (since c ≤ n).

Proved unconditionally in lz78_phrase_count_fiber_card_le_nat via Finset.card_le_card_of_injOn into the parent-data Fintype ((j : Fin c) → Fin (j+1)) × (Fin c → α) × Fin (c+1) (cardinality fintype_card_parentIdx = c!, times |α|^c, times c+1), with the empty fiber for c > n handled by lz78PhraseStrings_count_le.

@audit:ok (non-circular, non-degenerate; the injection x ↦ (parent, sym, tailIdx) in lz78_phrase_count_fiber_card_le_nat is injective by strong induction — reconstruct each phrase's dropLast from the parent index via the parent-extension invariant, recover the last symbol from sym, reassemble the phrase, then recover x via flatten ++ tail + List.ofFn_injective.)

The per-c Kraft term bound (Part C, geometric collapse).

The fiber sum over n-tuples with c distinct phrases is geometrically small: #fiber(c) · (1/2)^{c·bitLength(c,|α|)} ≤ (n+1)·(1/2)^c. Combines the counting bound lz78_phrase_count_fiber_card_le (#fiber(c) ≤ (n+1)·c!·|α|^c) with the bit-length decay 2^{c·bitLength(c,|α|)} ≥ ((c+1)·|α|)^c (from Nat.lt_pow_succ_log_self), giving #fiber·2^{-...} ≤ (n+1)·c!/(c+1)^c and the elementary inequality c!·2^c ≤ (c+1)^c.

Polynomial n-block Kraft bound for the greedy parse: the Kraft sum of 2^{-L_n(x)} over all n-tuples x : Fin n → α is bounded by a polynomial in n:

∑_{x : Fin n → α} (1/2)^{lz78GreedyEncodingLength n x} ≤ (n + 1)^2.

Why a polynomial and not the exact Kraft ≤ 1: the greedy longest-prefix-match parse is not complete — the flattened phrase list is only a prefix of the input (lz78PhraseStrings_flatten_prefix), and the unfinished tail (flatten ++ tail = input, with tail ≠ [] possible and tail a prefix of an existing phrase) is not charged a fresh (parent, symbol) token. Hence lz78GreedyEncodingLength n x = c · bitLength c |α| is the cost of only the c completed phrases and is not a lossless code length for x, so the exact Kraft inequality ∑ 2^{-L_n} ≤ 1 is false. What holds instead is the polynomial bound: the number of distinct parse structures with c phrases is ≤ c! · |α|^c, and 2^{-c·bitLength(c,|α|)} ≈ (c+1)^{-c}|α|^{-c}4^{-c}, so the structure-Kraft sum ∑_c (#structures)·2^{-c·bitLength} = O(1); the unfinished tail contributes a multiplicity ≤ n + 1, giving O(n) ≤ (n+1)^2.

The math is O(n), so any polynomial degree ≥ 1 is a true bound; the degree 2 here gives the summable μ(B_n) ≤ 1/n^2 in the Barron Markov + Borel–Cantelli lift (blockLogAvg₂_minus_error_le_rate_ae).

This is the combinatorial core of the LZ78 converse (Cover–Thomas lower bound, distinct-phrase counting).

The proof is assembled from three parts:

• Part A — fiberwise regrouping of the Kraft sum by the distinct-phrase count c = φ x (Finset.sum_fiberwise_of_maps_to', φ x ≤ n);
• Part B — the finite counting fact lz78_phrase_count_fiber_card_le (#fiber(c) ≤ (n+1)·c!·|α|^c), proved via the LZ78 dictionary parent-extension invariant (lz78PhraseStrings_dropLast_earlier) and a Fintype.card injection into ((j:Fin c)→Fin (j+1)) × (Fin c → α) × Fin (c+1);
• Part C — the per-c geometric collapse lz78_block_kraft_term_le (#fiber(c)·2^{-c·bitLength} ≤ (n+1)·(1/2)^c, built from the bit-length decay two_pow_bitLength_ge and the factorial-power decay factorial_two_pow_le_succ_pow), then sum_geometric_two_le and (n+1)·2 ≤ (n+1)² (with the n = 0 boundary 1 ≤ 1).

The per-n bad-set measure bound (Markov on the discrete block law plus the polynomial Kraft bound lz78_block_kraft_poly).

For n ≥ 1, the LZ78 converse bad set B_n = {ω : lz/n < blockLogAvg₂ n ω − err_n} has μ-measure at most 1/n², where err_n = (2 log n + 2 log(n+1))/(n log 2).

This is the Markov step of the Barron lift. The bad set factors through the block random variable (lz and blockLogAvg₂ depend on ω only via block_n ω), so μ(B_n) = (μ.map block_n)(S_n) = ∑_{x ∈ S_n} Pₙ(x) over the discrete block law Pₙ = μ.map block_n. For each x ∈ S_n with Pₙ(x) > 0 the defining inequality (cleared of denominators) gives Pₙ(x) < 2^{−Lₙ(x)}·2^{−n·err_n}, and 2^{−n·err_n} = 1/(n²(n+1)²). Summing and applying lz78_block_kraft_poly (∑_x 2^{−Lₙ(x)} ≤ (n+1)²) gives μ(B_n) ≤ (n+1)²/(n²(n+1)²) = 1/n². The combinatorial content lives entirely in that Kraft bound; this lemma is its measure-theoretic plumbing.

The Barron a.s.-eventual lift: the per-realization, a.s.-eventual converse lower bound on the greedy bit-rate by blockLogAvg₂ minus an o(1) error term.

For a stationary process p, almost surely the greedy bit-rate lz78GreedyEncodingLength n (block_n ω) / n is, eventually in n, at least blockLogAvg₂ n ω minus the vanishing error (2 log n + 2 log(n+1))/(n log 2):

∀ᵐ ω, ∀ᶠ n,  blockLogAvg₂ n ω − (2 log n + 2 log(n+1))/(n log 2) ≤ lz/n.

This is the Barron competitive-optimality a.s. lift (Cover–Thomas): a per-realization LZ78 codeword can be shorter than −log₂ Pₙ{xⁿ}, so the expectation-level converse H_D ≤ E[L] does not transfer pointwise. The lift is a Markov + first Borel–Cantelli argument on the bad set B_n = {ω : lz/n < blockLogAvg₂ n ω − err_n}: by lz78_block_kraft_poly, μ(B_n) = Pₙ{xⁿ : Pₙ(xⁿ) < 2^{−Lₙ}·2^{−n·err}} ≤ 2^{−n·err}·∑ 2^{−Lₙ} ≤ 2^{−n·err}·(n+1)², and with n·err = 2 log₂(n+1) + 2 log₂ n this is ≤ 1/n², summable, so first Borel–Cantelli gives ∀ᵐ ω, ∀ᶠ n, ω ∉ B_n.

Modeled on the Z-side blockLogAvgZ_ge_negLogQInftyZ_minus_error (SMB/AlgoetCover/Liminf.lean) — the same Markov + p-series + Borel–Cantelli template. It consumes the combinatorial polynomial Kraft bound lz78_block_kraft_poly through the per-n bad-set measure bound lz78_converse_bad_set_measure_le.

The almost-sure LZ78 converse lower bound for the longest-prefix-match greedy parser (Cover–Thomas, lower-bound half): for a stationary ergodic source p the per-symbol length of the greedy LZ78 parse lz78GreedyEncodingLength is, almost surely, asymptotically at least the bit entropy rate:

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

This is the lower-bound (converse) half of LZ78 asymptotic optimality — the harder direction (SMB liminf lower bound + arbitrary-prefix Kraft inequality + finite-alphabet bookkeeping).

Units: the encoding length is a base-2 code length (lz78GreedyEncodingLength = c · bitLength c |α|, 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 (not the nat-unit entropyRate), the unit correction documented in ZivEntropyBridge.lean ("Base-2 (bit) layer"). On a uniform i.i.d. source on A symbols the bit-rate limit is log₂ A = entropyRate₂ exactly, so the converse holds with equality in the limit; on the degenerate entropyRate = 0 boundary it reads 0 ≤ liminf.

The Barron reduction: the body is wired from two ingredients plus the bit SMB convergence,

• shannon_mcmillan_breiman₂ (SMB in bits) — gives Tendsto blockLogAvg₂ → entropyRate₂ a.s.;
• blockLogAvg₂_minus_error_le_rate_ae (the Barron a.s.-eventual lift) — gives ∀ᶠ n, blockLogAvg₂ n ω − err_n ≤ lz/n a.s., with err_n → 0;

assembled by Filter.liminf_le_liminf between the lower sequence Low n = blockLogAvg₂ n ω − err_n (which → entropyRate₂, so liminf Low = entropyRate₂) and lz/n (bounded above by lz78_rate_le_const, hence cobounded below). The converse content — the Barron competitive-optimality lift — sits in blockLogAvg₂_minus_error_le_rate_ae, which in turn consumes the combinatorial lz78_block_kraft_poly (the polynomial n-block Kraft bound).

@audit:ok (non-circular, non-bundled (signature (μ, p) + [IsProbabilityMeasure μ] only), non-degenerate, sufficiency TRUE-as-framed: the body wires SMB-in-bits (Low n → entropyRate₂) with the Barron a.s.-eventual lift (Low n ≤ lz/n eventually, err_n → 0) via liminf_le_liminf.)