Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.HashBool

Unrestricted depth-three lower bound: hash bool #

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

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

source
theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_eq_iff {d r : ℕ} (u : Fin (d + r - 1) → Bool) (x : Fin d → Bool) (a : Fin r → Bool) :
hashBool u x = a ↔ hashF2 ((BinaryAlgebra.bitsEquivF2 (Fin (d + r - 1))) u) ((BinaryAlgebra.bitsEquivF2 (Fin d)) x) = (BinaryAlgebra.bitsEquivF2 (Fin r)) a
source
theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_collision_iff {d r : ℕ} (u : Fin (d + r - 1) → Bool) (x y : Fin d → Bool) :
hashBool u x = hashBool u y ↔ hashF2 ((BinaryAlgebra.bitsEquivF2 (Fin (d + r - 1))) u) ((BinaryAlgebra.bitsEquivF2 (Fin d)) x) = hashF2 ((BinaryAlgebra.bitsEquivF2 (Fin (d + r - 1))) u) ((BinaryAlgebra.bitsEquivF2 (Fin d)) y)
source
def Complexity.DepthThreeLowerBound.BinaryHash.hashBoolFiberEquiv {d r : ℕ} (x : Fin d → Bool) (a : Fin r → Bool) :
{ u : Fin (d + r - 1) → Bool // hashBool u x = a } ≃ { u : Seed d r // hashF2 u ((BinaryAlgebra.bitsEquivF2 (Fin d)) x) = (BinaryAlgebra.bitsEquivF2 (Fin r)) a }

Transfer hash fibers between Boolean and field-vector presentations.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_fiber_card {d r : ℕ} (x : Fin d → Bool) (hx : x ≠ fun (x : Fin d) => false) (a : Fin r → Bool) :
    Fintype.card { u : Fin (d + r - 1) → Bool // hashBool u x = a } = 2 ^ (d - 1)
    source
    def Complexity.DepthThreeLowerBound.BinaryHash.hashBoolCollisionEquiv {d r : ℕ} (x y : Fin d → Bool) :
    { u : Fin (d + r - 1) → Bool // hashBool u x = hashBool u y } ≃ { u : Seed d r // hashF2 u ((BinaryAlgebra.bitsEquivF2 (Fin d)) x) = hashF2 u ((BinaryAlgebra.bitsEquivF2 (Fin d)) y) }

    Transfer hash collisions between Boolean and field-vector presentations.

    Equations
    Instances For
      source
      theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_collision_card {d r : ℕ} (x y : Fin d → Bool) (hxy : x ≠ y) :
      Fintype.card { u : Fin (d + r - 1) → Bool // hashBool u x = hashBool u y } = 2 ^ (d - 1)
      source
      def Complexity.DepthThreeLowerBound.BinaryHash.boolCoordinateCube {d : ℕ} (T : Finset (Fin d)) (rho : { i : Fin d // i ∉ T } → Bool) :
      Set (Fin d → Bool)

      Boolean assignments on a selected coordinate set.

      Equations
      Instances For
        source
        theorem Complexity.DepthThreeLowerBound.BinaryHash.mem_boolCoordinateCube_iff {d : ℕ} (T : Finset (Fin d)) (rho : { i : Fin d // i ∉ T } → Bool) (x : Fin d → Bool) :
        x ∈ boolCoordinateCube T rho ↔ (BinaryAlgebra.bitsEquivF2 (Fin d)) x ∈ coordinateCube T fun (i : { i : Fin d // i ∉ T }) => BinaryAlgebra.bitValue (rho i)
        source
        theorem Complexity.DepthThreeLowerBound.BinaryHash.injOn_hashBool_iff {d r : ℕ} (u : Fin (d + r - 1) → Bool) (T : Finset (Fin d)) (rho : { i : Fin d // i ∉ T } → Bool) :
        Set.InjOn (hashBool u) (boolCoordinateCube T rho) ↔ Set.InjOn (hashF2 ((BinaryAlgebra.bitsEquivF2 (Fin (d + r - 1))) u)) (coordinateCube T fun (i : { i : Fin d // i ∉ T }) => BinaryAlgebra.bitValue (rho i))
        source
        def Complexity.DepthThreeLowerBound.BinaryHash.hashBoolBadSeedEquiv {d r : ℕ} (T : Finset (Fin d)) (rho : { i : Fin d // i ∉ T } → Bool) :
        { u : Fin (d + r - 1) → Bool // ¬Set.InjOn (hashBool u) (boolCoordinateCube T rho) } ≃ { u : Seed d r // ¬Set.InjOn (hashF2 u) (coordinateCube T fun (i : { i : Fin d // i ∉ T }) => BinaryAlgebra.bitValue (rho i)) }

        Transfer bad-seed sets from Boolean to field-vector notation.

        Equations
        Instances For
          source
          theorem Complexity.DepthThreeLowerBound.BinaryHash.hashBool_badSeed_card_le {d r : ℕ} (T : Finset (Fin d)) (rho : { i : Fin d // i ∉ T } → Bool) :
          Fintype.card { u : Fin (d + r - 1) → Bool // ¬Set.InjOn (hashBool u) (boolCoordinateCube T rho) } ≤ (2 ^ T.card - 1) * 2 ^ (d - 1)