OAI/Computability/RationalHitting/BinaryBinomial.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RationalHitting.StackLanguage.multiplyClean line 9

   Source documentation

   Clean multiplication interface used by the finite rising-product loop.

   def multiplyClean : Program (Fin 8) :=
   …

   Mentions: OAI.RationalHitting.StackLanguage.Program

2. lemma OAI.RationalHitting.StackLanguage.eval_multiplyClean line 12
3. def OAI.RationalHitting.StackLanguage.factorMul line 46
4. def OAI.RationalHitting.StackLanguage.factorialScratch line 48
5. lemma OAI.RationalHitting.StackLanguage.eval_factorMul line 51
6. def OAI.RationalHitting.StackLanguage.factorialBody line 71

   Source documentation

   One rising-product step: multiply accumulator by the copied current index, advance the binary index, and drop one symbol of the unary loop counter.

   def factorialBody : Program (Fin 10) :=
   …

   Mentions: OAI.RationalHitting.StackLanguage.Program

7. lemma OAI.RationalHitting.StackLanguage.eval_factorialBody line 75
8. lemma OAI.RationalHitting.StackLanguage.factorial_wordValue_bits line 112
9. def OAI.RationalHitting.StackLanguage.factorialLoop line 119
10. lemma OAI.RationalHitting.StackLanguage.eval_factorialLoop line 123

    Source documentation

    Rising products, with a unary iteration budget obtained from the input. No scalar factorial operation occurs in this fixed finite program.

    lemma eval_factorialLoop (n L : ℕ) (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+n)≤L)
        (hi : (s 8).length+n≤L) :
        ∃ t≤n*(300*(L+1)^4+1)+1, ∃ v,
          Eval factorialLoop s v t ∧
          v 0 = (wordValue (s 0)*(wordValue (s 8)).ascFactorial n).bits ∧
          wordValue (v 8)=wordValue (s 8)+n ∧ v 9=[] ∧ factorialScratch v ∧
          (v 8).length≤(s 8).length+n := by
    …

    Mentions: OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.factorialScratch, OAI.RationalHitting.StackLanguage.wordValue, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.factorialLoop

11. theorem OAI.RationalHitting.StackLanguage.eval_factorial line 166

    Source documentation

    Ordinary factorial on unary n, including zero, with polynomial bit cost. The two binary registers initially contain 1; no computed value is an input.

    theorem eval_factorial (n : ℕ) (s : Store (Fin 10))
        (hf : factorialScratch s) (h0 : s 0=[true]) (h8 : s 8=[true])
        (h9 : (s 9).length=n) :
        ∃ t≤n*(300*(1+n*(1+n)+1)^4+1)+1, ∃ v,
          Eval factorialLoop s v t ∧ v 0=n.factorial.bits ∧
          wordValue (v 8)=n+1 ∧ v 9=[] ∧ factorialScratch v := by
    …

    Mentions: OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.factorialScratch, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.factorialLoop, OAI.RationalHitting.StackLanguage.wordValue

12. lemma OAI.RationalHitting.StackLanguage.factorial_bits_length line 183
13. def OAI.RationalHitting.StackLanguage.factorialCore line 199

    Source documentation

    Factorial with clean local registers: only the unary counter and output register are changed. This is the binary subroutine for the Taylor binomials.

    def factorialCore : Program (Fin 10) :=
    …

    Mentions: OAI.RationalHitting.StackLanguage.Program

14. lemma OAI.RationalHitting.StackLanguage.eval_factorialCore line 202
15. def OAI.RationalHitting.StackLanguage.unaryDiffBody line 235
16. def OAI.RationalHitting.StackLanguage.unaryDiff line 238
17. theorem OAI.RationalHitting.StackLanguage.eval_unaryDiff line 242

    Source documentation

    Variable-length subtraction of unary loop counters. The leftover flag is nonempty exactly when the second counter exceeded the first.

    theorem eval_unaryDiff {a b flag : K} (hab : a≠b) (haf : a≠flag) (hbf : b≠flag)
        (s : Store K) :
        Eval (unaryDiff a b flag) s
          (update (update (update s a ((s a).drop (s b).length)) b [])
            flag (List.replicate ((s b).length-(s a).length) true++s flag))
          (5*(s b).length+1) := by
    …

    Mentions: OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.unaryDiff

18. def OAI.RationalHitting.StackLanguage.Binomial.arith line 302
19. def OAI.RationalHitting.StackLanguage.Binomial.lowEmpty line 305
20. def OAI.RationalHitting.StackLanguage.Binomial.factorialCost line 306
21. def OAI.RationalHitting.StackLanguage.Binomial.factorBlock line 308
22. def OAI.RationalHitting.StackLanguage.Binomial.factorCost line 311
23. lemma OAI.RationalHitting.StackLanguage.Binomial.eval_factorBlock line 313
24. def OAI.RationalHitting.StackLanguage.Binomial.input line 367
25. def OAI.RationalHitting.StackLanguage.Binomial.prepared line 369
26. def OAI.RationalHitting.StackLanguage.Binomial.prepare line 372
27. lemma OAI.RationalHitting.StackLanguage.Binomial.eval_prepare line 375
28. lemma OAI.RationalHitting.StackLanguage.Binomial.lowEmpty_input line 397
29. lemma OAI.RationalHitting.StackLanguage.Binomial.lowEmpty_update line 400
30. lemma OAI.RationalHitting.StackLanguage.Binomial.lowEmpty_prepared line 404