Documentation

Complexitylib.RationalHitting.Internal.BinaryGcd

Rational hitting lists: binary gcd #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/BinaryGcd.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.subEmbed :
Fin 5 ↪ Fin 10

Embed the subtraction registers in the division register bank.

Equations
Instances For
    source
    def Complexity.RationalHitting.StackLanguage.subtract10 :
    Program (Fin 10)

    The subtraction program renamed into ten registers.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.RationalHitting.StackLanguage.eval_subtract10 (s : Store (Fin 10)) :
      ∃ t ≤ 17 * ((s 0).length + (s 1).length) + 2 * (s 2).length + 2 * (s 3).length + 2 * (s 4).length + 19, Eval subtract10 s (Function.update (Function.update (Function.update (Function.update (Function.update s 0 (subtractWord (s 0) (s 1) false).1) 1 []) 2 []) 3 [(subtractWord (s 0) (s 1) false).2]) 4 []) t
      source
      def Complexity.RationalHitting.StackLanguage.reducePick :
      Program (Fin 10)

      Select the successful subtraction result or restore the original value.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.RationalHitting.StackLanguage.eval_reducePick (s : Store (Fin 10)) (c : Bool) (hc : s 3 = [c]) (h9 : s 9 = []) :
        ∃ t ≤ 7 * (s 8).length + 2 * (s 0).length + 10, Eval reducePick s (Function.update (Function.update s 0 (if c = true then s 8 else s 0)) 7 ((!c) :: s 7)) t
        source
        def Complexity.RationalHitting.StackLanguage.reduceOnce :
        Program (Fin 10)

        One attempted subtraction, followed by normalization and scratch cleanup.

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

          The scratch-register emptiness invariant for division.

          Equations
          Instances For
            source
            theorem Complexity.RationalHitting.StackLanguage.eval_reduceOnce (s : Store (Fin 10)) (hs : DivScratch s) :
            ∃ t ≤ 100 * ((s 0).length + (s 5).length + 1), Eval reduceOnce s (Function.update (Function.update s 0 (reduceWord (s 0) (s 5)).1) 7 ((reduceWord (s 0) (s 5)).2 :: s 7)) t
            source
            @[simp]
            theorem Complexity.RationalHitting.StackLanguage.wordValue_bits (n : ℕ) :
            wordValue n.bits = n
            source
            def Complexity.RationalHitting.StackLanguage.divBody :
            Program (Fin 10)

            Remainder 0, denominator 5, unread MSD numerator 6, quotient 7.

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

              Repeat binary division steps over the input bits.

              Equations
              Instances For
                source
                theorem Complexity.RationalHitting.StackLanguage.eval_divBody (s : Store (Fin 10)) (hs : DivScratch s) (x : Bool) (l : List Bool) (h6 : s 6 = x :: l) :
                ∃ t ≤ 110 * ((s 0).length + (s 5).length + 2), Eval divBody s (Function.update (Function.update (Function.update s 6 l) 0 (reduceWord (x :: s 0) (s 5)).1) 7 ((reduceWord (x :: s 0) (s 5)).2 :: s 7)) t
                source
                theorem Complexity.RationalHitting.StackLanguage.eval_divLoop (s : Store (Fin 10)) (hs : DivScratch s) (hb : 0 < wordValue (s 5)) (hr : wordValue (s 0) < wordValue (s 5)) (B : ℕ) (hB : (s 0).length ≤ B) (hbB : (s 5).length ≤ B) :
                ∃ t ≤ (s 6).length * (250 * (B + 1)) + 1, Eval divLoop s (Function.update (Function.update (Function.update s 6 []) 0 (divideDigits (s 5) (s 6) (s 0) (s 7)).1) 7 (divideDigits (s 5) (s 6) (s 0) (s 7)).2) t
                source
                def Complexity.RationalHitting.StackLanguage.divide :
                Program (Fin 10)

                Binary division starts with numerator in 0 and denominator in 5. The original denominator is retained; quotient is placed in 7, remainder in 0. Every other register is cleared.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Complexity.RationalHitting.StackLanguage.eval_divide (s : Store (Fin 10)) (hs : DivScratch s) (h6 : s 6 = []) (h7 : s 7 = []) (hb : 0 < wordValue (s 5)) :
                  ∃ t ≤ 300 * ((s 0).length + 1) * ((s 5).length + 1) + 30, Eval divide s (Function.update (Function.update s 0 (wordValue (s 0) % wordValue (s 5)).bits) 7 (wordValue (s 0) / wordValue (s 5)).bits) t