Documentation

Complexity.Computability.Circuit.Rational

Rational hitting lists, nonzeroness, and admissibility #

A noncommutative rational formula is nonzero if it has a defined nonzero value at some substitution of square rational matrices of positive dimension, and admissible if it is defined at some such substitution. For all n and s there is an explicit, executable list of substitutions of rational matrices, of dimension and encoding length polynomial in n + s, at which every admissible nonzero formula in n variables with at most s nodes takes an invertible value somewhere (hittingList_hits). The construction is OpenAI's.

The list yields executable tests for nonzeroness and admissibility, by exact rational matrix evaluation. The admissibility test needs a list for two extra syntax nodes: if f has a defined value, either f or f + 1 has a nonzero value. The correctness theorems do not assert polynomial bit complexity of formula evaluation. The tests are deductions from the source result, without a claim of new priority. The generator's running time is bounded in Complexity.Computability.Circuit.Rational.Runtime: Cslib.Circuits.Rational.hittingList_polytime computes the encoding encodeOutput (hittingList n s) tidily in polynomial time from unary (n, s).

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Rational.hittingList (n s : ℕ) :
Output n

The explicit, executable list of rational matrix substitutions.

Instances For
    source
    theorem Cslib.Circuits.Rational.hits_zero {n : ℕ} (H : Output n) :
    Hits 0 H

    Every list hits the formulas with at most 0 nodes, since every formula has a node.

    source
    theorem Cslib.Circuits.Rational.hittingList_hits (n s : ℕ) :
    Hits s (hittingList n s)

    The generated list hits every admissible nonzero formula with at most s nodes at an invertible value. This holds for all n and s; for s = 0 it is hits_zero.

    source
    theorem Cslib.Circuits.Rational.hittingList_dimension_le (n s : ℕ) :
    (hittingList n s).dimension ≤ 256 * (n + s + 1) ^ 10

    The generated matrices have polynomially bounded dimension.

    source
    theorem Cslib.Circuits.Rational.hittingList_encoding_length_le (n s : ℕ) :
    (encodeOutput (hittingList n s)).length ≤ PolynomialBounds.outputConstant * (n + s + 1) ^ 104

    The complete reduced-rational binary encoding has polynomial length, for all n and s, including n = 0. The constant PolynomialBounds.outputConstant differs from the source's, which assumes 1 ≤ n: covering n = 0 raises the grid-size coefficient from 24577 to 49153.

    source
    theorem Cslib.Circuits.Rational.admissible_inv_iff_nonzero {n : ℕ} (f : Formula n) :
    Admissible f.inv ↔ Nonzero f

    Some matrix evaluation of the inverse is defined exactly when the formula is nonzero.

    source
    theorem Cslib.Circuits.Rational.Admissible.exists_dimension_le {n : ℕ} {f : Formula n} (hf : Admissible f) :
    ∃ (d : ℕ), 0 < d ∧ d ≤ 256 * (n + f.nodeCount + 3) ^ 10 ∧ ∃ (X : Tuple n d) (v : Mat d), Evaluates f X v

    Every nonempty matrix domain has a witness of polynomially bounded dimension.

    source
    def Cslib.Circuits.Rational.Formula.admissible? {n : ℕ} (f : Formula n) :
    Bool

    Test whether the formula has a defined positive-dimensional rational matrix evaluation, by exact evaluation on the hitting list for f.nodeCount + 2 nodes: the two extra nodes cover f + 1, which is nonzero wherever f is defined and zero.

    Instances For
      source
      def Cslib.Circuits.Rational.Formula.nonzero? {n : ℕ} (f : Formula n) :
      Bool

      Test whether the formula has a defined nonzero rational matrix evaluation, by searching the hitting list for f.nodeCount + 2 nodes for an invertible value. A list for f.nodeCount nodes would suffice for this test; the same list as for Formula.admissible? is used.

      Instances For
        source
        theorem Cslib.Circuits.Rational.Formula.admissible?_eq_true_iff {n : ℕ} (f : Formula n) :
        f.admissible? = true ↔ Admissible f

        The generated finite domain test is correct, with no promise on the formula. It uses that the list hits formulas with f.nodeCount + 2 nodes.

        source
        theorem Cslib.Circuits.Rational.Formula.nonzero?_eq_true_iff {n : ℕ} (f : Formula n) :
        f.nonzero? = true ↔ Nonzero f

        The generated finite nonzeroness test is correct, with no admissibility promise. It uses only that the list hits formulas with f.nodeCount nodes.

        source
        @[instance_reducible]
        instance Cslib.Circuits.Rational.decidableAdmissible {n : ℕ} (f : Formula n) :
        Decidable (Admissible f)

        Computed decidability of the existence of a defined matrix evaluation.

        source
        @[instance_reducible]
        instance Cslib.Circuits.Rational.decidableNonzero {n : ℕ} (f : Formula n) :
        Decidable (Nonzero f)

        Computed decidability of the existence of a defined nonzero matrix evaluation.