An exact rational certificate checker produces the complete real positive-circuit catalogue
ProvedHirsch.checked_rational_circuit_catalogue_exactFor a rational k-by-n matrix A, enumerate all supports of size at most k+1. On every support supply either a nonzero supported rational vector annihilated by A and by the total-mass row, or rational coefficients forming a left inverse of the augmented supported system [A;ones]. A finite executable Boolean verifies these identities. If it returns true, the exact rational filter of the left-inverse solutions (full positive support, original null equations, total mass one) is precisely the set of all normalized support-minimal nonnegative REAL null vectors of A. No RREF, numerical rank, vertex enumeration, feasibility, catalogue-completeness or algorithm-correctness oracle is assumed. The witnesses are finite arithmetic data, not semantic completeness assumptions. The source reuses the accepted positive-circuit signed-ray/rank proof and includes kernel-evaluated positive, negative and output-count examples. It does not claim a polynomial bound for unbounded k, verify a JSON decoder, guarantee arbitrary solver termination, or give original-polytope edge routes.
import Mathlib open scoped BigOperators
namespace Hirsch
theorem checked_rational_circuit_catalogue_exact (n k : ℕ) (A : Fin k → Fin n → ℚ)
(tag : Finset (Fin n) → Bool)
(L : Finset (Fin n) → Fin n → Option (Fin k) → ℚ)
(z : Finset (Fin n) → Fin n → ℚ) :
let U := (Finset.range (k + 2)).biUnion
(fun r => (Finset.univ : Finset (Fin n)).powersetCard r)
let c : Finset (Fin n) → Fin n → ℚ := fun s i => if i ∈ s then L s i none else 0
decide (∀ s ∈ U, if tag s then
(∃ i, z s i ≠ 0) ∧ (∀ i, i ∉ s → z s i = 0) ∧
(∀ r, (∑ i, A r i * z s i) = 0) ∧ (∑ i, z s i) = 0
else ∀ i ∈ s, ∀ j ∈ s,
(∑ r, L s i (some r) * A r j) + L s i none = if i = j then 1 else 0) = true →
∀ x : Fin n → ℝ,
((∀ i, 0 ≤ x i) ∧ (∀ r, (∑ i, (A r i : ℝ) * x i) = 0) ∧
(∑ i, x i) = 1 ∧
∀ y : Fin n → ℝ, (∀ i, 0 ≤ y i) →
(∀ r, (∑ i, (A r i : ℝ) * y i) = 0) → y ≠ 0 →
Function.support y ⊆ Function.support x → Function.support x ⊆ Function.support y) ↔
∃ q ∈ (U.filter (fun s => tag s = false ∧ (∀ i ∈ s, 0 < L s i none) ∧
(∀ r, (∑ i, A r i * c s i) = 0) ∧ (∑ i, c s i) = 1)).image c,
x = fun i => (q i : ℝ) := by sorry
end Hirsch