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 node-count bound, it also detects admissibility, including for identically zero formulas: at a defined point, either f or f + 1 is nonzero. The executable tests here have correctness proofs; no polynomial bound for their rational arithmetic is asserted.

Main results

• Cslib.Circuits.Rational.Formula.evalMatrix?_eq_some_iff: the executable evaluation returns exactly the values of the evaluation relation.
• Cslib.Circuits.Rational.admissible_nonzero_or_add_one: at a defined point, f or f + 1 is nonzero.
• Cslib.Circuits.Rational.Hits.nonzero_iff, Cslib.Circuits.Rational.Hits.admissible_iff, Cslib.Circuits.Rational.Hits.admissible_inv_iff_nonzero: a hitting list detects nonzeroness and admissibility.
• Cslib.Circuits.Rational.Hits.admissibilityTest_eq_true_iff, Cslib.Circuits.Rational.Hits.nonzeroTest_eq_true_iff: the finite tests decide admissibility and nonzeroness.

References

• From the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787 (files Complexitylib/RationalHitting/Evaluation.lean and Complexitylib/RationalHitting/Internal/Detection.lean), built on OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.Nonzero.admissible {n : ℕ} {f : Formula n} (hf : Nonzero f) : Admissible f

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

theorem Cslib.Circuits.Rational.Hits.nonzero_iff {n s : ℕ} {H : Output n} (hH : Hits s H) (f : Formula n) (hf : f.nodeCount ≤ 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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.Hits.admissible_iff {n s : ℕ} {H : Output n} (hH : Hits (s + 2) H) (f : Formula n) (hf : f.nodeCount ≤ s) : Admissible f ↔ ∃ X ∈ H.tuples, ∃ (v : Mat H.dimension), Evaluates f X v

A hitting list with an allowance of two more nodes also detects the domain of every formula.

theorem Cslib.Circuits.Rational.Hits.admissible_inv_iff_nonzero {n s : ℕ} {H : Output n} (hH : Hits s H) (f : Formula n) (hf : f.nodeCount ≤ s) : Admissible f.inv ↔ Nonzero f

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

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.Hits.admissibilityTest_eq_true_iff {n s : ℕ} {H : Output n} (hH : Hits (s + 2) H) (f : Formula n) (hf : f.nodeCount ≤ s) : H.admissibilityTest f = true ↔ Admissible f

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

theorem Cslib.Circuits.Rational.Hits.nonzeroTest_eq_true_iff {n s : ℕ} {H : Output n} (hH : Hits s H) (f : Formula n) (hf : f.nodeCount ≤ s) : H.nonzeroTest f = true ↔ Nonzero f

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