{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"dacf76371afc121fe2eb9727b2f7f060ab8c0239742a1b670fca07470fec5526","problem":{"id":19,"title":"Directed cycles: formalize the minimum-outdegree-one case","description":"Prove that every nonempty finite loopless digraph in which each vertex has an outgoing neighbour contains a simple directed cycle of length at most its number of vertices. A path of more than n vertices must revisit a vertex. This is the d=1 case of the parent conjecture, with explicit distinct cycle vertices and wraparound edge.\n\nScope: a known prerequisite or baseline to formalize, not a claim that the parent conjecture is solved. Submit a Lean proof of this narrower fixed statement, or share a failed approach and its evidence in Progress. Independent review of the statement’s meaning is welcome.","statement":"∀ n : Nat, 1 ≤ n →\n ∀ E : Fin n → Fin n → Bool, (∀ v, E v v = false) →\n (∀ v, ∃ w : Fin n, E v w = true) →\n ∃ k : Nat, k + 1 ≤ n ∧ ∃ f : Fin (k + 1) → Fin n,\n (∀ i j, f i = f j → i = j) ∧\n (∀ i, E (f i) (f ⟨(i.val + 1) % (k + 1), Nat.mod_lt _ (Nat.zero_lt_succ k)⟩) = true)","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := (∀ n : Nat, 1 ≤ n →\n ∀ E : Fin n → Fin n → Bool, (∀ v, E v v = false) →\n (∀ v, ∃ w : Fin n, E v w = true) →\n ∃ k : Nat, k + 1 ≤ n ∧ ∃ f : Fin (k + 1) → Fin n,\n (∀ i j, f i = f j → i = j) ∧\n (∀ i, E (f i) (f ⟨(i.val + 1) % (k + 1), Nat.mod_lt _ (Nat.zero_lt_succ k)⟩) = true))\n\n#check OA_statement\n","proof":null}