The longest-prefix greedy worker returning the list of emitted phrase strings (the LZ78 dictionary entries) in order.

• fuel : ℕ bounds recursion depth (instantiated to input.length + 1).
• dict : List (List α) — phrase strings emitted so far, in order.
• cur : List α — the candidate prefix being grown (still ∈ dict or empty); acc plus the next symbol forms the next test.
• input : List α — the remaining un-consumed suffix.

Invariant maintained for the Nodup proof: dict.Nodup and cur ∈ dict (or cur = []). At each symbol s, form cur ++ [s]; if it is already a dictionary entry, keep growing; otherwise emit it (it is ∉ dict by the guard) and reset cur := [].

lz78PhraseStrings input — the longest-prefix greedy parse of input, returning the ordered list of emitted phrase strings.

The worker preserves Nodup: if the running dictionary is already Nodup, the dictionary returned by the worker is Nodup. The emitted string is ∉ dict by the if-guard, so List.Nodup.concat applies.

The list of emitted phrase strings of the longest-prefix greedy parse is Nodup.

The additive foldr-length over an append: the total phrase length of l ++ [w] is the total over l plus w.length. (The accumulator fun w acc => w.length + acc is additive, so foldr_append would leave a non-zero seed; this dedicated lemma keeps the seed at 0.)

Worker form of the length budget: the total symbol count across the phrases the worker emits is at most the symbols it holds, namely the accumulated dict length plus cur.length plus input.length. No length is created, since the worker only re-emits dict entries and pieces carved out of cur ++ input.

The total number of symbols across all emitted phrase strings is at most the input length. (Each emitted phrase consumes input symbols; the unfinished tail accounts for the slack, so this is ≤, not =.)

The worker conserves the flattened string: the concatenation (List.flatten) of all emitted phrase strings, followed by an unfinished tail, reproduces the symbols seen so far dict.flatten ++ cur ++ input. This is the reconstruction invariant: the phrases tile a prefix of the input by concatenation at their cumulative lengths, with the leftover tail being the un-emitted suffix (the ≤-slack of lz78PhraseStrings_total_length_le). Proved by structural induction on fuel, tracking the cur accumulator across the keep-growing / emit branches.

@audit:ok

The concatenation of all emitted phrase strings, followed by an unfinished tail, equals the input. The cumulative phrase lengths therefore furnish an absolute-position tiling of a prefix of the input, with the tail accounting for the ≤-slack. Instantiates lz78PhraseStringsAux_flatten_conserve at the top-level fuel.

@audit:ok

The worker conserves the flattened string and bounds the tail: the unfinished tail at termination is the final candidate prefix cur, which the greedy invariant keeps as a dictionary entry (or empty). So the tail is a member of the returned phrase list (or []), bounding its length by the longest phrase. Proved by induction on fuel, threading the invariant cur ∈ dict ∨ cur = [] (preserved on both the keep-growing and emit branches).

@audit:ok (fuel-induction establishing the tail ∈ dict ∪ {[]} invariant).

The unfinished tail of the parse is a phrase string (a member of lz78PhraseStrings input) or empty. Hence its length is at most the longest phrase length, which bounds the un-emitted trailing tail input.length - e.

The flatten length equals the additive foldr total, bridging the reconstruction-invariant List.flatten length to the cumulative-length foldr accumulator used by the tiling.

Flatten slice content correspondence (pure list fact). For a list of lists L, dropping the cumulative length of the first j sublists from the flatten and taking the j-th sublist length recovers L[j] exactly: (L.flatten.drop (cumLen j)).take (L[j].length) = L[j], where cumLen j = (L.take j).foldr (·.length + ·) 0.

This is the content half of the absolute-position tiling: the tiling carries phrase lengths/positions, and this lemma certifies that the slice at those positions reproduces the j-th phrase string.

The worker maintains the parent-extension invariant: every emitted phrase string is (an earlier dictionary entry) ++ [symbol] or [symbol]. Stated positionally: for the worker output D, each D[j].dropLast either equals [] or appears strictly earlier in D (i.e. in D.take j).

This is the dictionary structure behind the LZ78 phrase-count bound: at each step the worker emits cur ++ [s] where cur is a current dictionary entry (or []), and dictionaries only grow by appending, so cur sits strictly before the emitted phrase. Threaded with the running invariant cur ∈ dict ∨ cur = [].

For the longest-prefix greedy parse, each emitted phrase's dropLast is either [] or an earlier emitted phrase.

The property is specific to the LZ78 dictionary structure, not a general fact about lists of lists: it fails for L = [[a, b]], where L[0].dropLast = [a] ∉ L.take 0 = [] and ≠ []. What makes it hold is that the dictionary grows only by appending cur ++ [s] with cur an earlier entry, so the emit branch has (cur ++ [s]).dropLast = cur ∈ dict by List.dropLast_concat.

@audit:ok (non-vacuous; the fuel-induction discharges its base and nil cases through the threaded running invariant hdict, not by fuel exhaustion, and the top level supplies the sufficient fuel input.length + 1, so the quantified parse is not the empty list).

The worker emits only non-empty phrases: if every dictionary entry is non-empty, every entry of the worker output is non-empty. The emitted string is cur ++ [s], which is always non-empty.

All emitted phrase strings are non-empty.

When every phrase is non-empty, the count is bounded by the total length: the number of phrases is at most the sum of their lengths, since each length is ≥ 1.

Every entry of a list of strings has length at most the longest entry length (the Lmax accumulator used to bound the leading-boundary and trailing-tail symbol lengths in the tiling).

The number of distinct phrases emitted by the longest-prefix greedy parse is at most the input length. Combined with lz78PhraseStrings_nodup (the strings are distinct), this is the count c(n) ≤ n feeding the Cover–Thomas counting bound c(n) · log c(n) ≤ K·n.

Deterministic absolute-position tiling from the greedy parse. For an input list and a Markov order k, the greedy longest-prefix parse furnishes an absolute-position partition of the input prefix it covers: a leading boundary length b, a phrase count c, a covered length e ≤ input.length, the count bAbsorbed of leading phrases absorbed into [0, b) (those whose cumulative end is ≤ k), and the cumulative-position function N : Fin (c + 1) → ℕ.

The partition [b, e) is strictly monotone (each phrase consumes ≥ 1 symbol), every phrase start N j.castSucc exceeds k (the leading ≤ k phrases are absorbed), the count is anchored to the parse via c + bAbsorbed = (parse).length, and bAbsorbed ≤ k + 1 (the cumulative length increases by ≥ 1 each step, so at most k + 1 phrases fit below position k).

The boundary-length bounds (for the downstream limsup discharge): with Lmax the longest phrase length, the leading boundary b ≤ k + Lmax (the last absorbed phrase extends one phrase past the ≤ k cumulative prefix) and the trailing tail input.length - e ≤ Lmax (the un-emitted tail is one dictionary phrase or empty, lz78PhraseStrings_flatten_tail_mem).

This is the pure list-combinatorial heart of the LZ78 threading tiling: it carries the phrase lengths only (the downstream threading reads phrase content directly off the process, never the parse strings' content).

@audit:ok (pure list-combinatorial core, no hypothesis bundling; non-vacuous because c := parseCount - bAbsorbed with bAbsorbed = Nat.find the least index whose cumulative length exceeds k, so c > 0 whenever parseCount > k+1, and the boundary bounds come from lz78PhraseStrings_flatten_tail_mem plus the last-absorbed-phrase argument rather than from a vacuous tiling).