Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.TapeDivideFive

Unrestricted depth-three lower bound: tape divide five #

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

Control states of the divide five routine.

Instances For
    source
    @[instance_reducible]
    instance Complexity.DepthThreeLowerBound.TapeDivideFive.instDecidableEqState :
    DecidableEq State
    Equations
    source
    def Complexity.DepthThreeLowerBound.TapeDivideFive.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.TapeDivideFive.instFintypeState :
      Fintype State
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.DepthThreeLowerBound.TapeDivideFive.nextPhase (phase : Fin 5) :
      Fin 5

      Advance the remainder counter modulo five.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.TapeDivideFive.residue (n : ℕ) :
        Fin 5

        The remainder modulo five, viewed as an element of Fin 5.

        Equations
        Instances For
          source
          def Complexity.DepthThreeLowerBound.TapeDivideFive.program (counter destination : TapeRegister) :
          TapeMultiProgram State

          Transition function of the divide five routine.

          Equations
          Instances For
            source
            theorem Complexity.DepthThreeLowerBound.TapeDivideFive.runs_phase {counter destination : TapeRegister} (hne : counter ≠ destination) (T : TapeTapes) (n m : ℕ) (phase : Fin 5) :
            RunsIn (program counter destination).step (TapeMultiProgram.cfg (State.dec phase TapeUnary.DecState.start) (TapeCopy.onPair counter destination T (TapeUnary.counterTape n) (TapeUnary.counterTape m))) (TapeMultiProgram.cfg (State.done (residue (↑phase + n))) (TapeCopy.onPair counter destination T (TapeUnary.counterTape 0) (TapeUnary.counterTape (m + (↑phase + n) / 5)))) (8 * n + 3)
            source
            theorem Complexity.DepthThreeLowerBound.TapeDivideFive.runs_divide {counter destination : TapeRegister} (hne : counter ≠ destination) (T : TapeTapes) (n m : ℕ) :
            RunsIn (program counter destination).step (TapeMultiProgram.cfg (State.dec 0 TapeUnary.DecState.start) (TapeCopy.onPair counter destination T (TapeUnary.counterTape n) (TapeUnary.counterTape m))) (TapeMultiProgram.cfg (State.done (residue n)) (TapeCopy.onPair counter destination T (TapeUnary.counterTape 0) (TapeUnary.counterTape (m + n / 5)))) (8 * n + 3)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.TapeDivideFive.done_halts (counter destination : TapeRegister) (r : Fin 5) (h : TapeHeads) :
            program counter destination (State.done r) h = none