Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.AlgebraQuotient

Unrestricted depth-three lower bound: algebra quotient #

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

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

source
noncomputable def Complexity.DepthThreeLowerBound.BinaryAlgebra.quotientRepresentative {P : Polynomial F2} (hP : P.Monic) :
AdjoinRoot P →ₗ[F2] Polynomial F2

The canonical polynomial representative of a quotient-ring element.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.quotientRepresentative_mk {P : Polynomial F2} (hP : P.Monic) (f : Polynomial F2) :
    (quotientRepresentative hP) ((AdjoinRoot.mk P) f) = f %ₘ P
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.mk_quotientRepresentative {P : Polynomial F2} (hP : P.Monic) (z : AdjoinRoot P) :
    (AdjoinRoot.mk P) ((quotientRepresentative hP) z) = z
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degree_quotientRepresentative_lt {P : Polynomial F2} (hP : P.Monic) (z : AdjoinRoot P) :
    ((quotientRepresentative hP) z).degree < P.degree
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.quotientRepresentative_one {P : Polynomial F2} (hP : P.Monic) (hdeg : 0 < P.natDegree) :
    (quotientRepresentative hP) 1 = 1
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.BinaryAlgebra.InputQuotient {r : ℕ} (p : Fin r → F2) :
    Type

    The quotient by the monic polynomial specified by the input coefficients.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Complexity.DepthThreeLowerBound.BinaryAlgebra.BitQuotient {r : ℕ} (p : Fin r → Bool) :
      Type

      The input quotient ring with coefficients specified by bits.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.pack_mod_inputPolynomial {r : ℕ} (p a : Fin r → F2) :
        pack a %ₘ inputPolynomial p = pack a
        source
        noncomputable def Complexity.DepthThreeLowerBound.BinaryAlgebra.encode {r : ℕ} (p a : Fin r → F2) :
        InputQuotient p

        Map coefficient bits into the polynomial quotient ring.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates {r : ℕ} (p : Fin r → F2) :
          InputQuotient p ≃ₗ[F2] Fin r → F2

          Read the coefficients of the canonical quotient representative.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates_apply {r : ℕ} (p : Fin r → F2) (z : InputQuotient p) (i : Fin r) :
            (coordinates p) z i = ((quotientRepresentative ⋯) z).coeff ↑i
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates_symm_apply {r : ℕ} (p a : Fin r → F2) :
            (coordinates p).symm a = encode p a
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates_encode {r : ℕ} (p a : Fin r → F2) :
            (coordinates p) (encode p a) = a
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.encode_coordinates {r : ℕ} (p : Fin r → F2) (z : InputQuotient p) :
            encode p ((coordinates p) z) = z
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.encode_injective {r : ℕ} (p : Fin r → F2) :
            Function.Injective (encode p)
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.encode_surjective {r : ℕ} (p : Fin r → F2) :
            Function.Surjective (encode p)
            source
            @[instance_reducible]
            noncomputable instance Complexity.DepthThreeLowerBound.BinaryAlgebra.inputQuotientFintype {r : ℕ} (p : Fin r → F2) :
            Fintype (InputQuotient p)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputQuotient_card {r : ℕ} (p : Fin r → F2) :
            Fintype.card (InputQuotient p) = 2 ^ r
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitQuotient_card {r : ℕ} (p : Fin r → Bool) :
            Fintype.card (BitQuotient p) = 2 ^ r
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates_mk {r : ℕ} (p : Fin r → F2) (f : Polynomial F2) (i : Fin r) :
            (coordinates p) ((AdjoinRoot.mk (inputPolynomial p)) f) i = (f %ₘ inputPolynomial p).coeff ↑i
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.encode_zero {r : ℕ} (p : Fin r → F2) :
            encode p 0 = 0
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.encode_add {r : ℕ} (p a b : Fin r → F2) :
            encode p (a + b) = encode p a + encode p b
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.encode_smul {r : ℕ} (p : Fin r → F2) (c : F2) (a : Fin r → F2) :
            encode p (c • a) = c • encode p a
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates_encode_mul {r : ℕ} (p a b : Fin r → F2) (i : Fin r) :
            (coordinates p) (encode p a * encode p b) i = (pack a * pack b %ₘ inputPolynomial p).coeff ↑i
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.encode_mul {r : ℕ} (p a b : Fin r → F2) :
            (encode p fun (i : Fin r) => (pack a * pack b %ₘ inputPolynomial p).coeff ↑i) = encode p a * encode p b
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates_mul {r : ℕ} (p : Fin r → F2) (x y : InputQuotient p) (i : Fin r) :
            (coordinates p) (x * y) i = (pack ((coordinates p) x) * pack ((coordinates p) y) %ₘ inputPolynomial p).coeff ↑i
            source
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.coordinates_one {r : ℕ} (p : Fin r → F2) (hr : 0 < r) (i : Fin r) :
            (coordinates p) 1 i = if ↑i = 0 then 1 else 0
            source
            noncomputable def Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero {P : Polynomial F2} (hP : P.Monic) :
            AdjoinRoot P →ₗ[F2] F2

            Read the constant coefficient of the quotient representative.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero_apply {P : Polynomial F2} (hP : P.Monic) (z : AdjoinRoot P) :
              (degreeZero hP) z = ((quotientRepresentative hP) z).coeff 0
              source
              theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero_mk {P : Polynomial F2} (hP : P.Monic) (f : Polynomial F2) :
              (degreeZero hP) ((AdjoinRoot.mk P) f) = (f %ₘ P).coeff 0
              source
              theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero_one {P : Polynomial F2} (hP : P.Monic) (hdeg : 0 < P.natDegree) :
              (degreeZero hP) 1 = 1
              source
              theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero_surjective {P : Polynomial F2} (hP : P.Monic) (hdeg : 0 < P.natDegree) :
              Function.Surjective ⇑(degreeZero hP)
              source
              theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero_encode {r : ℕ} (p : Fin r → F2) (hr : 0 < r) (a : Fin r → F2) :
              (degreeZero ⋯) (encode p a) = a ⟨0, hr⟩
              source
              theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero_coordinates {r : ℕ} (p : Fin r → F2) (hr : 0 < r) (z : InputQuotient p) :
              (degreeZero ⋯) z = (coordinates p) z ⟨0, hr⟩
              source
              theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.degreeZero_sum_encode_pow {r t : ℕ} (p a : Fin r → F2) (beta : Fin t → Fin r → F2) :
              (degreeZero ⋯) (∑ j : Fin t, encode p (beta j) * encode p a ^ ↑j) = ((∑ j : Fin t, pack (beta j) * pack a ^ ↑j) %ₘ inputPolynomial p).coeff 0