Documentation

Complexitylib.RationalHitting.PolynomialTime.Internal

Canonical polynomial time for the rational hitting-list generator #

The source machine is bundled with its binary alphabet codec, guarded by the five-state unary validator, and translated through the reusable TM0 bridge.

source
def Complexity.RationalHitting.Internal.InputShape :
InputState → List Bool → Prop

The shape of every prefix that has not reached the dead state.

Equations
Instances For
    source
    theorem Complexity.RationalHitting.Internal.inputShape_step (q : InputState) (b : Bool) (w : List Bool) (h : InputShape q w) :
    InputShape (inputDFA.step q b) (w ++ [b])

    Each validator step preserves its prefix interpretation.

    source
    theorem Complexity.RationalHitting.Internal.inputShape (w : List Bool) :
    InputShape (inputDFA.eval w) w

    The validator state records the shape of the complete input.

    source
    theorem Complexity.RationalHitting.Internal.input_shape {w : List Bool} (hw : w ∈ inputDFA.accepts) :
    ∃ (n : ℕ) (s : ℕ), w = binaryInput (n + 1) (s + 1)

    Every accepted word has exactly the required two positive unary blocks.

    source
    theorem Complexity.RationalHitting.Internal.eval_replicate (q : InputState) (hq : inputDFA.step q true = q) (n : ℕ) :
    inputDFA.evalFrom q (List.replicate n true) = q

    True bits stay within the corresponding unary block.

    source
    theorem Complexity.RationalHitting.Internal.binaryInput_mem (n s : ℕ) :
    binaryInput (n + 1) (s + 1) ∈ inputDFA.accepts

    Both positive unary parameters pass the validator.

    source
    theorem Complexity.RationalHitting.Internal.inputVariables_binaryInput (n s : ℕ) :
    inputVariables (binaryInput n s) = n

    Reading the first block recovers its unary parameter.

    source
    theorem Complexity.RationalHitting.Internal.inputSize_binaryInput (n s : ℕ) :
    inputSize (binaryInput n s) = s

    Reading the second block recovers its unary parameter.

    source
    theorem Complexity.RationalHitting.Internal.binaryInput_length (n s : ℕ) :
    (binaryInput n s).length = n + s + 1

    Literal unary input length is the sum of its parameters and one separator.

    source
    theorem Complexity.RationalHitting.Internal.map_binaryInput (n s : ℕ) :
    List.map tapeBit (binaryInput n s) = unaryInput n s

    The binary input maps to the source's literal unary tape word.

    source
    @[reducible, inline]
    abbrev Complexity.RationalHitting.Internal.binaryMachine {m : ℕ} (G : Machine m) :
    MathlibTM0.BinaryMachine

    Bundle a source machine with its faithful binary alphabet codec.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.RationalHitting.Internal.binaryMachine_run {m : ℕ} (G : Machine m) (t : ℕ) (c : Config m) :
      (binaryMachine G).run t c = run G t c

      Bundling changes neither source configurations nor finite runs.

      source
      theorem Complexity.RationalHitting.Internal.binaryMachine_outputs {m n s time : ℕ} {G : Machine m} {H : Output n} (h : OutputsWithin G s time H) :
      (binaryMachine G).OutputsWithin (binaryInput n s) (encodeOutput H) time

      The source's complete-output theorem is exactly the bundled contract.

      source
      theorem Complexity.RationalHitting.Internal.hittingGenerator_binaryInput (n s : ℕ) :
      hittingGenerator (binaryInput (n + 1) (s + 1)) = encodeOutput (hittingList (n + 1) (s + 1))

      Literal positive unary inputs yield the source's exact encoded hitting list.

      source
      theorem Complexity.RationalHitting.Internal.hittingGenerator_mem_FP :
      hittingGenerator ∈ FP

      The total source-compatible generator belongs to canonical polynomial time.