Documentation

Complexitylib.Circuits.Unrolling.Transition.Fragment.Internal.Size

Size bounds for packed one-step transition fragments #

This internal module bounds every formula in a bounded transition layer by a machine-dependent linear function of the trace horizon. Since a configuration block itself has linear width, the packed one-step fragment has quadratic size.

source
def Complexity.CircuitUnrolling.caseSizeCoeff (k : ℕ) :
ℕ

Linear coefficient bounding the size of one transition-case formula.

Equations
Instances For
    source
    noncomputable def Complexity.CircuitUnrolling.effectSizeCoeff {k : ℕ} (tm : NTM k) :
    ℕ

    Linear coefficient bounding a transition-effect selector.

    Equations
    Instances For
      source
      noncomputable def Complexity.CircuitUnrolling.nextSizeCoeff {k : ℕ} (tm : NTM k) :
      ℕ

      Linear coefficient bounding a next-configuration formula.

      Equations
      Instances For
        source
        def Complexity.CircuitUnrolling.widthSizeCoeff {k : ℕ} (tm : NTM k) :
        ℕ

        Linear coefficient bounding the width of a configuration fragment.

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.CircuitUnrolling.size_configVar_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (atom : ConfigAtom tm T) :
          (configVar tm T base atom).size = 1

          Internal exact size of a configuration-variable formula.

          source
          @[simp]
          theorem Complexity.CircuitUnrolling.size_haltVar_internal {k : ℕ} (tm : NTM k) (T base : ℕ) :
          (haltVar tm T base).size = 1

          Internal exact size of the halted-state variable.

          source
          theorem Complexity.CircuitUnrolling.size_readFormula_succ_le_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (symbol : Γ) :
          (readFormula tm T base tape symbol).size + 1 ≤ 4 * (T + 2)

          A read formula plus its enclosing list connective costs at most four nodes per represented head position.

          source
          theorem Complexity.CircuitUnrolling.size_caseFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (view : TransitionCase tm) :
          (caseFormula tm T base choiceWire view).size ≤ caseSizeCoeff k * (T + 2)

          Internal linear size bound for a complete local transition case.

          source
          theorem Complexity.CircuitUnrolling.size_effectFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (selects : TransitionEffect tm → Bool) :
          (effectFormula tm T base choiceWire selects).size ≤ effectSizeCoeff tm * (T + 2)

          Internal linear size bound for a finite transition-effect selector.

          source
          theorem Complexity.CircuitUnrolling.size_selectedStateFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (state : tm.Q) :
          (selectedStateFormula tm T base choiceWire state).size ≤ effectSizeCoeff tm * (T + 2)

          Internal size bound for successor-state selection.

          source
          theorem Complexity.CircuitUnrolling.size_selectedMoveFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : TapeSlot k) (direction : Dir3) :
          (selectedMoveFormula tm T base choiceWire tape direction).size ≤ effectSizeCoeff tm * (T + 2)

          Internal size bound for head-movement selection.

          source
          theorem Complexity.CircuitUnrolling.size_selectedWriteFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : WritableSlot k) (symbol : Γ) :
          (selectedWriteFormula tm T base choiceWire tape symbol).size ≤ effectSizeCoeff tm * (T + 2)

          Internal size bound for write-symbol selection.

          source
          theorem Complexity.CircuitUnrolling.size_predecessorHeadFormula_le_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) (direction : Dir3) :
          (predecessorHeadFormula tm T base tape target direction).size ≤ 2 * (T + 2)

          Internal linear size bound for predecessor-head selection.

          source
          theorem Complexity.CircuitUnrolling.size_movedHeadFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) :
          (movedHeadFormula tm T base choiceWire tape target).size ≤ (3 * effectSizeCoeff tm + 13) * (T + 2)

          Internal linear size bound for a moved-head atom.

          source
          @[simp]
          theorem Complexity.CircuitUnrolling.size_headAtCellFormula_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (position : Fin (T + 2)) :
          (headAtCellFormula tm T base tape position).size = 1

          Internal exact size of the old-head-at-cell formula.

          source
          @[simp]
          theorem Complexity.CircuitUnrolling.size_haltedOrFormula_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (oldValue nextValue : BoolFormula) :
          (haltedOrFormula tm T base oldValue nextValue).size = oldValue.size + nextValue.size + 6

          Internal exact overhead of halted-or-successor multiplexing.

          source
          theorem Complexity.CircuitUnrolling.size_writtenCellFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : WritableSlot k) (position : Fin (T + 2)) (symbol : Γ) :
          (writtenCellFormula tm T base choiceWire tape position symbol).size ≤ effectSizeCoeff tm * (T + 2) + 7

          Internal linear size bound for a positive writable-cell formula.

          source
          theorem Complexity.CircuitUnrolling.size_nextFormula_le_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (atom : ConfigAtom tm T) :
          (nextFormula tm T base choiceWire atom).size ≤ nextSizeCoeff tm * (T + 2)

          Every successor-configuration atom has size linear in the horizon.

          source
          theorem Complexity.CircuitUnrolling.configWidth_le_linear_internal {k : ℕ} (tm : NTM k) (T : ℕ) :
          configWidth tm T ≤ widthSizeCoeff tm * (T + 2)

          The bounded configuration width is linear in the horizon.

          source
          theorem Complexity.CircuitUnrolling.configWidth_le_explicit_internal {k : ℕ} (tm : NTM k) (T : ℕ) :
          configWidth tm T ≤ (Fintype.card tm.Q + 5 * (k + 2)) * (T + 2)

          Internal explicit form of the linear configuration-width bound.

          source
          theorem Complexity.CircuitUnrolling.stepFragmentSize_le_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) :
          stepFragmentSize tm T configBase choiceWire ≤ stepSizeCoeff tm * (T + 2) ^ 2

          The exact packed one-step gate count is quadratic in the trace horizon.