OAI.InfiniteMatroidCounterexample.main
OpenThe theorem states that the ground type E = ℤ × D, where D is the type of pairs consisting of a natural number m and a Boolean function on Boolean m-tuples, is countable and infinite, and that there exist two matroids M₀ and M₁ on E, each with ground set all of E, each equal to its own dual, such that no independent set of M₀ and independent set of M₁ have union all of E. Yet the pair fails HasPackingCovering. That predicate asks for a partition of the common ground set into P and C, two disjoint subsets S₀ and S₁ of P that are spanning in the restrictions M₀|P and M₁|P respectively, and subsets I₀ and I₁ of C that are independent in the contractions of M₀ and M₁ onto C (the dual of the restriction of the dual to C), with I₀ ∪ I₁ = C. So the theorem asserts a countably infinite pair of self-dual matroids with no such packing-covering decomposition.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/InfiniteMatroid.lean; bytes 690..1022 -- Kind: theorem; original declaration names and bodies preserved. -- Source groups are independent. Target: Lean 4.33.1; see compilation.json. import Mathlib import Definitions.Def_InfiniteMatroid namespace OAI namespace InfiniteMatroidCounterexample open Matroid
theorem main :
Countable E ∧ Infinite E ∧
∃ M₀ M₁ : Matroid E,
M₀.E = Set.univ ∧ M₁.E = Set.univ ∧
M₀.dual = M₀ ∧ M₁.dual = M₁ ∧
(∀ I₀ I₁ : Set E, M₀.Indep I₀ → M₁.Indep I₁ → I₀ ∪ I₁ ≠ Set.univ) ∧
¬ HasPackingCovering M₀ M₁ := by
sorry
end InfiniteMatroidCounterexample
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.