Finite rational cone duality

A finite family of integral vectors admits a normalized nonnegative linear functional whenever the negative normalizing vector has no positive integral multiple in the monoid generated by the family.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_normalized_nonneg_linear_of_no_nat_certificate_of_isClosed {I : Type u_1} {J : Type u_2} [Fintype I] [Finite J] (A : I → J → ℤ) (u : J → ℤ) (hclosed : IsClosed ↑(PointedCone.hull ℝ (Set.range fun (i : I) (j : J) => ↑(A i j)))) (hno : ¬∃ (D : ℕ), 0 < D ∧ ∃ (c : I → ℕ), ∀ (j : J), ∑ i : I, ↑(c i) * A i j = -↑D * u j) : ∃ (L : (J → ℝ) →ₗ[ℝ] ℝ), (L fun (j : J) => ↑(u j)) = 1 ∧ ∀ (i : I), 0 ≤ L fun (j : J) => ↑(A i j)

Closed-cone separation followed by rational certificate extraction yields a normalized nonnegative linear functional.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_normalized_nonneg_linear_of_no_nat_certificate {I : Type u_1} {J : Type u_2} [Fintype I] [Finite J] (A : I → J → ℤ) (u : J → ℤ) (hno : ¬∃ (D : ℕ), 0 < D ∧ ∃ (c : I → ℕ), ∀ (j : J), ∑ i : I, ↑(c i) * A i j = -↑D * u j) : ∃ (L : (J → ℝ) →ₗ[ℝ] ℝ), (L fun (j : J) => ↑(u j)) = 1 ∧ ∀ (i : I), 0 ≤ L fun (j : J) => ↑(A i j)

A finite integral cone either contains a positive integer multiple of the negative normalizing vector, or admits a linear functional which is nonnegative on the generators and takes value one on that vector.