Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.LanguageBitArithmetic

Unrestricted depth-three lower bound: language bit arithmetic #

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

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

source
def Complexity.DepthThreeLowerBound.wordFreeze {n : ℕ} (a : BitWord n) :
BitWord n

Freeze a bit-word representation for the arithmetic evaluator.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.wordFreeze_eq {n : ℕ} (a : BitWord n) :
    wordFreeze a = a
    source
    def Complexity.DepthThreeLowerBound.cancelStep {r m : ℕ} (p : BitWord r) (k : ℕ) (a : BitWord m) :
    BitWord m

    Cancel one high coefficient using the shifted modulus.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.DepthThreeLowerBound.cancelStep_above {r m : ℕ} (p : BitWord r) (k : ℕ) (a : BitWord m) (i : Fin m) (hi : k < ↑i) :
      cancelStep p k a i = a i
      source
      theorem Complexity.DepthThreeLowerBound.cancelStep_at {r m : ℕ} (p : BitWord r) (a : BitWord m) (i : Fin m) (hi : r ≤ ↑i) :
      cancelStep p (↑i) a i = false
      source
      theorem Complexity.DepthThreeLowerBound.wordPoly_cancelStep_mod {r m : ℕ} (p : BitWord r) (k : ℕ) (a : BitWord m) :
      wordPoly (cancelStep p k a) %ₘ BinaryAlgebra.inputPolynomialBits p = wordPoly a %ₘ BinaryAlgebra.inputPolynomialBits p
      source
      def Complexity.DepthThreeLowerBound.reduceLoop {r m : ℕ} (p : BitWord r) :
      ℕ → BitWord m → BitWord m

      Iterate high-coefficient cancellation to compute a remainder.

      Equations
      Instances For
        source
        theorem Complexity.DepthThreeLowerBound.wordPoly_reduceLoop_mod {r m : ℕ} (p : BitWord r) (k : ℕ) (a : BitWord m) :
        wordPoly (reduceLoop p k a) %ₘ BinaryAlgebra.inputPolynomialBits p = wordPoly a %ₘ BinaryAlgebra.inputPolynomialBits p
        source
        theorem Complexity.DepthThreeLowerBound.reduceLoop_tail_false {r m : ℕ} (p : BitWord r) (k : ℕ) (a : BitWord m) (ha : ∀ (i : Fin m), r ≤ ↑i → k ≤ ↑i → a i = false) (i : Fin m) :
        r ≤ ↑i → reduceLoop p k a i = false
        source
        def Complexity.DepthThreeLowerBound.wordResize {m : ℕ} (r : ℕ) (a : BitWord m) :
        BitWord r

        Resize a bit word, truncating or padding with false bits.

        Equations
        Instances For
          source
          theorem Complexity.DepthThreeLowerBound.wordPoly_resize_of_tail_false {r m : ℕ} (a : BitWord m) (ha : ∀ (i : Fin m), r ≤ ↑i → a i = false) :
          wordPoly (wordResize r a) = wordPoly a
          source
          def Complexity.DepthThreeLowerBound.wordReduce {r m : ℕ} (p : BitWord r) (a : BitWord m) :
          BitWord r

          Reduce a bit-word polynomial modulo the monic modulus.

          Equations
          Instances For
            source
            theorem Complexity.DepthThreeLowerBound.wordPoly_reduce {r m : ℕ} (p : BitWord r) (a : BitWord m) :
            wordPoly (wordReduce p a) = wordPoly a %ₘ BinaryAlgebra.inputPolynomialBits p
            source
            def Complexity.DepthThreeLowerBound.wordMulMod {r : ℕ} (p a b : BitWord r) :
            BitWord r

            Multiply bit-word polynomials and reduce modulo the modulus.

            Equations
            Instances For
              source
              theorem Complexity.DepthThreeLowerBound.wordPoly_mulMod {r : ℕ} (p a b : BitWord r) :
              wordPoly (wordMulMod p a b) = wordPoly a * wordPoly b %ₘ BinaryAlgebra.inputPolynomialBits p