Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.HashFibers

Unrestricted depth-three lower bound: hash fibers #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/HashFibers.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.BinaryHash.hashF2FiberEquiv {d r : ℕ} (w : Data d) (hw : w ≠ 0) (a : Output r) :
{ u : Seed d r // hashF2 u w = a } ≃ (Nonpivot w hw → F2)

Identify a nonempty hash fiber with the corresponding kernel fiber.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_fiber_card {d r : ℕ} (w : Data d) (hw : w ≠ 0) (a : Output r) :
    Fintype.card { u : Seed d r // hashF2 u w = a } = 2 ^ (d - 1)
    source
    theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_surjective {d r : ℕ} (w : Data d) (hw : w ≠ 0) :
    Function.Surjective fun (u : Seed d r) => hashF2 u w
    source
    def Complexity.DepthThreeLowerBound.BinaryHash.hashF2CollisionEquiv {d r : ℕ} (x y : Data d) :
    { u : Seed d r // hashF2 u x = hashF2 u y } ≃ { u : Seed d r // hashF2 u (x - y) = 0 }

    Identify hash collisions with kernel solutions by translation.

    Equations
    Instances For
      source
      theorem Complexity.DepthThreeLowerBound.BinaryHash.hashF2_collision_card {d r : ℕ} (x y : Data d) (hxy : x ≠ y) :
      Fintype.card { u : Seed d r // hashF2 u x = hashF2 u y } = 2 ^ (d - 1)