graph_verdict tool v0.1

STEP: 1523 / Test: 35/35 PASS / Lean 4: 6 theorem zero sorry / Type: STEP 1486 離散数学 2nd tool (47 defer 全体 14 番目)

❶ Adjacency list → 7-verdict classification: self-loop → SELF ★ / no edges → ZERO / tree → TRUE / cyclic → BOTH / disconnected acyclic → NEITHER。

❷ directed/undirected 両対応、 3-color DFS で directed cycle 検出、 parent-tracking DFS で undirected cycle 検出。

❸ 姉妹 verdict tool 17 揃った。

決定表 (7 case)

ConditionVerdictReason
self-loop presentSELF ★self_loop_detected
0 edges (isolated)ZEROno_edges_isolated
connected + acyclic (tree/DAG)TRUEconnected_acyclic
connected + cyclicBOTHconnected_cyclic
disconnected + cyclicBOTHdisconnected_cyclic
disconnected + acyclicNEITHERdisconnected_acyclic
invalid inputNEITHERinvalid_input

使用例

// Triangle → BOTH (connected cyclic)
graphVerdict({ numVertices: 3, edges: [[0,1], [1,2], [2,0]] });

// Path graph → TRUE (tree)
graphVerdict({ numVertices: 3, edges: [[0,1], [1,2]] });

// Directed DAG
graphVerdict({ numVertices: 3, edges: [[0,1], [1,2], [0,2]], directed: true });
// { verdict: 'TRUE', reason: 'connected_acyclic' }

// Self-loop
graphVerdict({ numVertices: 2, edges: [[0,0], [0,1]] });
// { verdict: 'SELF', reason: 'self_loop_detected' }

Lean 4 (6 theorem zero sorry)

graph_self_loop_gives_self          : self-loop → SELF
graph_no_edges_gives_zero           : 0 edges → ZERO
graph_connected_cyclic_gives_both   : connected + cyclic → BOTH
graph_tree_gives_true               : connected + acyclic → TRUE
graph_disconnected_cyclic_gives_both : disconnected + cyclic → BOTH
graph_disconnected_acyclic_gives_neither : disconnected + acyclic → NEITHER

Honest scope

❶ BFS/DFS 標準実装のみ、 weighted graph / flow / matching 未 embed。

❂ 「世界初」 なし = Euler 1736 (Königsberg) 既知 D-FUMT₈ mapping。

❸ 累計 defer 35 → 34。