Papers With

← All papers
First page of Block-exchange descent for insertion: commuting projections and minimum masks

Block-exchange descent for insertion: commuting projections and minimum masks

Haobo Ma, Wenlin Zhang, Charles E. Hughes

cs.FL Oct 29, 2026 · v1 math.CO
formalization mathlib combinatorics
Read PDF arXiv abstract Code
TL;DR
The iteration-depth no-gap theorem for arbitrary languages over any alphabet type is formalized in Lean 4 with Mathlib, as a referenced artifact.
Abstract
For fixed nonempty words $u,v$, the minimum insertion degree of a shuffle is the least number of inserted-source runs among its representations. We prove that, after a block exchange from a minimum mask of degree $r$, the minimum over masks with commuting source projections is exactly $r-1$; a larger decrease occurs precisely when a noncommuting mask has fewer runs. If either source is unary, every such exchange is exact. We prove an explicit repair for an infinite periodic degree-three family. Computer-assisted results establish first-mask descent through combined length seventeen over every alphabet, degree-three first-mask descent through length thirty, and a uniform repair of all degree-three failures through length thirty, including all further letter identifications. Counterexamples to arbitrary, first, and last minimum-mask choices explain the need for alternative masks. Finally, we prove that minimum iteration depths have no gaps for arbitrary languages. General block-exchange descent and Singleton No-Gap remain open.
Problem

For fixed nonempty words u and v, the minimum insertion degree of a shuffle is the least number of inserted-source runs over its representations (masks). The question is whether a block exchange from a minimum mask lowers the degree by exactly one, and whether the degree spectrum has no gaps.

Approach

The exact obstruction to descent is characterized by splitting the masks of the exchanged word into those with commuting and noncommuting source projections. Exactness is proved when either source is unary, and an explicit label-shift repair is given for an infinite periodic degree-three family. Exhaustive numerical and symbolic equality-pattern enumerations with certificates cover the finite domains. The no-gap theorem for minimum iteration depths over arbitrary languages is formalized in Lean 4 with Mathlib.

Results

Over commuting masks the minimum after a block exchange is exactly r-1, and a larger drop happens only through noncommuting masks with fewer runs. Computer-assisted results give first-mask descent through combined length 17 over all alphabets, and degree-three descent and repair through length 30. Counterexamples rule out arbitrary, first and last minimum-mask choices, and minimum iteration depths are shown to have no gaps. General block-exchange descent and Singleton No-Gap remain open.