Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeHashRow

Unrestricted depth-three lower bound: tape hash row #

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

Control states for the run stage of the hash row routine.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.TapeHashRow.ClearState :
    Type

    Control states for the clear stage of the hash row routine.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Complexity.DepthThreeLowerBound.TapeHashRow.State :
      Type

      Control states of the hash row routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeHashRow.runProgram :
        TapeMultiProgram RunState

        Transition function for the run stage of the hash row routine.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeHashRow.clearProgram :
          TapeMultiProgram ClearState

          Transition function for the clear stage of the hash row routine.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeHashRow.program :
            TapeMultiProgram State

            Transition function of the hash row routine.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeHashRow.start :
              State

              Initial control state of the hash row routine.

              Equations
              Instances For
                source
                def Complexity.DepthThreeLowerBound.TapeHashRow.done :
                State

                Terminal control state of the hash row routine.

                Equations
                Instances For
                  source
                  def Complexity.DepthThreeLowerBound.TapeHashRow.resultStore (σ : TapeStore) (i d : ℕ) :
                  TapeStore

                  Tape-store contents at the result stage of the hash row routine.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Complexity.DepthThreeLowerBound.TapeHashRow.runs_row (σ : TapeStore) (i d r : ℕ) (hi : i < r) (hd : σ TapeRegister.dataLength = List.replicate d true) (ha : σ TapeRegister.indexA = []) (hb : σ TapeRegister.indexB = []) (hc : σ TapeRegister.indexC = List.replicate i true) (hkey : (σ TapeRegister.keyBits).length = d + r - 1) (hdata : (σ TapeRegister.dataBits).length = d) (hout : (σ TapeRegister.hashBits).length = r) :
                    RunsIn program.step (TapeMultiProgram.cfg start (storeTapes σ)) (TapeMultiProgram.cfg done (storeTapes (resultStore σ i d))) (d * (4 * i + 8 * d + 29) + 4 * i + 8 * d + 25)
                    source
                    @[simp]
                    theorem Complexity.DepthThreeLowerBound.TapeHashRow.program_done (h : TapeHeads) :
                    program done h = none