Finite positive-circuit completeness for nonnegative-kernel dual tests
ProvedHirsch.finite_positive_circuit_dual_testsFor any real linear map A from R^n to R^k, there is a fixed family c indexed by the subsets of the n coordinate indices. Each c_s is either zero or a nonzero nonnegative null vector of A with support exactly s, minimal among supports of nonzero nonnegative null vectors. The family depends on A but not on a subsequent real linear functional b. For every b, nonnegativity of b on the whole nonnegative kernel of A is equivalent to nonnegativity on all the c_s. Thus one representative per positive-circuit support suffices for every linear dual test. Unused support slots are zero; at most 2^n slots are available. The statement neither assumes a circuit-generation/Farkas theorem nor asserts a polynomial circuit count, the sharper rank(A)+1 support bound, an executable enumerator, geometric Minkowski reconstruction, or Polynomial Hirsch.
import Mathlib open scoped BigOperators
namespace Hirsch
theorem finite_positive_circuit_dual_tests (n k : ℕ)
(A : (Fin n → ℝ) →ₗ[ℝ] (Fin k → ℝ)) :
∃ c : Finset (Fin n) → (Fin n → ℝ),
(∀ s, c s = 0 ∨
((∀ i, 0 ≤ c s i) ∧ A (c s) = 0 ∧ c s ≠ 0 ∧
Function.support (c s) = (s : Set (Fin n)) ∧
∀ y : Fin n → ℝ, (∀ i, 0 ≤ y i) → A y = 0 → y ≠ 0 →
Function.support y ⊆ Function.support (c s) →
Function.support (c s) ⊆ Function.support y)) ∧
∀ b : (Fin n → ℝ) →ₗ[ℝ] ℝ,
(∀ x : Fin n → ℝ, (∀ i, 0 ≤ x i) → A x = 0 → 0 ≤ b x) ↔
∀ s, 0 ≤ b (c s) := by sorry
end Hirsch