Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.Hash

Unrestricted depth-three lower bound: hash #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/Hash.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.BinaryHash.F2 :
Type

The two-element field.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.BinaryHash.Data (d : ℕ) :
    Type

    Input vectors over the two-element field.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Complexity.DepthThreeLowerBound.BinaryHash.Seed (d r : ℕ) :
      Type

      Seed vectors for the binary linear hash family.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Complexity.DepthThreeLowerBound.BinaryHash.Output (r : ℕ) :
        Type

        Output vectors of the binary linear hash family.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.BinaryHash.sumIndex {d r : ℕ} (i : Fin r) (s : Fin d) :
          Fin (d + r - 1)

          Index a hash-seed coordinate by the sum of input and output positions.

          Equations
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryHash.sumIndex_val {d r : ℕ} (i : Fin r) (s : Fin d) :
            ↑(sumIndex i s) = ↑i + ↑s
            source
            theorem Complexity.DepthThreeLowerBound.BinaryHash.sumIndex_left_injective {d r : ℕ} (s : Fin d) :
            Function.Injective fun (i : Fin r) => sumIndex i s
            source
            def Complexity.DepthThreeLowerBound.BinaryHash.hashF2 {d r : ℕ} (u : Seed d r) (x : Data d) :
            Output r

            The seeded linear hash over the two-element field.

            Equations
            Instances For
              source
              @[simp]
              theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_apply {d r : ℕ} (u : Seed d r) (x : Data d) (i : Fin r) :
              hashF2 u x i = ∑ s : Fin d, u (sumIndex i s) * x s
              source
              @[simp]
              theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_zero_data {d r : ℕ} (u : Seed d r) :
              hashF2 u 0 = 0
              source
              @[simp]
              theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_zero_seed {d r : ℕ} (x : Data d) :
              hashF2 0 x = 0
              source
              theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_add_data {d r : ℕ} (u : Seed d r) (x y : Data d) :
              hashF2 u (x + y) = hashF2 u x + hashF2 u y
              source
              theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_sub_data {d r : ℕ} (u : Seed d r) (x y : Data d) :
              hashF2 u (x - y) = hashF2 u x - hashF2 u y
              source
              theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_add_seed {d r : ℕ} (u v : Seed d r) (x : Data d) :
              hashF2 (u + v) x = hashF2 u x + hashF2 v x
              source
              theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_sub_seed {d r : ℕ} (u v : Seed d r) (x : Data d) :
              hashF2 (u - v) x = hashF2 u x - hashF2 v x
              source
              def Complexity.DepthThreeLowerBound.BinaryHash.hashBool {d r : ℕ} (u : Fin (d + r - 1) → Bool) (x : Fin d → Bool) :
              Fin r → Bool

              The same seeded hash expressed on Boolean bit vectors.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem Complexity.DepthThreeLowerBound.BinaryHash.bitValue_hashBool {d r : ℕ} (u : Fin (d + r - 1) → Bool) (x : Fin d → Bool) (i : Fin r) :
                BinaryAlgebra.bitValue (hashBool u x i) = hashF2 (fun (j : Fin (d + r - 1)) => BinaryAlgebra.bitValue (u j)) (fun (s : Fin d) => BinaryAlgebra.bitValue (x s)) i
                source
                theorem Complexity.DepthThreeLowerBound.BinaryHash.bitsEquivF2_hashBool {d r : ℕ} (u : Fin (d + r - 1) → Bool) (x : Fin d → Bool) :
                (BinaryAlgebra.bitsEquivF2 (Fin r)) (hashBool u x) = hashF2 ((BinaryAlgebra.bitsEquivF2 (Fin (d + r - 1))) u) ((BinaryAlgebra.bitsEquivF2 (Fin d)) x)