Math and TheoryAn entropy increase for a structurally disassortative DomiRank graph
Problem and result
- Problem
- Zhang–Zhao DomiRank entropy monotonicity conjecture for disassortative graphs
- Posed in
- Zhang and Zhao, arXiv:2610.00107v4, Conjecture 4.9
- Status
- Disproved
- Result
- A connected graph with 14 vertices and 32 edges has negative degree–log-degree edge covariance and positive DomiRank scores on [251/1000, 63/250], yet its entropy increases by more than 1/10000 nats across that interval.
Abstract
A connected graph with 14 vertices and 32 edges has negative degree–log-degree edge covariance. All resolvent scores are positive on [251/1000,63/250] inside the stable domain. Its entropy nevertheless increases by more than 1/10000 in natural-logarithm units. This refutes the source’s assertion for every positive-score interval.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Graph theory and matrix analysis
- Subject
- Graph theory and graph polynomials
- Result type
- Counterexample to an interval monotonicity conjecture
- Formal proof
- Shared Lean library
- Family
domirank-entropy- Keywords
- DomiRank, network centrality, graph entropy, disassortative graphs, resolvent centrality
Statement and scope
Result summary. The catalogue summary repeats the abstract above, including its stated limits. The formally checked statements are listed under Formal proof.
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.pdf298 KB- PDF on GitHub
papers/mathematics/ domirank-entropy/ paper.pdf - LaTeX source
papers/mathematics/ domirank-entropy/ paper.tex - Bibliography
papers/mathematics/ domirank-entropy/ references.bib
Formal proof
The selected theorems of this result are proved in the shared Lean 4 library of the repository. Its Comparator configuration checks each one against the matching statement in the Challenge module and permits only the axioms propext, Classical.choice and Quot.sound.
- Proof module
lean/MathAndTheory/ Mathematics/ DomiRank/ Conclusion.lean - Family sources
lean/MathAndTheory/ Mathematics/ DomiRank/ - Challenge
lean/Challenges/ Mathematics/ DomiRank/ Main.lean - Solution interface
lean/Solutions/ Mathematics/ DomiRank/ Main.lean - Comparator file
lean/comparator/ mathematics/ domirank-entropy.json - Statement guide
lean/docs/ mathematics/ domirank-entropy.md - Toolchain
leanprover/lean4:v4.35.0
Checked theorems
Namespace MathAndTheory.DomiRank
DomiRankProblem.counterexample
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
python3 papers/mathematics/domirank-entropy/verification/scripts/verify.py- README
papers/mathematics/ domirank-entropy/ README.md - Verification guide
papers/mathematics/ domirank-entropy/ verification/ README.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Original problem. Zhang and Zhao, arXiv:2610.00107v4, Conjecture 4.9.
Prior work. The Omega Institute's public repository records a refutation of the broader unconditional assertion of version 1, committed on 5 October 2026 (issue #13267), with a graph that does not satisfy the hypothesis of Conjecture 4.9. Priority and novelty record.
Questions and answers
Is the DomiRank entropy conjecture of Zhang and Zhao true?
No. Conjecture 4.9 asserts that entropy decreases on every interval of positive scores for a structurally disassortative graph; the 14-vertex, 32-edge graph has strictly negative covariance yet h(251/1000) + 1/10000 < h(63/250). The narrower question restricted to the initial component of the positive-score set is not settled.
Is the proof formally verified?
Yes. Lean 4 proves the graph properties, the covariance sign, stability and score positivity on the whole interval, and the entropy increase. The result makes no claim about empirical behaviour on real networks.
Was DomiRank entropy monotonicity refuted before?
The broader unconditional assertion of version 1 was refuted earlier with a six-vertex graph of positive covariance, in the Omega Institute's public repository on 5 October 2026 (issue #13267). That graph does not satisfy the disassortativity hypothesis of Conjecture 4.9, which this counterexample refutes.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026domirankentropy,
author = {Dev D. Goyal},
title = {An entropy increase for a structurally disassortative DomiRank graph},
year = {2026},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/domirank-entropy},
note = {Lean-verified manuscript; not peer reviewed. Cite the repository commit used.}
}