Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeArithmetic

Unrestricted depth-three lower bound: tape arithmetic #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/TapeArithmetic.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.TapeArithmetic.update_onPair_src {α : Type uDepth1} (src dst : TapeRegister) (T : TapeRegister → α) (s d s' : α) :
Function.update (TapeCopy.onPair src dst T s d) src s' = TapeCopy.onPair src dst T s' d
source
theorem Complexity.DepthThreeLowerBound.TapeArithmetic.update_onPair_dst {α : Type uDepth2} {src dst : TapeRegister} (hne : src ≠ dst) (T : TapeRegister → α) (s d d' : α) :
Function.update (TapeCopy.onPair src dst T s d) dst d' = TapeCopy.onPair src dst T s d'
source
def Complexity.DepthThreeLowerBound.TapeArithmetic.decPositive :
TapeUnary.DecState → Bool

Read whether the decrement routine removed a positive unit.

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

    Control states for the add stage of the arithmetic routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeArithmetic.addProgram (counter destination : TapeRegister) :
      TapeMultiProgram AddState

      Transition function for the add stage of the arithmetic routine.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeArithmetic.addStart :
        AddState

        Initial control state of the add stage of the arithmetic routine.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeArithmetic.addDone :
          AddState

          Terminal control state of the add stage of the arithmetic routine.

          Equations
          Instances For
            source
            theorem Complexity.DepthThreeLowerBound.TapeArithmetic.runs_add {counter destination : TapeRegister} (hne : counter ≠ destination) (T : TapeTapes) (n m : ℕ) :
            RunsIn (addProgram counter destination).step (TapeMultiProgram.cfg addStart (TapeCopy.onPair counter destination T (TapeUnary.counterTape n) (TapeUnary.counterTape m))) (TapeMultiProgram.cfg addDone (TapeCopy.onPair counter destination T (TapeUnary.counterTape 0) (TapeUnary.counterTape (m + n)))) (8 * n + 3)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeArithmetic.add_done (counter destination : TapeRegister) (h : TapeHeads) :
            addProgram counter destination addDone h = none