Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.AlgebraLanguage

Unrestricted depth-three lower bound: algebra language #

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

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

source
@[reducible, inline]
abbrev Complexity.DepthThreeLowerBound.ParsedInput.QuotientRing (q : ParsedInput) :
Type

The polynomial quotient ring determined by the parsed modulus.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance Complexity.DepthThreeLowerBound.ParsedInput.quotientRingFintype (q : ParsedInput) :
    Fintype q.QuotientRing
    Equations
    source
    noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.quotientHash (q : ParsedInput) :
    q.QuotientRing

    The hashed input polynomial viewed in the quotient ring.

    Equations
    Instances For
      source
      noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.quotientCoefficient (q : ParsedInput) (j : Fin q.coefficientCount) :
      q.QuotientRing

      A parsed coefficient polynomial viewed in the quotient ring.

      Equations
      Instances For
        source
        noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.quotientEvaluation (q : ParsedInput) :
        q.QuotientRing

        Evaluate the coefficient polynomial at the hashed input in the quotient ring.

        Equations
        Instances For
          source
          theorem Complexity.DepthThreeLowerBound.ParsedInput.quotientHash_eq_encode (q : ParsedInput) :
          q.quotientHash = BinaryAlgebra.encode (fun (i : Fin q.ringDegree) => BinaryAlgebra.bitValue (q.polynomial i)) fun (i : Fin q.ringDegree) => BinaryAlgebra.bitValue (BinaryHash.hashBool q.hashSeed q.data i)
          source
          theorem Complexity.DepthThreeLowerBound.ParsedInput.quotientCoefficient_eq_encode (q : ParsedInput) (j : Fin q.coefficientCount) :
          q.quotientCoefficient j = BinaryAlgebra.encode (fun (i : Fin q.ringDegree) => BinaryAlgebra.bitValue (q.polynomial i)) fun (i : Fin q.ringDegree) => BinaryAlgebra.bitValue (q.coefficients j i)
          source
          noncomputable def Complexity.DepthThreeLowerBound.ParsedInput.coefficientBitsEquiv (q : ParsedInput) :
          (Fin q.ringDegree → Bool) ≃ q.QuotientRing

          Identify coefficient bit blocks with tuples of quotient-ring elements.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.ParsedInput.coefficientBitsEquiv_apply (q : ParsedInput) (v : Fin q.ringDegree → Bool) :
            q.coefficientBitsEquiv v = BinaryAlgebra.encode (fun (i : Fin q.ringDegree) => BinaryAlgebra.bitValue (q.polynomial i)) fun (i : Fin q.ringDegree) => BinaryAlgebra.bitValue (v i)
            source
            theorem Complexity.DepthThreeLowerBound.ParsedInput.coefficientBitsEquiv_coefficient (q : ParsedInput) (j : Fin q.coefficientCount) :
            q.coefficientBitsEquiv (q.coefficients j) = q.quotientCoefficient j
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.ParsedInput.quotientRing_card (q : ParsedInput) :
            Fintype.card q.QuotientRing = 2 ^ q.ringDegree
            source
            theorem Complexity.DepthThreeLowerBound.ParsedInput.quotientEvaluation_eq_mk (q : ParsedInput) :
            q.quotientEvaluation = (AdjoinRoot.mk q.modulus) q.evaluationPolynomial
            source
            theorem Complexity.DepthThreeLowerBound.ParsedInput.representative_quotientEvaluation (q : ParsedInput) :
            (BinaryAlgebra.quotientRepresentative ⋯) q.quotientEvaluation = q.evaluationRemainder
            source
            theorem Complexity.DepthThreeLowerBound.ParsedInput.degreeZero_quotientEvaluation (q : ParsedInput) :
            (BinaryAlgebra.degreeZero ⋯) q.quotientEvaluation = q.evaluationRemainder.coeff 0
            source
            theorem Complexity.DepthThreeLowerBound.ParsedInput.quotient_degreeZero_one (q : ParsedInput) (hr : 0 < q.ringDegree) :
            (BinaryAlgebra.degreeZero ⋯) 1 = 1
            source
            theorem Complexity.DepthThreeLowerBound.ParsedInput.evaluate_eq_true_iff_degreeZero (q : ParsedInput) :
            q.evaluate = true ↔ (BinaryAlgebra.degreeZero ⋯) q.quotientEvaluation = 0
            source
            theorem Complexity.DepthThreeLowerBound.language_eq_true_iff_quotient (w : List Bool) :
            language w = true ↔ InputFits w ∧ (BinaryAlgebra.degreeZero ⋯) (decodeInput w).quotientEvaluation = 0