Math and TheoryStructural selfadhesivity does not imply a numerically selfadhesive realization
Problem and result
- Problem
- Boege's selfadhesivity question: structural vs numerical selfadhesive polymatroids
- Posed in
- Boege, IJAR 2023 (arXiv:2205.07667), Question 4.18 (4.14 in the PDF version)
- Status
- Answered negatively
- Result
- An explicit five-variable conditional-independence model with 26 of the 80 elementary CI statements is structurally selfadhesive at every overlap, yet no real polymatroid inducing it is selfadhesive in Matúš's numerical sense.
Abstract
An explicit conditional-independence model on five variables, with 26 of the 80 elementary statements, admits for every overlap an adhesive polymatroid gluing whose two restrictions both induce it, yet no real polymatroid inducing it is selfadhesive in Matúš's numerical sense. This answers negatively Question 4.18 of Boege, who asked whether every structurally selfadhesive structural semigraphoid is induced by a selfadhesive polymatroid; his computation gave a positive answer for four variables. The positive part is certified by 32 integer polymatroids, the negative part by an exact identity among 51 nonnegative conditional mutual informations valid for every real inducing profile.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Entropy and conditional independence
- Subject
- Discrete analysis, tilings, probability and entropy
- Result type
- Counterexample answering a published question and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
structural-selfadhesivity- Keywords
- conditional independence, polymatroids, selfadhesivity, adhesive extensions, entropy region, Shannon inequalities, copy lemma, Boege
Statement and scope
Formal scope. Both parts are formalized in Lean for arbitrary real polymatroids, with actual subset and relabeling semantics, all 32 overlap witnesses and the exact separating identity. The minimality suggested by Boege's four-variable computation is a literature consequence and is not formalized.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf333 KB- PDF on GitHub
papers/mathematics/ structural-selfadhesivity/ manuscript.pdf - LaTeX source
papers/mathematics/ structural-selfadhesivity/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ structural-selfadhesivity/ - Lean project
papers/48 Lean filesmathematics/ structural-selfadhesivity/ proof/ e3_lean/ - Lakefile
papers/mathematics/ structural-selfadhesivity/ proof/ e3_lean/ lakefile.toml - Toolchain
leanprover/lean4:v4.35.0-rc3 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Exact certificates
python3 proof/E3_all_overlap_check.py proof/E3_all_overlap_polymatroids.json --output /tmp/e3-positive-check.json
python3 proof/E3_negative_check.py
python3 proof/E3_lean_witness_correspondence.pyLean
python3 proof/verify_E3.py --lake lake --reuse-packages "$PWD/proof/e3_lean/.lake/packages" --output /tmp/e3-verification- README
papers/mathematics/ structural-selfadhesivity/ README.md - Verification guide
papers/mathematics/ structural-selfadhesivity/ verification/ README.md - Verification record
papers/mathematics/ structural-selfadhesivity/ VERIFICATION.md - Authorship
papers/mathematics/ structural-selfadhesivity/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. Boege, 2023.
Questions and answers
Does structural selfadhesivity imply a numerically selfadhesive realization?
No. The preprint gives a five-variable CI model, with 26 of the 80 elementary statements, that has an adhesive gluing at all 32 overlaps but no selfadhesive inducing polymatroid, answering Boege's Question 4.18 negatively. Boege's computation gave a positive answer for four variables; the result does not characterize the five-variable entropy cone.
Is there earlier related work?
Yes. Boege, Bolt and Studený (DAM 2025) proved that numerical selfadhesivity implies the structural notion, and a neighbouring five-variable counterexample to their Open Problem 3 appeared in the ScaleMath repository in August 2026; its face-search and exact-identity methods are credited. Historical priority is not certified.
Is the proof formally verified?
Both parts are formalized in Lean 4 for arbitrary real polymatroids, with all 32 overlap witnesses and the exact separating identity. Minimality relative to Boege's four-variable computation is a literature consequence and is not formalized.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026structuralselfadhesivity,
author = {Goyal, Dev D.},
title = {A Five-Variable Separation between Structural and Numerical Selfadhesivity},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/structural-selfadhesivity}
}