Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeCancelRow

Unrestricted depth-three lower bound: tape cancel row #

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

Control states of the cancel row routine.

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

    Transition function of the cancel row routine.

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

      Initial control state of the cancel row routine.

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

        Terminal control state of the cancel row routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeCancelRow.frame (σ : TapeStore) (n j shift : ℕ) (out : List Bool) :
          TapeStore

          Tape-store invariant recording the loop counters and current output.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.frame_counter (σ : TapeStore) (n j s : ℕ) (out : List Bool) :
            frame σ n j s out TapeRegister.loop1 = List.replicate n true
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.frame_indexA (σ : TapeStore) (n j s : ℕ) (out : List Bool) :
            frame σ n j s out TapeRegister.indexA = List.replicate j true
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.frame_indexC (σ : TapeStore) (n j s : ℕ) (out : List Bool) :
            frame σ n j s out TapeRegister.indexC = List.replicate (s + j) true
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.frame_output (σ : TapeStore) (n j s : ℕ) (out : List Bool) :
            frame σ n j s out TapeRegister.productBits = out
            source
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.update_counter (σ : TapeStore) (n n' j s : ℕ) (out : List Bool) :
            Function.update (frame σ n j s out) TapeRegister.loop1 (List.replicate n' true) = frame σ n' j s out
            source
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.resultStore_frame (σ : TapeStore) (n j s : ℕ) (out out' : List Bool) :
            TapeCancelStep.resultStore (frame σ n j s out) j (s + j) out' = frame σ n (j + 1) s out'
            source
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.runs_row (v : Bool) (σ : TapeStore) (p c : List Bool) (s j n : ℕ) (hP : σ TapeRegister.polyBits = p) (hj : j + n ≤ p.length) (hsize : s + p.length ≤ c.length) :
            RunsIn (program v).step (TapeMultiProgram.cfg start (storeTapes (frame σ n j s (modulusUpdateLoop p v s j c)))) (TapeMultiProgram.cfg done (storeTapes (frame σ 0 (j + n) s (modulusUpdateLoop p v s (j + n) c)))) (n * (2 * s + 4 * p.length + 21) + 3)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeCancelRow.program_done (v : Bool) (h : TapeHeads) :
            program v done h = none