Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.HashTriangular

Unrestricted depth-three lower bound: hash triangular #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/HashTriangular.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.exists_last_nonzero {d : ℕ} (w : Data d) (hw : w ≠ 0) :
∃ (s : Fin d), w s ≠ 0 ∧ ∀ (a : Fin d), ↑s < ↑a → w a = 0
source
noncomputable def Complexity.DepthThreeLowerBound.BinaryHash.lastIndex {d : ℕ} (w : Data d) (hw : w ≠ 0) :
Fin d

The last nonzero coordinate used as a pivot in the hash argument.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.BinaryHash.lastIndex_nonzero {d : ℕ} (w : Data d) (hw : w ≠ 0) :
    w (lastIndex w hw) ≠ 0
    source
    theorem Complexity.DepthThreeLowerBound.BinaryHash.zero_after_lastIndex {d : ℕ} (w : Data d) (hw : w ≠ 0) (a : Fin d) (ha : ↑(lastIndex w hw) < ↑a) :
    w a = 0
    source
    theorem Complexity.DepthThreeLowerBound.BinaryHash.data_dim_pos {d : ℕ} (w : Data d) (hw : w ≠ 0) :
    0 < d
    source
    def Complexity.DepthThreeLowerBound.BinaryHash.Nonpivot {d r : ℕ} (w : Data d) (hw : w ≠ 0) :
    Type

    Seed positions other than the chosen pivot positions.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      noncomputable instance Complexity.DepthThreeLowerBound.BinaryHash.instFintypeNonpivot {d r : ℕ} (w : Data d) (hw : w ≠ 0) :
      Fintype (Nonpivot w hw)
      Equations
      source
      theorem Complexity.DepthThreeLowerBound.BinaryHash.card_nonpivot {d r : ℕ} (w : Data d) (hw : w ≠ 0) :
      Fintype.card (Nonpivot w hw) = d - 1
      source
      def Complexity.DepthThreeLowerBound.BinaryHash.triangularMap {d r : ℕ} (w : Data d) (hw : w ≠ 0) (u : Seed d r) :
      Output r × (Nonpivot w hw → F2)

      The triangular coordinate map used to solve the hash equations.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.DepthThreeLowerBound.BinaryHash.triangularMap_injective {d r : ℕ} (w : Data d) (hw : w ≠ 0) :
        Function.Injective (triangularMap w hw)
        source
        theorem Complexity.DepthThreeLowerBound.BinaryHash.triangularMap_bijective {d r : ℕ} (w : Data d) (hw : w ≠ 0) :
        Function.Bijective (triangularMap w hw)
        source
        noncomputable def Complexity.DepthThreeLowerBound.BinaryHash.triangularEquiv {d r : ℕ} (w : Data d) (hw : w ≠ 0) :
        Seed d r ≃ Output r × (Nonpivot w hw → F2)

        Invert the triangular map by solving for the pivot coordinates.

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryHash.triangularEquiv_fst {d r : ℕ} (w : Data d) (hw : w ≠ 0) (u : Seed d r) :
          ((triangularEquiv w hw) u).1 = hashF2 u w
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryHash.triangularEquiv_snd {d r : ℕ} (w : Data d) (hw : w ≠ 0) (u : Seed d r) (j : Nonpivot w hw) :
          ((triangularEquiv w hw) u).2 j = u ↑j