A monotone measure for pattern-language inclusion: every morphic inclusion, every pattern of length at most eight, and the inclusion depth in that range

Abstract

Luo's open-problem note from COLT 2005, reissued in 2026 as arXiv:2605.30389, asks for the inclusion depth ID_Σ(p) of a pattern p — the length of the longest strict chain of pattern-language inclusions joining L_Σ(x₁) to L_Σ(p) — and asks whether ID_Σ(p) = 2|p| - #var(p) - 1. It reduces that formula to one monotonicity statement, its Conjecture 1: if L(p) ⊂ L(q) then 2|p| - #var(p) > 2|q| - #var(q). The note reports that its author's program verified the inequality for patterns of length at most 7 and that longer patterns were "computationally impractical". Write μ(r) = 2|r| - #var(r). We prove that μ(σ(q)) ≥ μ(q) for every non-erasing substitution σ of patterns for variables and every pattern q, at every length, and that equality forces σ to act on the variables of q as an injective renaming, whose inverse substitution the proof produces; hence Conjecture 1 holds for every inclusion realised by a morphism, with no restriction on length. That is a genuine partial result: we exhibit a strict inclusion L(001x₁x₂) subsetneq L(x₁x₂x₃x₂) over {0,1} realised by no morphism — a phenomenon credited to Angluin, and not new here. Independently, we verify Conjecture 1 for every pair of patterns of length at most 8 over a two-letter alphabet — one length beyond the note's own computation, so that any counterexample must involve a pattern of length at least 9. The verification is an exhaustive check over 115,974 canonical patterns, run behind a proof that the check quantifies over all patterns and not merely over the enumerated representatives. As a consequence the upper half of the note's formula becomes unconditional in that range: every strict chain from L(x₁) to L(p) through patterns of length at most 8 has at most 2|p| - #var(p) - 1 steps, which together with the note's own displayed chain pins ID_Σ(0x₁1) = 4. Every theorem below is machine-checked in Lean 4.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-09-07 03:53 UTC

   File fingerprint

   f8fad274f10b56e31fb98449b9dc1512e3d46d995e4d7ee4cb4ef3aff5c1868e