Documentation

Complexitylib.RationalHitting.Internal.SignedBinary

Rational hitting lists: signed binary #

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

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

source
def Complexity.RationalHitting.StackLanguage.replaceRecord :
Program (Fin 8)

Replace the front variable-width record, consuming the replacement in 5.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.RationalHitting.StackLanguage.eval_replaceRecord (old new tail : List Bool) (s : Store (Fin 8)) (h0 : s 0 = codeWord old ++ tail) (h2 : s 2 = []) (h3 : s 3 = []) (h5 : s 5 = new) :
    Eval replaceRecord s (Function.update (Function.update s 0 (codeWord new ++ tail)) 5 []) (7 * old.length + 6 * new.length + 16)
    source
    def Complexity.RationalHitting.StackLanguage.arrayWrite :
    Program (Fin 8)

    Indexed overwrite with no fixed cell width or numerical oracle.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.RationalHitting.StackLanguage.eval_arrayWrite (pre post : List (List Bool)) (old new : List Bool) (s : Store (Fin 8)) (h0 : s 0 = codeArray (pre ++ old :: post)) (h1 : s 1 = []) (h2 : s 2 = []) (h3 : s 3 = []) (h4 : s 4 = List.replicate pre.length true) (h5 : s 5 = new) :
      ∃ t ≤ 40 * (s 0).length + 6 * new.length + 30, Eval arrayWrite s (Function.update (Function.update (Function.update s 0 (codeArray (pre ++ new :: post))) 4 []) 5 []) t
      source
      def Complexity.RationalHitting.StackLanguage.powerBody :
      Program (Fin 10)

      Repeated multiplication, preserving the binary base in register 8 and consuming a unary exponent in register 9. Used in the Taylor input matrices.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.RationalHitting.StackLanguage.powerLoop :
        Program (Fin 10)

        Repeat multiplication over a unary exponent counter.

        Equations
        Instances For
          source
          theorem Complexity.RationalHitting.StackLanguage.eval_powerBody (s : Store (Fin 10)) (hf : FactorialScratch s) (B : ℕ) (h0 : (s 0).length ≤ B) (h8 : (s 8).length ≤ B) :
          ∃ t ≤ 250 * (B + 1) ^ 4, Eval powerBody s (Function.update (Function.update s 0 (wordValue (s 0) * wordValue (s 8)).bits) 9 (s 9).tail) t
          source
          theorem Complexity.RationalHitting.StackLanguage.eval_powerLoop (n B : ℕ) (s : Store (Fin 10)) (hf : FactorialScratch s) (hcan : (wordValue (s 0)).bits = s 0) (hn : (s 9).length = n) (hp : (s 0).length + n * (s 8).length ≤ B) (hb : (s 8).length ≤ B) :
          ∃ t ≤ n * (250 * (B + 1) ^ 4 + 1) + 1, Eval powerLoop s (Function.update (Function.update s 0 (wordValue (s 0) * wordValue (s 8) ^ n).bits) 9 []) t
          source
          def Complexity.RationalHitting.StackLanguage.powerCore :
          Program (Fin 10)

          Initialize the multiplicative identity and execute exponentiation.

          Equations
          Instances For
            source
            theorem Complexity.RationalHitting.StackLanguage.eval_powerCore (s : Store (Fin 10)) (hf : FactorialScratch s) (h0 : s 0 = []) (n : ℕ) (hn : (s 9).length = n) :
            ∃ t ≤ n * (250 * (2 + (n + 1) * (s 8).length) ^ 4 + 1) + 3, Eval powerCore s (Function.update (Function.update s 0 (wordValue (s 8) ^ n).bits) 9 []) t

            A fixed finite power subroutine. Its exponent is unary and its output is canonical binary. No exponentiation instruction is supplied by the machine.

            source
            theorem Complexity.RationalHitting.StackLanguage.wordValue_complement (w : List Bool) :
            wordValue (List.map not w) + wordValue w + 1 = 2 ^ w.length
            source
            def Complexity.RationalHitting.StackLanguage.flipReverse {K : Type} (a b : K) :
            Program K

            Move a word to another stack while complementing each bit.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Complexity.RationalHitting.StackLanguage.eval_flipReverse {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (s : Store K) :
              Eval (flipReverse a b) s (Function.update (Function.update s a []) b ((List.map not (s a)).reverse ++ s b)) (5 * (s a).length + 1)
              source
              def Complexity.RationalHitting.StackLanguage.flipWord {K : Type} (a b : K) :
              Program K

              Complement every bit and restore the original word order.

              Equations
              Instances For
                source
                theorem Complexity.RationalHitting.StackLanguage.eval_flipWord {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (s : Store K) (hb : s b = []) :
                Eval (flipWord a b) s (Function.update s a (List.map not (s a))) (7 * (s a).length + 3)
                source
                def Complexity.RationalHitting.StackLanguage.absoluteWord (a b : List Bool) :
                List Bool

                Compute the absolute difference of two binary word values.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Complexity.RationalHitting.StackLanguage.absoluteWord_length (a b : List Bool) :
                  (absoluteWord a b).length ≤ max a.length b.length + 1
                  source
                  theorem Complexity.RationalHitting.StackLanguage.absoluteWord_value (a b : List Bool) :
                  wordValue (absoluteWord a b) = (↑(wordValue a) - ↑(wordValue b)).natAbs
                  source
                  def Complexity.RationalHitting.StackLanguage.absolutize :
                  Program (Fin 5)

                  Convert the modular subtraction result to an absolute magnitude according to its genuinely computed borrow bit.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Complexity.RationalHitting.StackLanguage.eval_absolutize (s : Store (Fin 5)) (c : Bool) (h3 : s 3 = [c]) (h1 : s 1 = []) (h2 : s 2 = []) :
                    ∃ t ≤ 30 * (s 0).length + 52, Eval absolutize s (Function.update s 0 (wordValue (if c = true then incrementWord (List.map not (s 0)) else s 0)).bits) t
                    source
                    def Complexity.RationalHitting.StackLanguage.signedDifference :
                    Program (Fin 5)

                    Signed difference of arbitrary naturals, in canonical signed magnitude.

                    Equations
                    Instances For
                      source
                      theorem Complexity.RationalHitting.StackLanguage.eval_signedDifference (s : Store (Fin 5)) (h2 : s 2 = []) (h3 : s 3 = []) (h4 : s 4 = []) :
                      ∃ t ≤ 100 * ((s 0).length + (s 1).length + 1), Eval signedDifference s (Function.update (Function.update (Function.update s 0 (↑(wordValue (s 0)) - ↑(wordValue (s 1))).natAbs.bits) 1 []) 3 [decide (wordValue (s 0) < wordValue (s 1))]) t