diff --git a/Complexity/Computability/Complexity/Problems/Clique.lean b/Complexity/Computability/Complexity/Problems/Clique.lean
index 3c5a157d85..2b4e33a775 100644
--- a/Complexity/Computability/Complexity/Problems/Clique.lean
+++ b/Complexity/Computability/Complexity/Problems/Clique.lean
@@ -122,6 +122,12 @@ theorem computableTidilyInPolyTime_compl :
   unfold compl encGraph
   fun_prop
 
+/-- Complementing a graph on its declared vertices is polynomial-time with the graph encoding. -/
+@[fun_prop]
+theorem computableInPolyTime_compl :
+    ComputableInPolyTime compl encGraph encGraph :=
+  .of_tidy computableTidilyInPolyTime_compl
+
 end Graph
 
 namespace Clique
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean
index 47feeb853d..941bbeec02 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean
@@ -491,4 +491,20 @@ theorem bitsPadWord {α : Type}
   .of_tidy (@Turing.MultiTapeTM.ComputableTidilyInPolyTime.bitsPadWord α input bound word
       hbound.tidy hword.tidy)
 
+/-- Repeat a fixed bit a unary number of times, including zero repetitions. -/
+@[fun_prop]
+theorem bitsReplicate (bit : Bool) :
+    ComputableInPolyTime (fun n => List.replicate n bit) encUnary encBits :=
+  .of_tidy (ComputableTidilyInPolyTime.bitsReplicate bit)
+
+/-- Apply a fixed Boolean operation pointwise to two computed raw words. The result stops at
+whichever word ends first; the two certificates retain their raw bit-string encoding. -/
+@[fun_prop]
+theorem bitsZipWithInput (op : Bool → Bool → Bool) {α : Type} {input : α ↪ List Bool}
+    {left right : α → List Bool}
+    (hleft : ComputableInPolyTime left input encBits)
+    (hright : ComputableInPolyTime right input encBits) :
+    ComputableInPolyTime (fun a => (left a).zipWith op (right a)) input encBits :=
+  .of_tidy (ComputableTidilyInPolyTime.bitsZipWithInput op hleft.tidy hright.tidy)
+
 end Turing.MultiTapeTM.ComputableInPolyTime
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
index 62ddcb0e00..f43a59c2d4 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
@@ -978,4 +978,14 @@ theorem mapWithInput {α : Type}
   .of_tidy (@Turing.MultiTapeTM.ComputableTidilyInPolyTime.mapWithInput α β γ encA encB encIn f
       list hlist.tidy hf.tidy)
 
+/-- Drop a computed unary number of bits from a computed raw word. Counts beyond the word
+length return the empty word, with no promise on the count or input. -/
+@[fun_prop]
+theorem bitsDropWithInput {α : Type} {input : α ↪ List Bool}
+    {list : α → List Bool} {count : α → ℕ}
+    (hlist : ComputableInPolyTime list input encBits)
+    (hcount : ComputableInPolyTime count input encUnary) :
+    ComputableInPolyTime (fun a => (list a).drop (count a)) input encBits :=
+  .of_tidy (ComputableTidilyInPolyTime.bitsDropWithInput hlist.tidy hcount.tidy)
+
 end Turing.MultiTapeTM.ComputableInPolyTime
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean
index 18e2885c8e..8ee5db6f5c 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean
@@ -121,4 +121,10 @@ theorem optionGetDWithInput {α : Type}
   .of_tidy (@Turing.MultiTapeTM.ComputableTidilyInPolyTime.optionGetDWithInput α β encA encB value
       fallback hvalue.tidy hfallback.tidy)
 
+/-- Construct an optional value while retaining the complete input encoding. -/
+@[fun_prop]
+theorem optionSome {α : Type} (enc : α ↪ List Bool) :
+    ComputableInPolyTime (some (α := α)) enc (encOption enc) :=
+  .of_tidy (ComputableTidilyInPolyTime.optionSome enc)
+
 end Turing.MultiTapeTM.ComputableInPolyTime