Documentation

Complexitylib.RationalHitting.Internal.BinaryFactorial

Rational hitting lists: binary factorial #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/BinaryFactorial.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.gcdBody :
Program (Fin 10)

One Euclidean algorithm step on binary stack words.

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

    Repeat Euclidean reduction until the second operand is zero.

    Equations
    Instances For
      source
      def Complexity.RationalHitting.StackLanguage.GcdScratch (s : Store (Fin 10)) :
      Prop

      The scratch-register emptiness invariant for the Euclidean algorithm.

      Equations
      Instances For
        source
        theorem Complexity.RationalHitting.StackLanguage.eval_gcdBody (s : Store (Fin 10)) (hs : GcdScratch s) (hb : 0 < wordValue (s 5)) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) :
        ∃ t ≤ 500 * (B + 1) ^ 2, Eval gcdBody s (Function.update (Function.update s 0 (s 5)) 5 (wordValue (s 0) % wordValue (s 5)).bits) t
        source
        theorem Complexity.RationalHitting.StackLanguage.gcd_product_halving {a b : ℕ} (ha : 0 < a) (hab : a ≤ b) :
        2 * (a * (b % a)) ≤ a * b

        Euclid's product is halved at every ordered step.

        source
        theorem Complexity.RationalHitting.StackLanguage.eval_gcdLoop_ordered (f : ℕ) (s : Store (Fin 10)) (hs : GcdScratch s) (hcan0 : (wordValue (s 0)).bits = s 0) (hcan5 : (wordValue (s 5)).bits = s 5) (hab : wordValue (s 5) ≤ wordValue (s 0)) (hf : wordValue (s 0) * wordValue (s 5) < 2 ^ f) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) :
        ∃ t ≤ f * (500 * (B + 1) ^ 2 + 1) + 1, Eval gcdLoop s (Function.update (Function.update s 0 ((wordValue (s 0)).gcd (wordValue (s 5))).bits) 5 []) t
        source
        theorem Complexity.RationalHitting.StackLanguage.eval_gcdLoop (s : Store (Fin 10)) (hs : GcdScratch s) (hcan0 : (wordValue (s 0)).bits = s 0) (hcan5 : (wordValue (s 5)).bits = s 5) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) :
        ∃ t ≤ (2 * B + 1) * (500 * (B + 1) ^ 2 + 1) + 1, Eval gcdLoop s (Function.update (Function.update s 0 ((wordValue (s 0)).gcd (wordValue (s 5))).bits) 5 []) t

        No value-sized fuel: the compiler executes an ordinary while loop, and Euclid's product-halving supplies a bound linear in the input bit lengths.

        source
        def Complexity.RationalHitting.StackLanguage.quotient :
        Program (Fin 10)

        Destructive exact binary quotient, retaining its positive denominator.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Complexity.RationalHitting.StackLanguage.eval_quotient (s : Store (Fin 10)) (hs : GcdScratch s) (hb : 0 < wordValue (s 5)) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) :
          ∃ t ≤ 400 * (B + 1) ^ 2, Eval quotient s (Function.update s 0 (wordValue (s 0) / wordValue (s 5)).bits) t
          source
          def Complexity.RationalHitting.StackLanguage.fractionArith :
          Fin 10 ↪ Fin 12

          Extra work registers for retaining numerator and denominator through Euclid.

          Equations
          Instances For
            source
            @[simp]
            theorem Complexity.RationalHitting.StackLanguage.fractionArith_val (i : Fin 10) :
            ↑(fractionArith i) = ↑i
            source
            def Complexity.RationalHitting.StackLanguage.FractionScratch (s : Store (Fin 12)) :
            Prop

            The clean-register invariant for reducing a rational fraction.

            Equations
            Instances For
              source
              theorem Complexity.RationalHitting.StackLanguage.fractionScratch_gcd (s : Store (Fin 12)) (hs : FractionScratch s) :
              GcdScratch fun (k : Fin 10) => s (fractionArith k)
              source
              theorem Complexity.RationalHitting.StackLanguage.eval_fractionGcd (s : Store (Fin 12)) (hs : FractionScratch s) (hcan0 : (wordValue (s 0)).bits = s 0) (hcan5 : (wordValue (s 5)).bits = s 5) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) :
              ∃ t ≤ (2 * B + 1) * (500 * (B + 1) ^ 2 + 1) + 1, Eval (Program.rename (⇑fractionArith) gcdLoop) s (Function.update (Function.update s 0 ((wordValue (s 0)).gcd (wordValue (s 5))).bits) 5 []) t
              source
              theorem Complexity.RationalHitting.StackLanguage.eval_fractionQuotient (s : Store (Fin 12)) (hs : FractionScratch s) (hb : 0 < wordValue (s 5)) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) :
              ∃ t ≤ 400 * (B + 1) ^ 2, Eval (Program.rename (⇑fractionArith) quotient) s (Function.update s 0 (wordValue (s 0) / wordValue (s 5)).bits) t
              source
              theorem Complexity.RationalHitting.StackLanguage.fractionScratch_update (s : Store (Fin 12)) (hs : FractionScratch s) (i : Fin 12) (hi : i = 0 ∨ i = 5 ∨ 10 ≤ ↑i) (w : List Bool) :
              FractionScratch (Function.update s i w)