Correctness of finite matrix tests

The domain test uses the size-two extension f + 1: at a defined point, either f is nonzero or f + 1 is nonzero. A hitting list for both therefore contains a point in the domain of f, even if f is identically zero.

theorem Complexity.RationalHitting.Internal.matrix_inverse_left {d : ℕ} (a : Mat d) (ha : Matrix.det a ≠ 0) : a * (Matrix.det a)⁻¹ • Matrix.adjugate a = 1

theorem Complexity.RationalHitting.Internal.matrix_inverse_right {d : ℕ} (a : Mat d) (ha : Matrix.det a ≠ 0) : (Matrix.det a)⁻¹ • Matrix.adjugate a * a = 1

theorem Complexity.RationalHitting.Internal.evalMatrix_sound {n d : ℕ} (f : Formula n) (X : Tuple n d) {v : Mat d} (h : f.evalMatrix? X = some v) : Evaluates f X v

theorem Complexity.RationalHitting.Internal.evalMatrix_complete {n d : ℕ} {f : Formula n} {X : Tuple n d} {v : Mat d} (h : Evaluates f X v) : f.evalMatrix? X = some v

theorem Complexity.RationalHitting.Internal.nonzero_admissible {n : ℕ} {f : Formula n} (hf : Nonzero f) : Admissible f

theorem Complexity.RationalHitting.Internal.hits_nonzero_iff {n s : ℕ} {H : Output n} (hH : Hits s H) (f : Formula n) (hf : f.size ≤ s) : Nonzero f ↔ ∃ X ∈ H.tuples, ∃ (v : Mat H.dimension), Evaluates f X v ∧ IsUnit v

theorem Complexity.RationalHitting.Internal.admissible_nonzero_or_add_one {n : ℕ} (f : Formula n) (hf : Admissible f) : Nonzero f ∨ Nonzero (f.add (Formula.const 1))

theorem Complexity.RationalHitting.Internal.hits_admissible_iff {n s : ℕ} {H : Output n} (hH : Hits (s + 2) H) (f : Formula n) (hf : f.size ≤ s) : Admissible f ↔ ∃ X ∈ H.tuples, ∃ (v : Mat H.dimension), Evaluates f X v

theorem Complexity.RationalHitting.Internal.hits_admissible_inv_iff_nonzero {n s : ℕ} {H : Output n} (hH : Hits s H) (f : Formula n) (hf : f.size ≤ s) : Admissible f.inv ↔ Nonzero f

theorem Complexity.RationalHitting.Internal.admissibilityTest_iff {n : ℕ} (H : Output n) (f : Formula n) : H.admissibilityTest f = true ↔ ∃ X ∈ H.tuples, ∃ (v : Mat H.dimension), Evaluates f X v

theorem Complexity.RationalHitting.Internal.nonzeroTest_iff {n : ℕ} (H : Output n) (f : Formula n) : H.nonzeroTest f = true ↔ ∃ X ∈ H.tuples, ∃ (v : Mat H.dimension), Evaluates f X v ∧ IsUnit v

theorem Complexity.RationalHitting.Internal.hits_admissibilityTest_eq_true_iff {n s : ℕ} {H : Output n} (hH : Hits (s + 2) H) (f : Formula n) (hf : f.size ≤ s) : H.admissibilityTest f = true ↔ Admissible f

theorem Complexity.RationalHitting.Internal.hits_nonzeroTest_eq_true_iff {n s : ℕ} {H : Output n} (hH : Hits s H) (f : Formula n) (hf : f.size ≤ s) : H.nonzeroTest f = true ↔ Nonzero f