Finite-prefix detection for nondecreasing words

The combinatorial core of the profile upper bound, stated for an arbitrary upward-closed predicate D : U → Prop on a linear order (u ≤ v → D u → D v), read as "the letter u is default-like". For a word r, its non-default prefixes are the nonempty prefixes τ ⪯ r with ¬ D (last τ) (ndPrefixes).

Theorem (exists_short_distinguishing_prefix): if a word r and a nondecreasing word s have different non-default prefix sets, there is a nonempty label τ of length at most r.length + 1, with ¬ D (last τ), that prefixes exactly one of them. The reference word r is arbitrary: only s, whose long prefix gets cut, needs to be nondecreasing.

The extra position: a longer non-default prefix of s is cut down to length r.length + 1; the cut is still a prefix of s, is not a prefix of r (too long), and is non-default because its last letter is at most the last letter of the longer prefix (nondecreasing) and D is upward closed, so ¬ D is downward closed.

Nothing here involves structures, ordinals, countability, allowed sets, or nesting. The specialization to D u ↔ B u ≅ B_* and the allowed-position membership enter afterward, in the profile statement.

def FirstOrder.Language.FiberAssembly.UpwardClosed {U : Type u} [LinearOrder U] (D : U → Prop) : Prop

An upward-closed predicate on the letters.

Equations

• FirstOrder.Language.FiberAssembly.UpwardClosed D = ∀ {u v : U}, u ≤ v → D u → D v

def FirstOrder.Language.FiberAssembly.ndPrefixes {U : Type u} (D : U → Prop) (r : List U) : Set (Label U)

The non-default prefixes of a word: nonempty prefixes whose last letter is not default-like.

Equations

• FirstOrder.Language.FiberAssembly.ndPrefixes D r = {τ : FirstOrder.Language.FiberAssembly.Label U | ↑τ <+: r ∧ ¬D τ.last}

theorem FirstOrder.Language.FiberAssembly.mem_ndPrefixes {U : Type u} {D : U → Prop} {r : List U} {τ : Label U} : τ ∈ ndPrefixes D r ↔ ↑τ <+: r ∧ ¬D τ.last

theorem FirstOrder.Language.FiberAssembly.last_le_last_of_prefix {U : Type u} [LinearOrder U] {p q : List U} (hq : List.Pairwise (fun (x1 x2 : U) => x1 ≤ x2) q) (hpq : p <+: q) (hp : p ≠ []) (hq' : q ≠ []) : p.getLast hp ≤ q.getLast hq'

A nonempty prefix of a nondecreasing word has its last letter at most the last letter of any longer prefix.

theorem FirstOrder.Language.FiberAssembly.exists_short_distinguishing_prefix {U : Type u} [LinearOrder U] {D : U → Prop} (hD : UpwardClosed D) {r s : List U} (hs : List.Pairwise (fun (x1 x2 : U) => x1 ≤ x2) s) (hne : ndPrefixes D r ≠ ndPrefixes D s) : ∃ (τ : Label U), (↑τ).length ≤ r.length + 1 ∧ ¬D τ.last ∧ ¬(↑τ <+: r ↔ ↑τ <+: s)

Finite-prefix detection. If an arbitrary word r and a nondecreasing word s have different non-default prefix sets, a non-default label of length at most r.length + 1 prefixes exactly one of them. Only s needs to be nondecreasing.