OAI/Computability/WLIdentification/ExponentialComputation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.WordExpressions.Exp line 12

   Source documentation

   One-exponential realizability by a single finite word expression, with an explicit bound on all its intermediate words.

   def Exp {n : ℕ} (f : (Fin n → Word) → Word) : Prop :=
   …

   Mentions: OAI.WLIdentification.Word

2. theorem OAI.WLIdentification.WordExpressions.Poly.toExp line 17
3. theorem OAI.WLIdentification.WordExpressions.Exp.congr line 24
4. theorem OAI.WLIdentification.WordExpressions.Exp.bindPoly line 30

   Source documentation

   Feeding one-exponential data to a fixed polynomial word program stays single-exponential; arbitrary composition of two exponential programs is not asserted.

   theorem bindPoly {f : (Fin n → Word) → Word} {g : (Fin (n+1) → Word) → Word}
       (hf : Exp f) (hg : Poly g) : Exp (fun S => g (Fin.snoc S (f S))) := by
   …

   Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.Exp, OAI.WLIdentification.WordExpressions.Poly

5. theorem OAI.WLIdentification.WordExpressions.Exp.loopPoly line 48
6. theorem OAI.WLIdentification.WordExpressions.Exp.powerBudget line 82
7. theorem OAI.WLIdentification.WordExpressions.Exp.inEXPTIME line 108

   Source documentation

   A genuine EXPTIME decider from a proved single-exponential Boolean program.

   theorem inEXPTIME {p : (Fin 1 → Word) → Bool} (hp : Exp (fun S => boolWord (p S))) :
       InEXPTIME {w | p (fun _ => w) = true} := by
   …

   Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.Exp, OAI.WLIdentification.WordExpressions.boolWord, OAI.WLIdentification.InEXPTIME

8. theorem OAI.WLIdentification.WordExpressions.inEXPTIME_of_budget line 128

   Source documentation

   A polynomial budget-relative test is executed on a physically generated unary exponential budget, rather than receiving an oracle-size bound.

   theorem inEXPTIME_of_budget {L : BinaryLanguage} (C d : ℕ)
       {p : (Fin 2 → Word) → Bool} (hp : BoolPoly p)
       (h : ∀ w, p ![w, unary (2^(C*(w.length+1)^d))] = true ↔ w ∈ L) : InEXPTIME L := by
   …

   Mentions: OAI.WLIdentification.BinaryLanguage, OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.BoolPoly, OAI.WLIdentification.WordExpressions.unary, OAI.WLIdentification.InEXPTIME

9. theorem OAI.WLIdentification.WordExpressions.BoolPoly.allRange line 148
10. theorem OAI.WLIdentification.WordExpressions.BoolPoly.anyRange line 156
11. theorem OAI.WLIdentification.WordExpressions.NatPoly.sumRange line 168
12. theorem OAI.WLIdentification.WordExpressions.Poly.tabulateRange line 180
13. theorem OAI.WLIdentification.WordExpressions.NatPoly.iteProp line 231
14. theorem OAI.WLIdentification.WordExpressions.BoolPoly.ite line 238
15. theorem OAI.WLIdentification.WordExpressions.BoolPoly.iteProp line 244