Documentation

Complexitylib.RationalHitting

Rational hitting lists, nonzeroness, and admissibility #

OpenAI's source constructs one uniform polynomial-time generator of rational matrix hitting lists for noncommutative rational formulas: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Main.lean

The source runtime counts ordinary transitions of a fixed finite-state Mathlib TM0 machine. Its inputs are two unary parameters separated by a nonblank symbol, and its output is the complete canonical binary encoding of the list. Complexitylib.RationalHitting.PolynomialTime transfers this generator to canonical FP, returning empty output on malformed binary inputs.

The additional executable tests decide nonzeroness and admissibility using exact rational matrix evaluation. The latter needs a list for two extra syntax nodes: if f has a defined value, either f or f + 1 has a nonzero value. Their correctness theorems do not assert polynomial bit complexity of evaluation. These are deductions from the source result, without a claim of new priority.

source
def Complexity.RationalHitting.hittingList (n s : ℕ) :
Output n

The explicit, executable list of rational matrix substitutions.

Equations
Instances For
    source
    theorem Complexity.RationalHitting.hittingList_hits (n s : ℕ) (hs : 1 ≤ s) :
    Hits s (hittingList n s)

    The generated list hits every nonzero formula of bounded size with an invertible value.

    source
    theorem Complexity.RationalHitting.hittingList_dimension_le (n s : ℕ) :
    (hittingList n s).dimension ≤ 256 * (n + s + 1) ^ 10

    The generated matrices have polynomially bounded dimension.

    source
    theorem Complexity.RationalHitting.hittingList_encoding_length_le (n s : ℕ) (hn : 1 ≤ n) :
    (encodeOutput (hittingList n s)).length ≤ PolynomialBounds.outputConstant * (n + s + 1) ^ 104

    The complete reduced-rational binary encoding has polynomial length.

    source
    theorem Complexity.RationalHitting.exists_uniform_generator :
    ∃ (m : ℕ) (G : Machine m) (C : ℕ) (k : ℕ), 0 < C ∧ 0 < k ∧ ∀ (n s : ℕ), 1 ≤ n → 1 ≤ s → OutputsWithin G s (C * (n + s + 1) ^ k) (hittingList n s)

    A fixed finite-state Mathlib machine generates these exact lists in polynomial bit time.

    source
    theorem Complexity.RationalHitting.exists_polynomial_hitting_generator :
    MainStatement

    OpenAI's combined dimension, encoding-length, hitting, and finite-machine runtime theorem.

    source
    theorem Complexity.RationalHitting.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 Complexity.RationalHitting.Admissible.exists_dimension_le {n : ℕ} {f : Formula n} (hf : Admissible f) :
    ∃ (d : ℕ), 0 < d ∧ d ≤ 256 * (n + f.size + 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 Complexity.RationalHitting.Formula.admissible? {n : ℕ} (f : Formula n) :
    Bool

    Test whether the formula has a defined positive-dimensional rational matrix evaluation.

    Equations
    Instances For
      source
      def Complexity.RationalHitting.Formula.nonzero? {n : ℕ} (f : Formula n) :
      Bool

      Test whether the formula has a defined nonzero rational matrix evaluation.

      Equations
      Instances For
        source
        theorem Complexity.RationalHitting.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.

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

        source
        @[instance_reducible]
        instance Complexity.RationalHitting.decidableAdmissible {n : ℕ} (f : Formula n) :
        Decidable (Admissible f)

        Computed decidability of the existence of a defined matrix evaluation.

        Equations
        source
        @[instance_reducible]
        instance Complexity.RationalHitting.decidableNonzero {n : ℕ} (f : Formula n) :
        Decidable (Nonzero f)

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

        Equations