pith. sign in

arxiv: 2604.20778 · v1 · submitted 2026-04-22 · 🧮 math.CO

Modularity, Extensions and Connectivity in Infinite Matroids

Mattias Ehatamm , Peter Nelson , Fernanda Rivera Omana This is my paper

Pith reviewed 2026-05-09 23:51 UTC · model grok-4.3

classification 🧮 math.CO MSC 05B35
keywords infinite matroidsmodular pairssingle-element extensionsmatroid quotientsmatroid projectionsmatroid connectivityfinitary matroids
0
0 comments X

The pith

Generalizing modular pairs to arbitrary families enables a complete theory of single-element extensions for infinite matroids.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper generalizes the notion of a modular pair from finite matroids to arbitrary families of sets in infinite matroids. This step supports a full account of single-element extensions, clarifies how quotients relate to projections, proves that matroids with every flat modular must be finitary, and supplies two fresh characterizations of the connectivity parameter lambda. Existing finite techniques often fail outright in the infinite setting, so the work introduces infinite versions of nullity, local connectivity and skewness to make the arguments work. If the generalization holds, it supplies systematic ways to build and analyze infinite matroids that previously lacked such structure.

Core claim

We generalize the well-studied notion of a modular pair of a finite matroid to arbitrary families of sets in infinite matroids, and use it to develop the theory of infinite matroids in several as-yet-unexplored areas. Our results include a complete theory of single-element extensions, a description of the relationship between quotients and projections, a proof that matroids for which every flat is modular must be finitary, and two new perspectives on the infinite matroid connectivity parameter lambda. In most cases, existing theory for finite matroids either fails completely or does not extend in obvious ways, and as a result we develop multiple new techniques for reasoning about infinite, 0

What carries the argument

The generalization of modular pairs to arbitrary families of sets in infinite matroids, which carries the argument by allowing consistent definitions of extensions, quotients, projections and connectivity measures.

If this is right

  • A complete theory of single-element extensions exists for arbitrary infinite matroids.
  • Quotients and projections stand in a describable relationship through the modular-pair framework.
  • Any matroid in which every flat is modular must be finitary.
  • The connectivity parameter lambda admits two new characterizations based on modularity.
  • Infinite analogues of nullity, local connectivity and skewness can be defined and used without inconsistency.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the generalization works, infinite matroids can be constructed incrementally by adding one element at a time in a controlled way.
  • The finitariness result separates matroids into those with strong modular structure and those that must allow non-finite flats.
  • The new views on lambda may supply alternative bounds or computations for connectivity in other infinite combinatorial objects.

Load-bearing premise

The proposed generalization of modular pairs to arbitrary families of sets behaves consistently enough in the infinite setting to support extension theory and the other results without contradictions.

What would settle it

An infinite matroid in which the generalized modular-pair condition produces a single-element extension that violates the matroid axioms, or a non-finitary matroid in which every flat satisfies the modular condition.

read the original abstract

We generalize the well-studied notion of a modular pair of a finite matroid to arbitrary families of sets in infinite matroids, and use it to develop the theory of infinite matroids in several as-yet-unexplored areas. Our results include a complete theory of single-element extensions, a description of the relationship between quotients and projections, a proof that matroids for which every flat is modular must be finitary, and two new perspectives on the infinite matroid connectivity parameter \lambda. In most cases, existing theory for finite matroids either fails completely or does not extend in obvious ways, and as a result we develop multiple new techniques for reasoning about infinite matroids, including establishing well-behaved infinite analogues of nullity, local connectivity and skewness. We also point to an online repository containing formalized proofs of all our results using the lean4 proof assistant

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper generalizes the notion of a modular pair from finite matroids to arbitrary families of sets in infinite matroids. It develops a complete theory of single-element extensions, describes the relationship between quotients and projections, proves that matroids in which every flat is modular must be finitary, and provides two new perspectives on the infinite matroid connectivity parameter λ. The work introduces infinite analogues of nullity, local connectivity, and skewness, with all results supported by a complete Lean4 formalization.

Significance. If the central generalization holds, the results fill important gaps in infinite matroid theory where finite-case techniques fail to extend. The complete single-element extension theory and the finitary characterization of matroids with modular flats are likely foundational. The machine-checked Lean4 proofs constitute a notable strength, supplying direct evidence that the new notions are consistent and free of hidden inconsistencies when moving beyond finite matroids.

minor comments (2)
  1. The abstract states that an online repository contains the formalized proofs; the published version should include a stable, citable link or DOI to this repository.
  2. Notation for the new infinite analogues (nullity, local connectivity, skewness) should be introduced with explicit comparison to their finite counterparts in an early section to aid readers familiar with the finite theory.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment and the recommendation of minor revision. The report contains no major comments requiring point-by-point rebuttal.

Circularity Check

0 steps flagged

No significant circularity; new definition yields formally verified results

full rationale

The paper defines a generalization of modular pairs to arbitrary families of sets in infinite matroids and derives theorems (single-element extensions, quotients/projections relation, finitary property for modular-flat matroids, new views on λ) from this definition using new techniques for nullity, local connectivity and skewness. No equation or claim reduces to a prior fitted parameter, self-referential definition, or load-bearing self-citation. The complete Lean4 formalization of all stated results supplies machine-checked, independent verification that the new notions are consistent and well-behaved, satisfying the criterion for non-circular external support. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claims rest on the standard axiomatic definition of (infinite) matroids together with the new generalization of modular pairs; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Standard axioms for matroids, extended to the infinite case as in prior literature
    The paper assumes the usual definition of infinite matroids and builds the modular-pair generalization on top of it.

pith-pipeline@v0.9.0 · 5444 in / 1429 out tokens · 45643 ms · 2026-05-09T23:51:44.118239+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    J. E. Bonin, W. R. Schmitt, Splicing matroids, Eur. J. Combin. 32 (2011), 722–744

    work page 2011

  2. [2]

    Bowler, J

    N. Bowler, J. Carmesin, An excluded minors method for infinite matroids, J. Combin. Theory Ser. B 128 (2018), 104–113

    work page 2018

  3. [3]

    Bowler and S

    N. Bowler and S. Geschke, Self-dual uniform matroids on infinite sets, Proc. Amer. Math. Soc. 144 (2016), 459 – 471

    work page 2016

  4. [4]

    Bruhn, R

    H. Bruhn, R. Diestel, Infinite matroids in graphs, Discrete Math. 311 (2011), 1461–1471

    work page 2011

  5. [5]

    Bruhn, R

    H. Bruhn, R. Diestel, M. Kriesell, R. Pendavingh, P. Wollan, Axioms for infinite matroids, Adv. Math. 239 (2013), 18–46. 54 EHATAMM, NELSON, AND RIVERA OMAÑA

    work page 2013

  6. [6]

    Bruhn, P

    H. Bruhn, P. Wollan, Finite connectivity in infinite matroids, Eur. J. Com- bin. 33 (2012), 1900–1912

    work page 2012

  7. [7]

    H. H. Crapo, Single-element extensions of matroids, J. Res. Nat. Bur. Standards Sect. B 69B (1965), 55–65

    work page 1965

  8. [8]

    Edmonds, Matroid intersection, Ann

    J. Edmonds, Matroid intersection, Ann. Discr. Math 4 (1979), 39–49

    work page 1979

  9. [9]

    Hochstättler, S

    W. Hochstättler, S. Kromberg, Adjoints and duals of matroids linearly rep- resentable over a skewfield, Mathematica Scandanavica 78 (1996), 5–12

    work page 1996

  10. [10]

    Geelen, B

    J. Geelen, B. Gerards, G.Whittle, MatroidT-connectivity, SIAM J. Discrete Math. 20 (2006), 588–596

    work page 2006

  11. [11]

    Gollin, A

    J. Gollin, A. Joó, Wild generalised truncation of infinite matroids, arXiv:2504.05064 [math.CO]

    work page arXiv

  12. [12]

    Geelen, R

    J. Geelen, R. Kapadia, Representation of matroids with a modular plane, arXiv:1304.6448 [math.CO]

    work page arXiv

  13. [13]

    Geelen, P

    J. Geelen, P. Nelson, The structure of matroids with a spanning clique or projective geometry, J. Combin. Theory Ser. B 127 (2017), 65-81

    work page 2017

  14. [14]

    Higgs, Equicardinality of bases inB-matroids, Can

    D.A. Higgs, Equicardinality of bases inB-matroids, Can. Math. Bull 12 (1969), 861–862

    work page 1969

  15. [15]

    Higgs, Matroids and duality, Colloq

    D.A. Higgs, Matroids and duality, Colloq. Math. 20 (1969), 215 – 220

    work page 1969

  16. [16]

    Kapadia, Matroids with a modular4-point line, SIAM J

    R. Kapadia, Matroids with a modular4-point line, SIAM J. Discrete Math. 28 (2014), 862–877

    work page 2014

  17. [17]

    de Moura, S

    L.M. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language. In: CADE (2021)

    work page 2021

  18. [18]

    Oxley, A matroid extension result, SIAM J

    J. Oxley, A matroid extension result, SIAM J. Discrete Math. 33 (2019), 138–152

    work page 2019

  19. [19]

    In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp

    The mathlib Community, The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367–381. Association for Computing Machinery, New York (2020)

    work page 2020

  20. [20]

    The mathlib Community, mathlib4, https://github.com/leanprover- community/mathlib4, (GitHub repository)

    work page

  21. [21]

    Nelson,Matroid, https://github.com/apnelson1/Matroid, (GitHub repos- itory)

    P. Nelson,Matroid, https://github.com/apnelson1/Matroid, (GitHub repos- itory)

    work page

  22. [22]

    Oxley, Matroid Theory (second edition), Oxford University Press, 2011

    J. Oxley, Matroid Theory (second edition), Oxford University Press, 2011

    work page 2011

  23. [23]

    Sachs, Partition and modulated lattices, Pacific J

    D. Sachs, Partition and modulated lattices, Pacific J. Math. 11 (1961), 325– 345

    work page 1961

  24. [24]

    H.Whitney, Ontheabstractpropertiesoflineardependence, Amer. J.Math. 57 (1935), 509–533. MODULARITY, EXTENSIONS, AND CONNECTIVITY IN INFINITE MATROIDS 55 Appendix A : Formalization Formalized Proofs.A proof assistant (such aslean4) is a piece of software that can check an appropriately written proof for correctness. Preparing a proof in a form that can be ...

    work page 1935