Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeRemainderOuter

Unrestricted depth-three lower bound: tape remainder outer #

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

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

source
def Complexity.DepthThreeLowerBound.TapeRemainderOuter.ScratchEmpty (σ : TapeStore) :
Prop

All scratch counters used by remainder cancellation are empty.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.DepthThreeLowerBound.TapeRemainderOuter.BodyState :
    Type

    Control states for the body stage of the remainder outer routine.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DepthThreeLowerBound.TapeRemainderOuter.tailProgram :
      TapeMultiProgram (TapeCancel.State ⊕ TapeRemainderSetup.CleanupState)

      Transition function for the tail stage of the remainder outer routine.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeRemainderOuter.bodyProgram :
        TapeMultiProgram BodyState

        Transition function for the body stage of the remainder outer routine.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeRemainderOuter.bodyStart :
          BodyState

          Initial control state of the body stage of the remainder outer routine.

          Equations
          Instances For
            source
            def Complexity.DepthThreeLowerBound.TapeRemainderOuter.bodyDone :
            BodyState

            Terminal control state of the body stage of the remainder outer routine.

            Equations
            Instances For
              source
              def Complexity.DepthThreeLowerBound.TapeRemainderOuter.bodyCost (s r : ℕ) :
              ℕ

              Transition budget for the remainder outer routine at its body stage.

              Equations
              Instances For
                source
                @[simp]
                theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.bodyProgram_done (h : TapeHeads) :
                bodyProgram bodyDone h = none
                source
                theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.cleanup_result (σ : TapeStore) (r s : ℕ) (out : List Bool) (hclean : ScratchEmpty σ) :
                TapeRemainderSetup.clearIndices (TapeCancel.resultStore (TapeRemainderSetup.preparedStore σ r s) r s out) = Function.update σ TapeRegister.productBits out
                source
                theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.runs_body (σ : TapeStore) (p c : List Bool) (s : ℕ) (hP : σ TapeRegister.polyBits = p) (hOut : σ TapeRegister.productBits = c) (hDegree : σ TapeRegister.ringDegree = List.replicate p.length true) (hLoop0 : σ TapeRegister.loop0 = List.replicate s true) (hclean : ScratchEmpty σ) (hbound : s + p.length < c.length) :
                RunsIn bodyProgram.step (TapeMultiProgram.cfg bodyStart (storeTapes σ)) (TapeMultiProgram.cfg bodyDone (storeTapes (Function.update σ TapeRegister.productBits (cancelByUpdates p c s)))) (bodyCost s p.length)
                source
                def Complexity.DepthThreeLowerBound.TapeRemainderOuter.iterationCost (r : ℕ) :
                ℕ

                Transition budget for the remainder outer routine at its iteration stage.

                Equations
                Instances For
                  source
                  theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.bodyCost_le (s r : ℕ) (hs : s ≤ r) :
                  4 + 1 + bodyCost s r + 1 ≤ iterationCost r
                  source
                  @[reducible, inline]
                  abbrev Complexity.DepthThreeLowerBound.TapeRemainderOuter.State :
                  Type

                  Control states of the remainder outer routine.

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

                    Transition function of the remainder outer routine.

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

                      Initial control state of the remainder outer routine.

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

                        Terminal control state of the remainder outer routine.

                        Equations
                        Instances For
                          source
                          def Complexity.DepthThreeLowerBound.TapeRemainderOuter.frame (σ : TapeStore) (k : ℕ) (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.TapeRemainderOuter.frame_counter (σ : TapeStore) (k : ℕ) (out : List Bool) :
                            frame σ k out TapeRegister.loop0 = List.replicate k true
                            source
                            @[simp]
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.frame_output (σ : TapeStore) (k : ℕ) (out : List Bool) :
                            frame σ k out TapeRegister.productBits = out
                            source
                            @[simp]
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.frame_poly (σ : TapeStore) (k : ℕ) (out : List Bool) :
                            frame σ k out TapeRegister.polyBits = σ TapeRegister.polyBits
                            source
                            @[simp]
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.frame_degree (σ : TapeStore) (k : ℕ) (out : List Bool) :
                            frame σ k out TapeRegister.ringDegree = σ TapeRegister.ringDegree
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.frame_clean (σ : TapeStore) (k : ℕ) (out : List Bool) (h : ScratchEmpty σ) :
                            ScratchEmpty (frame σ k out)
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.update_counter (σ : TapeStore) (k k' : ℕ) (out : List Bool) :
                            Function.update (frame σ k out) TapeRegister.loop0 (List.replicate k' true) = frame σ k' out
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.update_output (σ : TapeStore) (k : ℕ) (out out' : List Bool) :
                            Function.update (frame σ k out) TapeRegister.productBits out' = frame σ k out'
                            source
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.runs_loop (σ : TapeStore) (p c : List Bool) (k : ℕ) (hP : σ TapeRegister.polyBits = p) (hDegree : σ TapeRegister.ringDegree = List.replicate p.length true) (hclean : ScratchEmpty σ) (hk : k ≤ p.length) (hsize : k + p.length ≤ c.length) :
                            RunsIn program.step (TapeMultiProgram.cfg start (storeTapes (frame σ k c))) (TapeMultiProgram.cfg done (storeTapes (frame σ 0 (reduceByUpdates p k c)))) (k * iterationCost p.length + 3)
                            source
                            @[simp]
                            theorem Complexity.DepthThreeLowerBound.TapeRemainderOuter.program_done (h : TapeHeads) :
                            program done h = none