Exact matrix evaluation and consequences of hitting lists

These deductions use OpenAI's rational-formula semantics. Inverse is partial: every evaluated inverse node must have a genuine two-sided inverse.

A hitting list detects nonzeroness by an invertible value. With two extra syntax nodes in the size bound, it also detects admissibility, including for identically zero formulas. The executable tests here have correctness proofs; no polynomial bound for their rational arithmetic is asserted.

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

The executable evaluator returns exactly the values admitted by the evaluation relation.

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

A nonzero evaluation already supplies a point in the formula's domain.

theorem Complexity.RationalHitting.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

Positive dimension makes an invertible hitting value a nonzero witness.

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

At any defined point, either the value of f or the value of f + 1 is nonzero.

theorem Complexity.RationalHitting.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

A hitting list with a size allowance of two also detects the domain of every formula.

theorem Complexity.RationalHitting.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

An invertible hit turns a nonzero formula into one with an admissible inverse.

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

The executable domain test searches exactly the defined evaluations on the list.

theorem Complexity.RationalHitting.Output.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

The executable determinant test searches exactly the invertible evaluations on the list.

theorem Complexity.RationalHitting.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

A hitting list for size s + 2 decides admissibility of formulas of size at most s.

theorem Complexity.RationalHitting.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

A hitting list for size s decides nonzeroness of formulas of size at most s.