Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.LanguageInputBlockLists

Unrestricted depth-three lower bound: language input block lists #

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

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

source
inductive Complexity.DepthThreeLowerBound.InputBlockKind :
Type

Kinds of parameter and data blocks in the encoded input.

Instances For
    source
    @[instance_reducible]
    instance Complexity.DepthThreeLowerBound.instDecidableEqInputBlockKind :
    DecidableEq InputBlockKind
    Equations
    source
    @[instance_reducible]
    instance Complexity.DepthThreeLowerBound.instFintypeInputBlockKind :
    Fintype InputBlockKind
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Complexity.DepthThreeLowerBound.inputBlockOffset (n : ℕ) :
    InputBlockKind → ℕ

    The starting position of the selected input block.

    Equations
    Instances For
      source
      def Complexity.DepthThreeLowerBound.inputBlockLength (n : ℕ) :
      InputBlockKind → ℕ

      The length of the selected input block.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.inputBlockData (w : List Bool) (kind : InputBlockKind) :
        List Bool

        Extract the selected block from the input word.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Complexity.DepthThreeLowerBound.inputBlock_end_le {w : List Bool} (h : InputFits w) (kind : InputBlockKind) :
          inputBlockOffset w.length kind + inputBlockLength w.length kind ≤ w.length
          source
          theorem Complexity.DepthThreeLowerBound.inputBlock_offset_le {w : List Bool} (h : InputFits w) (kind : InputBlockKind) :
          inputBlockOffset w.length kind ≤ w.length
          source
          theorem Complexity.DepthThreeLowerBound.inputBlock_prefix_length {w : List Bool} (h : InputFits w) (kind : InputBlockKind) :
          (List.take (inputBlockOffset w.length kind) w).length = inputBlockOffset w.length kind
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_length {w : List Bool} (h : InputFits w) (kind : InputBlockKind) :
          (inputBlockData w kind).length = inputBlockLength w.length kind
          source
          theorem Complexity.DepthThreeLowerBound.inputBlock_reconstruct (w : List Bool) (kind : InputBlockKind) :
          w = List.take (inputBlockOffset w.length kind) w ++ inputBlockData w kind ++ List.drop (inputBlockOffset w.length kind + inputBlockLength w.length kind) w
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_getD (w : List Bool) (kind : InputBlockKind) {i : ℕ} (hi : i < inputBlockLength w.length kind) :
          (inputBlockData w kind).getD i false = w.getD (inputBlockOffset w.length kind + i) false
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_data_nat (w : List Bool) {i : ℕ} (hi : i < dataDimension w.length) :
          (inputBlockData w InputBlockKind.data).getD i false = (decodeInput w).data ⟨i, hi⟩
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_data (w : List Bool) (i : Fin (dataDimension w.length)) :
          (inputBlockData w InputBlockKind.data).getD (↑i) false = (decodeInput w).data i
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_hash_nat (w : List Bool) {i : ℕ} (hi : i < hashBlockLength (dataDimension w.length)) :
          (inputBlockData w InputBlockKind.hash).getD i false = (decodeInput w).hashSeed ⟨i, hi⟩
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_hash (w : List Bool) (i : Fin (hashBlockLength (dataDimension w.length))) :
          (inputBlockData w InputBlockKind.hash).getD (↑i) false = (decodeInput w).hashSeed i
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_polynomial_nat (w : List Bool) {i : ℕ} (hi : i < hashDimension (dataDimension w.length)) :
          (inputBlockData w InputBlockKind.polynomial).getD i false = (decodeInput w).polynomial ⟨i, hi⟩
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_polynomial (w : List Bool) (i : Fin (hashDimension (dataDimension w.length))) :
          (inputBlockData w InputBlockKind.polynomial).getD (↑i) false = (decodeInput w).polynomial i
          source
          theorem Complexity.DepthThreeLowerBound.inputBlock_coefficient_index_lt {n j i : ℕ} (hj : j < independenceOrder (dataDimension n)) (hi : i < hashDimension (dataDimension n)) :
          j * hashDimension (dataDimension n) + i < inputBlockLength n InputBlockKind.coefficients
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_coefficients_nat (w : List Bool) {j i : ℕ} (hj : j < independenceOrder (dataDimension w.length)) (hi : i < hashDimension (dataDimension w.length)) :
          (inputBlockData w InputBlockKind.coefficients).getD (j * hashDimension (dataDimension w.length) + i) false = (decodeInput w).coefficients ⟨j, hj⟩ ⟨i, hi⟩
          source
          theorem Complexity.DepthThreeLowerBound.inputBlockData_coefficients (w : List Bool) (j : Fin (independenceOrder (dataDimension w.length))) (i : Fin (hashDimension (dataDimension w.length))) :
          (inputBlockData w InputBlockKind.coefficients).getD (↑j * hashDimension (dataDimension w.length) + ↑i) false = (decodeInput w).coefficients j i