The greedy encoding length of a finite tuple: parse List.ofFn x with the genuine longest-prefix-match greedy parse lz78PhraseStrings, count its c distinct emitted phrases, and charge c · bitLength c |α| bits (each of the c phrases costs at most bitLength c |α| bits, the uniform Cover–Thomas per-phrase cost at the final dictionary size). This plugs into the parent lz78EncodingLength : ∀ n, (Fin n → α) → ℕ parameter of lz78_asymptotic_optimality.

The phrase count c = (lz78PhraseStrings (List.ofFn x)).length is the genuine distinct-phrase count (c ≤ n always, c = O(n / log n) asymptotically via lz78PhraseStrings_count_isBigO), so the per-symbol rate is data-dependent and asymptotically bounded — unlike a one-symbol-per-phrase parse.

The longest-prefix greedy parse lz78PhraseStrings of List.ofFn x emits at most n distinct phrases (lz78PhraseStrings_count_le plus List.length_ofFn).

The greedy encoding length lz78GreedyEncodingLength n x of x : Fin n → α is bounded by n · (log(n+1) + log|α| + 2), since the parse has c ≤ n distinct phrases, each costing at most bitLength n |α| bits. Combines the distinct-phrase count bound c ≤ n with bitLength-monotonicity in the dictionary size. This is the bit-length upper bound of Cover–Thomas.

The per-symbol asymptotic bit-rate bound on ℝ for the genuine greedy parse: dividing by n gives ≤ log(n+1) + log|α| + 2.

The per-symbol bit-rate is nonnegative: the greedy encoding length divided by n is ≥ 0 for every n (including n = 0, where the division is 0/0 = 0). The numerator is a ℕ cast and the denominator a ℕ cast, so the quotient is a nonnegative real.

(Nat.log 2 m : ℝ) * Real.log 2 ≤ Real.log m: the integer base-2 logarithm bounded by Real.log m / Real.log 2 with the denominator cleared. A real-valued restatement of Real.natLog_le_logb.

(c : ℝ) * Real.log (c + 1) ≤ (c : ℝ) * Real.log 2 + (c : ℝ) * Real.log c: the per-phrase +1-shift slack, from Real.log (c + 1) ≤ Real.log 2 + Real.log c (via Real.log (c + 1) ≤ Real.log (2 * c) for c ≥ 1; trivial for c = 0).

The per-symbol greedy bit rate lz78GreedyEncodingLength n x / n is bounded by a deterministic constant depending only on |α|, for every n (including the degenerate n = 0, where the rate is 0). The constant (1 + 8 * Real.log (|α| + 1) / Real.log 2) + (Nat.log 2 |α| + 2) comes from the Ziv product bound c * Real.log c ≤ 8 * Real.log (|α| + 1) * n (lz78PhraseStrings_mul_log_le), c ≤ n, and natLog_mul_log_two_le.

The per-symbol greedy bit-rate decomposes, deterministically and for each n, into a c·log c term and an o(1) overhead.

For 0 < n, writing c = (lz78PhraseStrings (List.ofFn x)).length for the distinct phrase count of the greedy parse, the greedy bit-rate splits as

lz/n ≤ (c · log c) / (log 2 · n) + overhead(n, x)

where the overhead overhead(n, x) = (c · log 2 + c · (log₂|α| + 2)) / (log 2 · n) collects the +1-shift slack (log(c+1) ≤ log 2 + log c) and the alphabet / parent-index constant cost. The first term is the combinatorial c·log₂c/n that the Ziv comparison connects to blockLogAvg₂ = -log₂Pₙ/n; the overhead is o(1) since c = O(n/log n) (lz78PhraseStrings_count_isBigO).

This is the unit-coherent (Nat.log 2 → Real.log / log 2) restatement of the encoding-length expansion inside lz78_rate_le_const; the bit-rate is left exactly as c·log c/(log 2 · n) + overhead, so the dominant term is available for the a.s.-eventual limsup comparison.

IsLZ78EncodingLengthBoundPassthrough B — hypothesis pass-through for an upper bound B : ℕ → ℕ on the genuine greedy encoding length lz78GreedyEncodingLength.

The canonical bound n · (log(n+1) + log|α| + 2) satisfies the encoding-length pass-through predicate, supplied by the Cover–Thomas bound lz78_encoding_length_le_n_log_n_plus_const.

Monotonicity of the bound pass-through.