Comments from peer review

Stream: Seymour

[Martin Dvořák]

Unfortunately, we got rejected from CPP. Below are the comments from the peer review.

[Martin Dvořák]

Paper summary

The Paper present a formalization in Lean4/Mathlib of composition direction of Seymour's Theorem for regular matroids. Recall that matroids are a combinatorial abstraction of the notion of independence (as in linear independence in vector spaces, algebraic independence over a field or acyclicity in graph). Seymour’s Regular Matroid Decomposition Theorem says that each regular matroid can be obtained from graphic matroids, their duals, and copies of R10 by taking 1-, 2-, and 3-sums. They only proove the composition direction stating that matroid constructed as above are regular.

The main difficulty to formalize such broad abstractions as matroids is that they are several equivalent definition which may rely or not on some finiteness assumption. Hence the authors start the paper by making a case for their choice of approach: They choose to follow a less general one that avoid using too much of not yet formalized graph theory. In return it requires proof to go across three levels of abstraction (matrices, standard representation matrices, and binary matroids in general).

Comments for authors

The paper is well written and present a substantial formalization effort a large part of which deserve to be integrated in Mathlib. The technical choices are clearly discussed. Moreover the authors take care of giving some feedback and advice about Lean Mathlib and the aesop tactic (in appendix).

However, aside the choice of the mathematical approach, translating the definition into formal one seems to be relatively straightforward, with few genuinely novel or challenging aspects beyond the usual dependent type issues (e.g., handling matrix dimensions in block matrices). Also it is far from being the first formalization in matroid theory. As such, the paper offers only incremental progress rather than a significant new contribution. Taken together, the work does not reach the level of originality or depth expected for acceptance.

We also have a few suggestions concerning the presentation: it is quite technical with a lot of repetition in the presented code that could be abbreviated (see eg: Set.drop?, Matrix.toMatrixDropUnionDrop, standardReprSum3 or the three identical Matroid.IsSum?of.isRegular theorems). On the other hand the reader not specialist of matroids, may have difficulty to follow the logical progression of the paper. I would strongly recommend the following changes:

• The authors seem to assume that the reader is familiar with the notion of 1-, 2-, 3-sums. They should give a broad intuitive idea of what they are right at the beginning of the introduction.
• The author should insert couple of paragraph in the introduction explaining the structure of the paper as well as his logical progression
• at the beginning of each section, the author should add a little paragraph recalling the reader where he is in this logical progression.

[Martin Dvořák]

Paper summary

This paper presents a formalization of the composition (forward) direction of Seymour's decomposition theorem for regular matroids in Lean 4. This direction proves the structural property that any 1-, 2-, and 3-sum of two regular matroids is a regular matroid.

This new library establishes formal definitions and proves properties for a range of necessary concepts, including totally unimodular matrices (some of which were contributed to Mathlib), vector matroids and their standard representations, the definition of regular matroids via totally unimodular representations, and the 1-, 2-, and 3-sum operations.

Using this, the authors provide a machine-checked proof of the composition direction. An interesting aspect of this formalization is its generality: the proof holds for matroids that have finite rank but may possess infinite ground sets. In addition to proving the composition direction, the authors also provide a formal statement of the corresponding decomposition direction (that all regular matroids can be decomposed into graphic, cographic, and $R10$ matroids) to complete the formal statement of Seymour's theorem.

Comments for authors

The paper is an interesting read, and describes the key definitions and main statements for the theorem in question. The "trusted code" is presented clearly. The pictures of matrices are nice and helpful also! For me, there are some balances which I think were not struck quite right, however.

• The definition of regular matroid presented here is not the typical one given, which I was somewhat surprised to see. More surprising is that this distinction and alternate definition was not explicitly mentioned, and I would have liked to see comments on why this particular definition was chosen, as opposed to the usual "representable over any field" version: it's a nontrivial theorem that they're the same! Consulting Truemper, I see that perhaps this was simply due to following the source very closely, and arguably therefore this is covered around line 235, but a difference in definition for a word which is mentioned in the title is a big enough difference to deserve some more detail.
• The paper spends much time on definitions, and much less time on the difficulties (or lack thereof) of formalising the theorem itself. It is nice to display these definitions, but I would have liked to see quite a bit more detail in Section 11. For instance, line 1134 writes that the proof for 1-sums is nearly identical to the source, but a (sketch) proof of what that is could have added to the presentation here. And a sketch proof of the titular theorem also seems worth mentioning. For 3-sums, a high level description of the differences between the informal and formalized proof is given, but it is tricky to contextualise this without referencing (or already knowing) the informal proof; and a slightly less high level description would also be interesting to read. More generally, I'd like to know if there are any insights gained from this formalization that could be applicable elsewhere.
• Relatedly, it seems there is little discussion of the design choices made when writing some of the definitions. For instance, matrixSum1 is a function, while Matroid.IsSum1of is a predicate, but why was standardReprSum1 chosen to be a (partial) function too? As it's partial, it seems more natural to use a predicate, which checks the precondition too. Lots of time is taken to detail the definitions, so I would like to read the authors' thoughts on what they learnt (and any wrong steps) taken towards getting these ones.

Minor comments:

• Giving a summary of the structure of the paper near the end of the introduction would be valuable for signposting.
• Around line 190, explicitly mentioning Oxley and Truemper would be nice here, to avoid the reader jumping to the references.
• Around line 290, there's a slight ambiguity in the informal descriptions: where exactly is B2 quantified in (iii)? A little thought or foreknowledge reveals the answer, but I think a nicer way to present this would be to declare the word base, then define independence, then write the base axioms with reference to the notion of independence (closer to how Mathlib does it: using indep to define the maximality axiom)
• When defining independence, there's also a slight ambiguity: does "any base" mean for all bases, or for some base? Again, an experienced reader will know the answer, but some readers may be encountering matroids for the first time here!
• The choice of variable names is unfortunate in this section, the informal version sometimes uses different letters from the formal version, meaning we're left with many, many different letters around: M, E, B, X, I, J, alpha, P, Y. It may be worth looking for some overlap if it can be found here.
• Around line 360, it may be worth explicitly mentioning that m,n are arbitrary (finite) types, not necessarily natural numbers: some readers expect matrices to be indexed by naturals! This is referenced again around line 808. This may also give you the opportunity to recall what Fin is, and why it's relevant to your formalisation (you mention Fin 2 and Fin 3 fairly often later)
• Certain variables are declared repeatedly, most notably {𝛼 : Type*} and [DecidableEq 𝛼]. Consider omitting these, or mentioning them only once near the start, to save you space and to save the reader the overhead (a kind of LaTeX-variable!). You may also consider ignoring DecidableEq assumptions altogether in the presentation, especially since at no point is the computability aspect mentioned in your discussion.
• Line 432: how does this differ from Subtype.toSum?
• Line 510: The source [12] only mentions the standard representation once, so giving an informal description of what it is here would help a lot: you write "standard representation matrix B", but this isn't a well-known concept to most readers of papers in this journal! More generally, [12] is a big reference and it's used often, so for points like this which are specific, writing something like [12, p32] or [12, Sec 3.2] is quite a bit more useful.
• Line 591, "as it would be hard to verify that total unimodularity is preserved in our prior approach." I'd very much like to know why this would be hard! In particular, I'm more interested in this than getting another reminder that {𝛼 R : Type*} [DecidableEq 𝛼].
• Line 860: mentioning the dimension of D0 explicitly would be useful.
• Section 10 overall gives me quite a lot of code, some of which is quite repetitive. I'm not sure that the contents of the definition of Matrix.toMatrixDropUnionDrop, for instance, is all that valuable: perhaps a link to the full definition together with the informal description and a summary could have sufficed. Or, if there's a particular point you'd like to stress which is made by this definition, you should explain it more explicitly.

[Martin Dvořák]

Paper summary

This paper formalizes the statement of Seymour's matroid decomposition theorem in Lean and proves the composition direction (that 1-, 2-, and 3-sums of regular matroids are regular). The authors have developed supporting formalizations around totally unimodular matrices, vector and regular matroids, standard representations, and the 1-, 2-, and 3-sums of vector matroids. The formalization builds upon the Matroid library in Mathlib.

It presents proof-engineering ideas that helped simplify the formalization compared to existing proofs, avoiding the combinatorics of $Δ$-sums and re-signings by introducing a "canonical" signing.

The supplementary materials appear to be accurate formalizations of the presented material. It is structured and appears to be reusable for future work toward proving the full theorem.

Comments for authors

This formalization work is a notable milestone and appears to be valuable for future developments toward a full proof of Seymour's decomposition theorem. At the same time, the paper currently reads more like a technical companion to the formalization rather than an articulation of the mathematical or formal-methods contributions. Much of the exposition describes what was implemented, with comparatively little attention to why the result is interesting, what conceptual or engineering challenges arose, or what was learned that could transfer to other formalizations.

Below are some suggestions to help strengthen the paper in a revision:

• State the main theorem precisely. The theorem is given informally, but the paper does not present a clear mathematical formulation of the composition directed being formalized. An exact statement would help clarify the scope of the formalization. An example of the ambiguity is that the full matroid decomposition appears to be, Matroid.RankFinite.isRegular_iff_isGood, and the composition direction of it is Matroid.IsGood.isRegular, which not only shows the regularity of 1-, 2-, and 3-sums of regular matroids (as shown in the paper), but the regularity of graphic matroids (proved in the code), and of cographic matroids (stubbed out with sorry). A clear statement of the theorem in the paper would help prevent confusion.
• A stronger narrative of the mathematics of the theorem would help motivate why formalizing the theorem is difficult or interesting. The paper mentions some applications of the theorem, but it would help to understand what is important about regular matroids. Furthermore, a description of what structural phenomena that the various sums capture would be elucidating.
• A discussion of the decomposition direction, even if only qualitative. The paper hints that this is the natural next step, but a section outlining what remains to be formalized, what obstacles are expected, and how the current formalization positions that work would be beneficial to the work.
• The narrative around "compromises" can be a discussion of reasonable scoping decisions, rather than weaknesses. This can also help with the clarity of the rest of the presentation; for example, the paper could add the assumption that matroids have finite ground sets, and whatever generalizes to the infinite matroids of Bruhn et al. (the Matroid in Mathlib) can be briefly mentioned in a short section.
• Relatedly, reflect more on design choices and trade-offs. Section 2 briefly compares Oxley vs Truemper as foundations but does not analyze the consequences to future developments. It explains the immediate convenience, but not the appropriateness, or the potential design tradeoffs. The brief sentence about experiments in proving equivalences being hard could be expanded upon to paint a picture of what was hard.
• Differentiate routine formalizations from novel ideas. Sections 4-10 contain many code listings, but it's not clear what required new mathematical ideas, formalization ideas, or design choices. For example, in section 7 it is unclear whether totally unimodular signings are a new idea that simplified the formalization or if they are a direct formalization from the literature.
• Make novelty more explicit relative to prior work. The related work section is detailed but largely descriptive. It leaves it to the reader to determine the novelty of the formalization.
• Trim low-level implementation details. The Decidable class appears frequently in excerpts, but without explanation. If these are only required to interface with Mathlib, a brief comment suffices and could be omitted, since they distract from the conceptual presentation. If these are required to enable proof by reflection, that is worth explaining as well.
• I noticed in the code that R10's regularity uses a proof by reflection. That is potentially interesting for CPP, yet it does not appear in the paper. If it is omitted because it does not appear in the paper's formulation of the composition direction, consider still highlighting it as it may interest readers.

Small comments:

• 345 and elsewhere: "infinite matroid" vs "infinite ground set" is somewhat confusing. My understanding is that infinite matroid is a specific axiomatization of matroids from Bruhn et al., and it might be misunderstood by readers.
• 361: Citing Schönfinkel (1924) for currying feels out of place. Multi-argument functions are standard in Lean and not specific to matrices.
• 407 and elsewhere: Avoiding the set->type coercion and using Set.Elem directly is unusual and might merit explanation.
• 226: "graph theory which is not supported in Mathlib" could be phrased more carefully, since Mathlib has graph theory, but perhaps not the specific graph theory needed for [9]/[12].
• 1229: Typo, Matroid.IsRegular.isGood_of_rankFinite instead of Matroid.IsRegular.isGood.

[Evgenia Karunus]

Interesting comments, thanks for posting, good to know what's generally expected!

[Martin Dvořák]

I am confused by the fact that the first reviewer wrote

"Also it is far from being the first formalization in matroid theory. As such, the paper offers only incremental progress rather than a significant new contribution. Taken together, the work does not reach the level of originality or depth expected for acceptance."

but then the same reviewer added a comment:

"The consensus among the referees is that the paper’s rejection stemmed not from its (quite good and substantial) formalization, but from shortcomings in its presentation. Too few research outcomes are presented here, as opposed to merely describing the implementation. One would like to see reflection on what was difficult, novel, or what conceptual insights were gained. We all believe that with significant restructuring, it could become a strong paper. Therefore we encourage the author to resubmit, maybe with work toward the full theorem (which is admittedly more difficult)."

[Evgenia Karunus]

I think they implied that the conceptually interesting stuff should be described verbally in a paper, because it's hard/impossible to determine what the novelty is by skimming the code.

[Evgenia Karunus]

Meaning - the easy-to-find novelty could be "this is a first formalization of matroid theory", which it isn't.
Another easy-to-find novelty could be "translating the definitions into formal definitions", which also doesn't work because that part seemed straightforward.

So they need a verbal description of what was conceptually interesting and why, because their immediate guesses didn't work.

[Alex Nelson]

In addition, after carefully reading the reviewers's comments yesterday several times, I feel they are also implicitly asking the questions, "Who is the audience for this paper? Who are the readers you are writing for?"

[Martin Dvořák]

Oh yeah, we were keeping it implicit. In my Ph.D. thesis, which is more long-winded, I extensively talk about who the intended audience is, but in the paper, we kept it implicit. We did, however, have an internal document answering this question; unfortunately, I cannot find it now. From what I remember, we all agreed on writing for a reader who knows Lean but doesn't know what a matroid is. I think the only exception is the appendix, in which we write for the authors of the tools we were using.

[Alex Nelson]

How well do you think the article spoke to that audience? And do you think it was a suitable audience for the CPP?

[Martin Dvořák]

I don't know. Do you have a suggestion?

[Alex Nelson]

Well, I will be frank: when I joined the project, I thought the paper was written for matroid theorists who were already pretty competent at using some proof assistant (not necessarily Lean, and not necessarily based on CoC/dependent-types).

[Alex Nelson]

But looking at the paper again (with the benefit of some time passing since I last looked at it), I really can't shake the feeling that there are several different audiences being spoken to, consequently none of them are adequately addressed.

[Martin Dvořák]

After taking a step back and rereading the comments, I understand the criticism as follows...

There is huge disconnect between what I wanted to write and what the reviewers wanted to read (and, of course, there is also some disconnect between what I wanted to write and what we wrote in the end, but this gap seems much less important).

From my point of view, I saw our contributions divided into two levels, with the primary level being infinitely more important than the secondary level.

Primary contributions:

• the definitions
• the theorem statements
• there exists a sorry-free proof (the only thing about the proof that matters is what #print axioms shows)

Secondary contributions:

• what the proof looks like
• what we learned from it
• what we could have done differently

My plan was to cover the primary contributions as perfectly as possible, and bring up the secondary contributions only if some space remains.

However, the reviewers had completely different perspective! They would say something like:
"OK, there are some definitions, good, there are some theorems, good. However, all of it is in the code. Give me something that isn't written in the code!"

From the reviewers' perspective, the goal of writing the paper was not to summarize the project for somebody who doesn't open the repository, but to provide some surplus value to somebody who opens the repository and has the paper next to it. And we didn't provide enough of those "extras".

[Martin Dvořák]

Put differently, we were answering this question:
"What is objectively true about our project?"
While doing so, we neglected this question:
"What is interesting about our project?"

With the new perspective, our new manuscript should go much further into "what is interesting" and "what was challenging".

That said, I am probably the worst person from the entire team to elaborate on "what is interesting" and "what was challenging".
There wasn't a single moment in the project when I would be approaching it as "let's learn what is easy in Lean and what is surprisingly hard to formalize".
Every single time, I was approaching the project as "let me create a sorry-free proof, no matter the cost".
Of course, I could reflect on what was hard for me, but every time something was harder than I expected it to be, I don't know if it was harder than I expected because it was inherently hard, because Lean made it hard, or because I chose a wrong approach.
For example, I can confidently say that proving standardReprSum3_hasTuSigning was hard for me, but I cannot say why it was hard (and I definitely cannot say whether it would be similarly hard for a different person).

Hopefully, other contributors can reflect on "what was hard" better and provide a better insight into "what is interesting".

[Martin Dvořák]

In retrospect, the way the paper is written makes most of the text more suitable for a thesis than for a conference paper. In my thesis, I mostly play hide-the-pain Harold: I talk about the results, not about the struggles on the way there. In a thesis, the author needs more to be accurate than to be competitive.

Unfortunately, it seems that for a successful paper, we need to be somewhat boastful; it isn't enough to plainly say what we did, as we did in our paper. The question remains who will be the person to elaborate on "what is interesting" and "what was challenging" for the new version. Shortening should come later, once we know how much new content we need to accommodate.

[Martin Dvořák]

One more comment: I like to write papers as if I were presenting a product. In contrast, the reviewers would probably prefer if it was written as a case study how we made the product.

Do you have the same impression?

[Byung-Hak Hwang]

For me, when I write a math paper, I usually prefer to clearly explain the results, much like you do. However, in the case of our paper, I don’t think it contains fundamentally new theoretical results. Rather, it might be more appropriate to document what can happen during the process of manual formalization, and what kinds of issues and design choices need to be considered in order to make our implementation compatible with existing libraries. I wonder if this is what the reviewers had in mind as well.

[Martin Dvořák]

I get the second part of your message. But aren't math papers supposed to contain proofs? I thought that only formalization papers have the luxury of being able to explain results without explaining proofs, as those proofs are provided elsewhere.

[Byung-Hak Hwang]

I agree with your point. In math papers, the proofs are at the core of the paper, whereas in formalization, I see the product itself as the central contribution. Still, I think we should ask what a reader can actually gain from this paper. Simply presenting our implementation seems more suitable for a well-organized GitHub repository. For a paper submitted to a journal or a conference, it may be more important to reflect on what we learned through this project, and what readers can learn from it. For that reason, I suspect this is what the reviewers were getting at with their request.

[Martin Dvořák]

Since you seem to be on the same page as the reviewers, do you have concrete suggestions what to write in the paper?

[Martin Dvořák]

Another point in favor of NOT documenting the project in our paper is that our repository contains a summary in Seymour.lean by which we already do more for documenting our code that most projects do.

That said, I suggest first focusing for on what we WANT to say, and only then I would discuss what will be removed from the paper (depending on how much over the page limit will the combination of old and new content together be).

[Martin Dvořák]

Some info about the process (as opposed to the result, which reviewers seem not to be interested in) can be found in our status updates here:
https://github.com/Ivan-Sergeyev/seymour/tree/main/slides

[Byung-Hak Hwang]

Martin Dvořák 말함:

Since you seem to be on the same page as the reviewers, do you have concrete suggestions what to write in the paper?

Sorry for the late reply. Although I may not be the right person to suggest an outline for the paper since I’m not fully aware of all the details of the entire development process, I’ll try my best.

[Martin Dvořák]

I will be on vacation for the next three days, but I will be able to keep replying today. Before @Byung-Hak Hwang makes changes, could @Cameron Rampell open a PR with the changes he suggests?

[Martin Dvořák]

Byung-Hak Hwang said:

suggest an outline for the paper

Or are you willing to outline a new paper from scratch? @Cameron Rampell has already given up on the idea of writing an entirely new paper afaik.

[Cameron Rampell]

I pushed my contributions for the paper on Github (which I probably should have opened in a new pull request). Could you make sure it compiles? I didn't have all the packages necessary to compile the code locally, so I just went about blindly editing LaTeX files instead.

[Martin Dvořák]

Indeed, it should be at least three different PRs. If you don't know how to open several PRs, I can always just copypaste selected files from your PR, but you will not appear in the commit history.

[Cameron Rampell]

I'm fine with that if it's easier for all of us.

[Martin Dvořák]

As for changes to the paper, which is perhaps the most urgent thing to discuss, I disagree with
\section{Proof Outline and Design Choices}
since

• Definitions and statements have not appeared yet. There is no proof to outline.
• Design choices should probably be discussed throughout. Of course, the main design choices can already come here.

Once you change the section title, we can discuss what should be expanded.

[Martin Dvořák]

As for the other changes, I think that ⊕₂ and ⊕₃ are too much of notation abuse, since the 2-sum and the 3-sum are relations, not functions. Interestingly, the 1-sum is a function, but you don't write such notation there.

[Cameron Rampell]

Do you think we can simply relocate the proof outline after we have defined everything? I suppose I can easily fix the notational stuff too.

[Martin Dvořák]

I don't really know but my impression is that the reviewers would have preferred some kind of overall outline before the definitions.

[Martin Dvořák]

Cameron Rampell said:

I'm fine with that if it's easier for all of us.

Certainly not for all of us, but I am willing to manually update the files.

[Martin Dvořák]

Martin Dvořák said:

As for the other changes, I think that ⊕₂ and ⊕₃ are too much of notation abuse, since the 2-sum and the 3-sum are relations, not functions. Interestingly, the 1-sum is a function, but you don't write such notation there.

On the other hand, I really like your description of the 2-sum and the 3-sum in prose. Could the sentences be perhaps a bit modified so that the reader knows that we illustrate what those notions mean for graphs? I am not sure if the reader implicitly understands that your description is not general for all pairs of (binary) matroids.

[Cameron Rampell]

Could I just insert something like "we describe what this operation looks like in the graphical case: one joins two graphs along a single common edge, then deletes that edge from the combined graph"?

[Martin Dvořák]

Sounds good. Do you think we will be able to accompany the prose with images?
#Seymour > Pictures for the paper

[Cameron Rampell]

Sure, I think I can easily reproduce those images in TikZ.

[Martin Dvořák]

Another big thing to discuss is what to do about the "side-quest results" that are mentioned in our paper (I am talking about lemmas like Matrix.exists_standardRepr_isBase which we didn't need in any proof but we decided to provide them for the sake of creating a useful library). Currently we cite them verbatim and, on top of that, we describe them shortly in prose. We can...

• keep them verbatim
• state them in some kind of symbolic informalism (perhaps similar to blueprint)
• keep only the prose (i.e., mention them but not state them)
• remove all side quests from the paper

I have no idea what would be best.

[Byung-Hak Hwang]

Over the past few days my computer was broken down. I’ll first take a look at Cameron’s PR.

[Byung-Hak Hwang]

It seems neither of you want to rewrite the paper from scratch. I think it would be useful to look through papers published in ITP and CPP to get a better sense of the expected style and how similar results are presented. Do you know of any ITP or CPP papers that are similar in spirit to our project?

[Martin Dvořák]

Byung-Hak Hwang said:

It seems neither of you want to rewrite the paper from scratch.

Yeah, sorry. Apart from the 3-day vacation I took, I have been too busy with finishing my Ph.D..

[Martin Dvořák]

Byung-Hak Hwang said:

Do you know of any ITP or CPP papers that are similar in spirit to our project?

Similar in spirit as in "presenting mathematical results, not a paper on metatheory, not a paper about tooling" ?

If you mean it this broadly, then circa a half of recent ITP papers is similar in spirit.

[Martin Dvořák]

Martin Dvořák said:

• I noticed in the code that R10's regularity uses a proof by reflection. That is potentially interesting for CPP, yet it does not appear in the paper. If it is omitted because it does not appear in the paper's formulation of the composition direction, consider still highlighting it as it may interest readers.
  

@Tristan Figueroa-Reid
Would you have time to write a very short section about proving regularity of R10, which you implemented?

[Martin Dvořák]

Byung-Hak Hwang said:

Do you know of any ITP or CPP papers that are similar in spirit to our project?

You can have a look at a very new distinguished paper:
https://arxiv.org/pdf/2509.04922

[Tristan Figueroa-Reid]

Would you have time to write a very short section about proving regularity of R10, which you implemented?

[Have there been any changes in the place where I should write this?]

[Martin Dvořák]

Tristan Figueroa-Reid said:

[Have there been any changes in the place where I should write this?]

Overleaf doesn't want to compile such a large document anymore, unless we get the paid subscription. Hence I suggest we continue here:
https://github.com/Ivan-Sergeyev/seymour/tree/main/paper

[Martin Dvořák]

Or do you @Cameron Rampell want to take it to Overleaf now that the writing is in your hands? I don't know whether the compilation-time issue persists after switching to the LIPICS template.

[Byung-Hak Hwang]

Quick question. Is anyone currently working on revisions?

[Martin Dvořák]

I am not working on revisions. I will just write up a few paragraphs (or rather adapt from my thesis) about a certain design decision, and it will be up to yall whether to include it or not.

[Martin Dvořák]

Here.
toMatrixDropUnionDropInternal.txt