Documentation

Complexitylib.RationalHitting.Internal.CyclotomicGrid

Rational hitting lists: cyclotomic grid #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/CyclotomicGrid.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

source
noncomputable def Complexity.RationalHitting.CyclotomicRing.modulus (e : ℕ) :
Polynomial ℚ

The cyclotomic modulus for roots of unity of power-of-two order.

Equations
Instances For
    source
    def Complexity.RationalHitting.CyclotomicRing.degree (e : ℕ) :
    ℕ

    Degree of the chosen cyclotomic modulus.

    Equations
    Instances For
      source
      def Complexity.RationalHitting.CyclotomicRing.dimension (e : ℕ) :
      ℕ

      Order of the chosen root of unity.

      Equations
      Instances For
        source
        theorem Complexity.RationalHitting.CyclotomicRing.modulus_eq_cyclotomic (e : ℕ) :
        modulus e = Polynomial.cyclotomic (dimension e) ℚ
        source
        instance Complexity.RationalHitting.CyclotomicRing.modulus_irreducible (e : ℕ) :
        Fact (Irreducible (modulus e))
        source
        @[reducible, inline]
        abbrev Complexity.RationalHitting.CyclotomicRing.R (e : ℕ) :
        Type

        The rational cyclotomic quotient used for the matrix construction.

        Equations
        Instances For
          source
          theorem Complexity.RationalHitting.CyclotomicRing.degree_pos (e : ℕ) :
          0 < degree e
          source
          theorem Complexity.RationalHitting.CyclotomicRing.dimension_pos (e : ℕ) :
          0 < dimension e
          source
          theorem Complexity.RationalHitting.CyclotomicRing.modulus_monic (e : ℕ) :
          (modulus e).Monic
          source
          theorem Complexity.RationalHitting.CyclotomicRing.modulus_natDegree (e : ℕ) :
          (modulus e).natDegree = degree e
          source
          noncomputable def Complexity.RationalHitting.CyclotomicRing.powerBasis (e : ℕ) :
          PowerBasis ℚ (R e)

          The quotient's power basis generated by the adjoined root.

          Equations
          Instances For
            source
            noncomputable def Complexity.RationalHitting.CyclotomicRing.basis (e : ℕ) :
            Module.Basis (Fin (degree e)) ℚ (R e)

            Reindex the power basis by the explicit cyclotomic degree.

            Equations
            Instances For
              source
              theorem Complexity.RationalHitting.CyclotomicRing.basis_apply (e : ℕ) (i : Fin (degree e)) :
              (basis e) i = AdjoinRoot.root (modulus e) ^ ↑i
              source
              instance Complexity.RationalHitting.CyclotomicRing.dimension_neZero (e : ℕ) :
              NeZero (dimension e)
              source
              instance Complexity.RationalHitting.CyclotomicRing.charZero (e : ℕ) :
              CharZero (R e)
              source
              instance Complexity.RationalHitting.CyclotomicRing.finite (e : ℕ) :
              Module.Finite ℚ (R e)
              source
              noncomputable def Complexity.RationalHitting.CyclotomicRing.intoComplex (e : ℕ) :
              R e →ₐ[ℚ] ℂ

              An embedding of the cyclotomic quotient into the complex numbers.

              Equations
              Instances For
                source
                theorem Complexity.RationalHitting.CyclotomicRing.root_primitive (e : ℕ) :
                IsPrimitiveRoot (AdjoinRoot.root (modulus e)) (dimension e)

                The cyclotomic quotient is a field for the chosen powers of two. Irreducibility allows regular-representation invertibility to be proved at a single primitive root.

                source
                noncomputable def Complexity.RationalHitting.CyclotomicRing.character (e : ℕ) :
                AddChar (ZMod (dimension e)) (R e)

                The additive character generated by the primitive cyclotomic root.

                Equations
                Instances For
                  source
                  theorem Complexity.RationalHitting.CyclotomicRing.character_primitive (e : ℕ) :
                  (character e).IsPrimitive
                  source
                  noncomputable def Complexity.RationalHitting.CyclotomicRing.rho (e : ℕ) :
                  R e →ₐ[ℚ] Matrix (Fin (degree e)) (Fin (degree e)) ℚ

                  The regular rational matrix representation of the cyclotomic field.

                  Equations
                  Instances For
                    source
                    theorem Complexity.RationalHitting.CyclotomicRing.rho_root_apply (e : ℕ) (i j : Fin (degree e)) :
                    (rho e) (AdjoinRoot.root (modulus e)) i j = ((basis e).repr (AdjoinRoot.root (modulus e) ^ (↑j + 1))) i
                    source
                    theorem Complexity.RationalHitting.FiniteGrid.exists_eval_ne_zero {K : Type u_1} [Field K] {k : ℕ} (p : MvPolynomial (Fin k) K) (hp : p ≠ 0) (S : Finset K) (hS : p.totalDegree < S.card) :
                    ∃ (x : Fin k → K), (∀ (i : Fin k), x i ∈ S) ∧ (MvPolynomial.eval x) p ≠ 0

                    The fixed grid, independent of the coefficients, finds a nonzero value.

                    source
                    theorem Complexity.RationalHitting.FiniteGrid.det_totalDegree_le {K : Type u_1} [Field K] {k : ℕ} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι (MvPolynomial (Fin k) K)) (d : ℕ) (hA : ∀ (i j : ι), (A i j).totalDegree ≤ d) :
                    A.det.totalDegree ≤ Fintype.card ι * d
                    source
                    theorem Complexity.RationalHitting.FiniteGrid.simultaneous {K : Type u_1} [Field K] {k : ℕ} (P : List (MvPolynomial (Fin k) K)) (hP : ∀ p ∈ P, p ≠ 0) (d : ℕ) (hd : ∀ p ∈ P, p.totalDegree ≤ d) (S : Finset K) (hS : P.length * d < S.card) :
                    ∃ (x : Fin k → K), (∀ (i : Fin k), x i ∈ S) ∧ ∀ p ∈ P, (MvPolynomial.eval x) p ≠ 0

                    The common grid specializes a list of determinant conditions simultaneously, rather than one formula gate at a time.