Deficit two: the union of two skew omitted circuits is an actual minimal witness (Erdős 624)
ProvedErdos624.skew_omitted_union_witnessSetting: is a finite set of inputs, an arbitrary list map (the actual colour lists), a natural number. A colour is nonbottom if and covering if every -subset contains some with . An actual minimal witness of is with and for every . A valid label for is a map into an -vector space with for every actual minimal witness with . For , and (the dimension of the valid parity space). Theorem. Let be nonbottom and covering with valid label of global rank (stated as ). Let be disjoint, nonempty, with , such that the only zero-sum subsets of are , and with , , . Then is an actual minimal witness of : and for all .
Source: converse half of the deficit-two classification in 'Actual Witness Spans and Intrinsic Kernel Diversity'. Note: the source derives from exact global rank ; here it is an explicit hypothesis, and 'genuine hole' is weakened to , .
Context: Erdős Problem 624 asks whether , where is the least such that some with satisfies for all . This is an auxiliary finite statement from Sol's Round 13 notes on the two-track (PAIR) case. It does not settle Erdős Problem 624, PAIR or Step 17; the initial near-critical population those notes start from is not established.
import Mathlib open Finset
namespace Erdos624
theorem skew_omitted_union_witness {U : Type*} [Fintype U] [DecidableEq U] {C : Type*} [DecidableEq C]
{W : Type*} [AddCommGroup W] [Module (ZMod 2) W]
(L : Finset U → Finset C) (k : ℕ) (u : C) (hu : u ∉ L ∅)
(hcov : ∀ Y : Finset U, #Y = k → ∃ A ⊆ Y, u ∈ L A)
(p : U → W)
(hvalid : ∀ F : Finset U, 0 < #F → #F ≤ k → u ∈ L F → (∀ F' ⊂ F, u ∉ L F') →
∑ x ∈ F, p x = 0)
(hglob : k ≤ Module.finrank (ZMod 2) (Submodule.span (ZMod 2) (Set.range p)) + 2)
(A B : Finset U) (hAB : Disjoint A B) (hA : A.Nonempty) (hB : B.Nonempty)
(hA0 : ∑ x ∈ A, p x = 0) (hB0 : ∑ x ∈ B, p x = 0)
(hzs : ∀ G ⊆ A ∪ B, ∑ x ∈ G, p x = 0 → G = ∅ ∨ G = A ∨ G = B ∨ G = A ∪ B)
(huA : u ∉ L A) (huB : u ∉ L B) (hk : #(A ∪ B) ≤ k) :
u ∈ L (A ∪ B) ∧ ∀ F' ⊂ A ∪ B, u ∉ L F' := by sorry
end Erdos624