Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeUnaryCompare

Unrestricted depth-three lower bound: tape unary compare #

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

Control states of the unary compare routine.

Instances For
    source
    @[instance_reducible]
    instance Complexity.DepthThreeLowerBound.TapeUnaryCompare.instDecidableEqState :
    DecidableEq State
    Equations
    source
    def Complexity.DepthThreeLowerBound.TapeUnaryCompare.instDecidableEqState.decEq (x✝ x✝¹ : State) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Complexity.DepthThreeLowerBound.TapeUnaryCompare.instFintypeState :
      Fintype State
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance Complexity.DepthThreeLowerBound.TapeUnaryCompare.instInhabitedState :
      Inhabited State
      Equations
      source
      def Complexity.DepthThreeLowerBound.TapeUnaryCompare.scanState :
      TapeUnaryCompareScan.State → State

      Control states for the scan stage of the unary compare routine.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeUnaryCompare.rewindRState (o : Ordering) :
        TapeRewind.State → State

        Control states for the rewind r stage of the unary compare routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeUnaryCompare.rewindSState (o : Ordering) :
          TapeRewind.State → State

          Control states for the rewind s stage of the unary compare routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeUnaryCompare.mapInstruction {Q : Type uDepth1} {R : Type uDepth2} (f : Q → R) (instruction : Option (Q × TapeHeads × TapeMoves)) :
            Option (R × TapeHeads × TapeMoves)

            Map only the target control state of an optional transition instruction.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeUnaryCompare.program (r s : TapeRegister) :
              TapeMultiProgram State

              Transition function of the unary compare routine.

              Equations
              Instances For
                source
                theorem Complexity.DepthThreeLowerBound.TapeUnaryCompare.scan_code (r s : TapeRegister) (q : TapeUnaryCompareScan.State) (h : TapeHeads) (q' : TapeUnaryCompareScan.State) (writes : TapeHeads) (moves : TapeMoves) (hc : TapeUnaryCompareScan.code r s q h = some (q', writes, moves)) :
                program r s (scanState q) h = some (scanState q', writes, moves)
                source
                theorem Complexity.DepthThreeLowerBound.TapeUnaryCompare.rewindR_code (r s : TapeRegister) (o : Ordering) (q : TapeRewind.State) (h : TapeHeads) (q' : TapeRewind.State) (writes : TapeHeads) (moves : TapeMoves) (hc : TapeRewind.program r q h = some (q', writes, moves)) :
                program r s (rewindRState o q) h = some (rewindRState o q', writes, moves)
                source
                theorem Complexity.DepthThreeLowerBound.TapeUnaryCompare.rewindS_code (r s : TapeRegister) (o : Ordering) (q : TapeRewind.State) (h : TapeHeads) (q' : TapeRewind.State) (writes : TapeHeads) (moves : TapeMoves) (hc : TapeRewind.program s q h = some (q', writes, moves)) :
                program r s (rewindSState o q) h = some (rewindSState o q', writes, moves)
                source
                theorem Complexity.DepthThreeLowerBound.TapeUnaryCompare.runs_rewindR (r s : TapeRegister) (o : Ordering) (T : TapeTapes) (before after : List Bool) :
                RunsIn (program r s).step (TapeMultiProgram.cfg (State.rewindR o) (Function.update T r (cursorTape before after))) (TapeMultiProgram.cfg (State.rewindS o) (Function.update T r (wordTape (before ++ after)))) (before.length + 2)
                source
                theorem Complexity.DepthThreeLowerBound.TapeUnaryCompare.runs_rewindS (r s : TapeRegister) (o : Ordering) (T : TapeTapes) (before after : List Bool) :
                RunsIn (program r s).step (TapeMultiProgram.cfg (State.rewindS o) (Function.update T s (cursorTape before after))) (TapeMultiProgram.cfg (State.done o) (Function.update T s (wordTape (before ++ after)))) (before.length + 2)
                source
                theorem Complexity.DepthThreeLowerBound.TapeUnaryCompare.runs_compare {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (m n : ℕ) (hR : T r = wordTape (List.replicate m true)) (hS : T s = wordTape (List.replicate n true)) :
                RunsIn (program r s).step (TapeMultiProgram.cfg (State.scan TapeUnaryCompareScan.State.beginR) T) (TapeMultiProgram.cfg (State.done (TapeUnaryCompareScan.result m n)) T) (4 * min m n + 7)
                source
                theorem Complexity.DepthThreeLowerBound.TapeUnaryCompare.runs_compare_linear {r s : TapeRegister} (hrs : r ≠ s) (T : TapeTapes) (m n : ℕ) (hR : T r = wordTape (List.replicate m true)) (hS : T s = wordTape (List.replicate n true)) :
                RunsIn (program r s).step (TapeMultiProgram.cfg (State.scan TapeUnaryCompareScan.State.beginR) T) (TapeMultiProgram.cfg (State.done (TapeUnaryCompareScan.result m n)) T) (7 * (m + n + 1))