HEXAGONbeta

An intrinsic interval-deletion characterization of digraph support families

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatoricscs.LO — Logic in Computer Science

Contributed by Michael Mislan ↗

Version 1 / Oct 20, 2026 / CC BY 4.0

Abstract

For a finite directed graph with loops allowed, its supported subsets are those in which every vertex has an in-neighbour within the subset. We characterize exactly which set families arise this way on their original ground set. Starting from the power set, a legal step chooses an inclusion-maximal remaining nonmember, selects a previously unused root absent from every target-family member below it, and deletes the rooted interval. A family is a digraph support family if and only if some legal deletion sequence reaches it. The maximal residual set may follow any fixed valid policy; only roots require branching. Successful traces have at most one step per vertex and reconstruct a realizing digraph. Consequences include exact root sets and trace length, a finite recognizer, conventional NP membership for explicit lists, projection, deletion and product closure, and RAF realizability criteria using the published antimatroid characterization. The characterization and selected consequences and trace-checking interfaces are verified in Lean 4; conventional statements and computational examples are identified separately.

Provenance statement

The text is primarily AI-generated. AI systems assisted the mathematical development, computations and Lean formalization under human direction; human understanding covers some parts of the work.

Formalizations

References

  1. Angluin, Dana; Frazier, Michael; Pitt, Leonard. Learning conjunctions of Horn clauses. Machine Learning, vol. 9, no. 2–3, pp. 147–164. 1992DOI
  2. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 theorem prover and programming language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021DOI
  3. Dowling, William F.; Gallier, Jean H. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, vol. 1, no. 3, pp. 267–284. 1984DOI
  4. Edelman, Paul H.; Jamison, Robert E. The theory of convex geometries. Geometriae Dedicata, vol. 19, no. 3, pp. 247–270. 1985DOI
  5. Fulkerson, Delbert R.; Gross, Oliver A. Incidence matrices and interval graphs. Pacific Journal of Mathematics, vol. 15, no. 3, pp. 835–855. 1965DOI
  6. Ganter, Bernhard. Two basic algorithms in concept analysis. Formal Concept Analysis (ICFCA 2010), vol. 5986, pp. 312–340. 2010. Reprint of the 1984 Technische Hochschule Darmstadt preprint FB4-831DOI
  7. Hordijk, Wim; Steel, Mike. Detecting autocatalytic, self-sustaining sets in chemical reaction systems. Journal of Theoretical Biology, vol. 227, no. 4, pp. 451–461. 2004DOI
  8. Kauffman, Stuart A. Autocatalytic sets of proteins. Journal of Theoretical Biology, vol. 119, no. 1, pp. 1–24. 1986DOI
  9. Korte, Bernhard; Lovász, László; Schrader, Rainer. Greedoids. Springer, vol. 4. 1991
  10. Liberatore, Paolo. Common equivalence and size after forgetting. 2020. arXiv:2006.11152
Show all 16 referencesShow fewer references
  1. Liberatore, Paolo. Reconstructing a single-head formula to facilitate logical forgetting. Journal of Logic and Computation, vol. 33, no. 7, pp. 1596–1624. 2023DOI
  2. Mislan, Michael. Antimatroid characterization of RAF interior operators. 2026. Version 1.0. Preprint. Zenodo. 10.5281/zenodo.23459454DOI
  3. Steel, Mike. Interior operators and their relationship to autocatalytic networks. Acta Biotheoretica, vol. 71, no. 4, pp. 21. 2023. arXiv:2305.16714arXivDOI
  4. Steel, Mike; Hordijk, Wim; Xavier, Joana C. Autocatalytic networks in biology: structural theory and algorithms. Journal of the Royal Society Interface, vol. 16, no. 151, pp. 20180808. 2019DOI
  5. The mathlib Community. The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. 2020DOI
  6. Wild, Marcel. The joy of implications, aka pure Horn formulas: Mainly a survey. Theoretical Computer Science, vol. 658, pp. 264–292. 2017DOI

Version history

  1. v1Submitted by Michael MislanInitial depositCurrentOct 19, 2026