From 34af428cd0e2a29a94b0d7aeb3e86c702348c2ef Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 24 Oct 2026 09:48:34 -0400
Subject: [PATCH 1/2] feat(polytime): expose plain word and option construction
 rules

---
 .../MultiTape/Complexity/PolyTime/BitString.lean | 16 ++++++++++++++++
 .../MultiTape/Complexity/PolyTime/List.lean      | 10 ++++++++++
 .../MultiTape/Complexity/PolyTime/Option.lean    |  6 ++++++
 3 files changed, 32 insertions(+)

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

From 927f7323ecb86881fdbae96ffc8c3c9241f5766c Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 24 Oct 2026 09:51:44 -0400
Subject: [PATCH 2/2] feat(clique): expose plain graph complement certificate

---
 Complexity/Computability/Complexity/Problems/Clique.lean | 6 ++++++
 1 file changed, 6 insertions(+)

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