From c0cc3261079718a7bf4f0f0345c5310caf1a24f9 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Thu, 29 Oct 2026 16:39:11 +0000
Subject: [PATCH] refactor(Computability/PolyTime): deduplicate certificate and
 fold helpers (#949)

---
 .../BoundedIncidenceCounter.lean              |   4 +-
 .../BoundedIncidenceSemantics.lean            |  14 ---
 .../BoundedIncidenceStepCert.lean             | 117 +-----------------
 .../BooleanAnalysis/SparsePolyCounter.lean    |  10 +-
 .../CNF/BranchedSparseCNFCounter.lean         |   9 +-
 .../PolyTime/CNF/GreedyParityContext.lean     |  75 -----------
 .../PolyTime/CNF/GreedyParitySearch.lean      |  19 +--
 .../PolyTime/CNF/SparseCNFLeafCounter.lean    |   6 -
 .../PolyTime/CommonCountingAccum.lean         |  19 ++-
 .../PolyTime/GreedyLabelSchedule.lean         |   5 +-
 .../PolyTime/GreedySlotScore.lean             |   6 +-
 .../PolyTime/ParityFactorEval.lean            |   2 +-
 .../PolyTime/SparseMonomialJet.lean           |   7 --
 13 files changed, 36 insertions(+), 257 deletions(-)

diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
index 64f6785a1..82a2b1db0 100644
--- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
+++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
@@ -66,8 +66,8 @@ bounded-incidence, bounded-width $\mathbb{F}_2$ polynomial-system branch evaluat
 
 namespace Cslib.Complexity.SubexponentialSAT.SparsePolyCounter
 
-open Finset Cslib Cslib.BitString Cslib.Complexity Cslib.GenericRAM Cslib.LinearAlgebra
-open Turing.MultiTapeTM
+open Finset Cslib Cslib.BitString Cslib.CommonCountingAccum Cslib.Complexity Cslib.GenericRAM
+open Cslib.LinearAlgebra Turing.MultiTapeTM
 
 local notation "encSys" => encList (encList (encList encNat))
 
diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean
index 2fbadb1a1..573698f9c 100644
--- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean
+++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean
@@ -444,20 +444,6 @@ private theorem sum_card_listScopeFamily_augScopes (n' : ℕ) (eqs' : List (List
   exact Finset.sum_congr rfl fun f _ =>
     congrArg Finset.card (listScopeFamily_map_equationVars n' eqs' f)
 
-private theorem le_foldl_max_of_mem {init x : ℕ} {l : List ℕ} (hx : x ∈ l) :
-    x ≤ l.foldl max init := by
-  have hinit : ∀ (m : ℕ) (ys : List ℕ), m ≤ ys.foldl max m := fun m ys => by
-    induction ys generalizing m with
-    | nil => exact le_rfl
-    | cons b bs ih => exact le_trans (Nat.le_max_left m b) (ih (max m b))
-  induction l generalizing init with
-  | nil => cases hx
-  | cons a as ih =>
-    simp only [List.foldl_cons]
-    rcases List.mem_cons.mp hx with rfl | hmem
-    · exact le_trans (Nat.le_max_right init x) (hinit (max init x) as)
-    · exact ih hmem
-
 private theorem varIncidence_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : List (List (List ℕ)))
     (v : Fin n') :
     let augScopes := withNeutralScopesList (eqs'.map equationVars) n'
diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean
index fa03af8aa..be24fe4a5 100644
--- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean
+++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean
@@ -76,8 +76,8 @@ globally polynomial workspace.
 
 namespace Cslib.Complexity.SubexponentialSAT.SparsePolyCounter
 
-open Finset Cslib Cslib.BitString Cslib.Complexity Cslib.GenericRAM Cslib.LinearAlgebra
-open Turing.MultiTapeTM
+open Finset Cslib Cslib.BitString Cslib.CommonCountingAccum Cslib.Complexity Cslib.GenericRAM
+open Cslib.LinearAlgebra Turing.MultiTapeTM
 
 local notation "encSys" => encList (encList (encList encNat))
 
@@ -566,28 +566,6 @@ section LoopCertificates
 
 open ComputableInPolyTime
 
-private theorem le_foldl_max_init (init : ℕ) (xs : List ℕ) : init ≤ xs.foldl max init := by
-  induction xs generalizing init with
-  | nil => exact le_rfl
-  | cons b bs ih => exact (Nat.le_max_left init b).trans (ih (max init b))
-
-private theorem le_foldl_max_of_mem {xs : List ℕ} {x init : ℕ} (hx : x ∈ xs) :
-    x ≤ xs.foldl max init := by
-  induction xs generalizing init with
-  | nil => cases hx
-  | cons a as ih =>
-    rcases List.mem_cons.mp hx with rfl | hmem
-    · exact (Nat.le_max_right init x).trans (le_foldl_max_init (max init x) as)
-    · exact ih hmem
-
-private theorem foldl_max_le {xs : List ℕ} {init B : ℕ} (hinit : init ≤ B)
-    (hxs : ∀ x ∈ xs, x ≤ B) : xs.foldl max init ≤ B := by
-  induction xs generalizing init with
-  | nil => exact hinit
-  | cons a as ih =>
-    exact ih (max_le hinit (hxs a (List.mem_cons_self ..))) fun x hx =>
-      hxs x (List.mem_cons_of_mem _ hx)
-
 /-- Maximum unary-clamped variable-group dimension `min (2 * n') |V_{t,g}|` across `g < r_u` at a
 fixed interpolation node `t`. -/
 def maxGroupDim (n' r_u : ℕ) (vGroups_t : List (List ℕ)) : ℕ :=
@@ -608,51 +586,6 @@ private theorem maxGroupDim_le_maxAllGroupDim {n' Q_u r_u t : ℕ}
     maxGroupDim n' r_u (varGroups.getD t []) ≤ maxAllGroupDim n' Q_u r_u varGroups :=
   le_foldl_max_of_mem (List.mem_map.mpr ⟨t, List.mem_range.mpr ht, rfl⟩)
 
-private def HasPolySpace {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool}
-    {f : α → β} (c : NativeCertificate f ei eo) : Prop :=
-  PolyBounded (fun a => (ei a).length) c.space
-
-private theorem polyBounded_length_of_hasPolySpace {α β : Type} {ei : α ↪ List Bool}
-    {eo : β ↪ List Bool} {f : α → β} {c : NativeCertificate f ei eo} (hc : HasPolySpace c) :
-    PolyBounded (fun a => (ei a).length) (fun a => (eo (f a)).length) := by
-  obtain ⟨c₀, d₀, hs⟩ := hc.exists_le
-  obtain ⟨k, _, hl⟩ := c.computes
-  refine .of_forall_le (k * (c₀ + 1)) d₀ fun a => (hl a).trans ?_
-  have h1 : 1 ≤ ((ei a).length + 1) ^ d₀ := Nat.one_le_pow _ _ (Nat.succ_pos _)
-  have := hs a; nlinarith
-
-private theorem hasPolySpace_comp {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
-    {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} {d : NativeCertificate g em eo}
-    {c : NativeCertificate f ei em} (hd : HasPolySpace d) (hc : HasPolySpace c) :
-    HasPolySpace (d.comp c) := hc.add (hd.comp (polyBounded_length_of_hasPolySpace hc))
-
-private theorem hasPolySpace_prod {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
-    {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} {c : NativeCertificate f ei em}
-    {d : NativeCertificate g ei eo} (hc : HasPolySpace c) (hd : HasPolySpace d) :
-    HasPolySpace (c.prod d) := hc.add hd
-
-private theorem exists_natAbs_rowEntry_le_two_pow {ι γ : Type} {sz : ι → ℕ}
-    {encΓ : γ ↪ List Bool} {f : γ → JetRows} {L : ι → ℕ}
-    (hf : PolyBounded (fun y => (encΓ y).length) (fun y => (encJet (f y)).length))
-    (hL : PolyBounded sz L) :
-    ∃ M : ι → ℕ, PolyBounded sz M ∧
-      ∀ x y, (encΓ y).length ≤ L x → ∀ j u, (rowEntry (f y) j u).natAbs ≤ 2 ^ M x := by
-  obtain ⟨c, d, hle⟩ := hf.exists_le
-  refine ⟨fun x => c * (L x + 1) ^ d, NativeCertificate.polyBounded_pow_of_polyBounded hL c d,
-    fun x y hy j u => ?_⟩
-  have hout := (hle y).trans
-    (Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hy 1) d))
-  exact (Nat.size_le.mp
-    ((CommonCountingAccum.size_natAbs_rowEntry_le_length_encJetRows (f y) j u).trans hout)).le
-
-private theorem foldl_keep_fst {ι π α : Type*} (step : π → α → ι → α)
-    (par : π) (xs : List ι) (init : α) :
-    xs.foldl (fun pa i => (pa.1, step pa.1 pa.2 i)) (par, init) =
-      (par, xs.foldl (step par) init) := by
-  induction xs generalizing init with
-  | nil => rfl
-  | cons _ _ ih => exact ih _
-
 private theorem foldl_optAddJet_spec (J ℓ j M : ℕ) (f : ℕ → Option JetRows)
     (hf : ∀ i < j, ∀ y, f i = some y → ∀ j' < J, ∀ u' < ℓ, (rowEntry y j' u').natAbs ≤ M) :
     let res := (List.range j).foldl
@@ -688,52 +621,6 @@ private theorem length_encJetRows_foldl_optAddJet_le {J ℓ j N M : ℕ} {f : 
     (Nat.size_le_size ((hbd j' hj' u' hu').trans (Nat.mul_le_mul_right M hj))).trans
       (Nat.size_mul_le N M)
 
-private theorem computableInO_snd_indexFold {ι β : Type} {encIn : ι ↪ List Bool}
-    {encB : β ↪ List Bool} {count : ι → ℕ} {initial : ι → β} {body : ℕ × β → β}
-    (cn : NativeCertificate count encIn encNat) (ci : NativeCertificate initial encIn encB)
-    (cb : NativeCertificate body (encPair encNat encB) encB)
-    (hcn : cn.IsPolynomial) (hci : ci.IsPolynomial) (hcb : HasPolySpace cb)
-    {B : ι → ℕ} (hB_pb : PolyBounded (fun x => (encIn x).length) B)
-    (hB : ∀ x j, j ≤ count x → (encB (IndexFold.run body j (initial x)).2).length ≤ B x)
-    (R P_cb : ι → ℕ) (hP_cb : PolyBounded (fun x => (encIn x).length) P_cb)
-    (hR : ∀ x j, j ≤ count x →
-      (encPair encNat encB (IndexFold.run body j (initial x))).length ≤
-        2 * (encNat (count x)).length + 1 + B x →
-      cb.time (IndexFold.run body j (initial x)) ≤ R x + P_cb x) :
-    ∃ P : ι → ℕ, PolyBounded (fun x => (encIn x).length) P ∧
-      ComputableInO (fun x => (IndexFold.run body (count x) (initial x)).2) encIn encB
-        (fun x => (count x + 1) * (R x + P x)) P := by
-  have hcnt_pb := (cn.polyTime hcn).polyBounded_length
-  let S_st : ι → ℕ := fun x => 2 * (encNat (count x)).length + 1 + B x
-  have hSst_pb := (((PolyBounded.const 2).mul hcnt_pb).add (.const 1)).add hB_pb
-  obtain ⟨cs, ds, hcs⟩ := hcb.exists_le
-  let Q : ι → ℕ := fun x => cs * (S_st x + 1) ^ ds
-  have hQ_pb := NativeCertificate.polyBounded_pow_of_polyBounded hSst_pb cs ds
-  have hsq_pb := NativeCertificate.polyBounded_pow_of_polyBounded hcnt_pb 1 2
-  have hloop := IndexFold.computableInO cn ci cb (fun x => R x + P_cb x) Q B
-    (fun x j hj => hR x j hj (IndexFold.length_run_le body (initial x) hj (hB x j hj)))
-    (fun x j hj => (hcs _).trans (Nat.mul_le_mul_left cs (Nat.pow_le_pow_left
-      (Nat.add_le_add_right (IndexFold.length_run_le body (initial x) hj (hB x j hj)) 1) ds))) hB
-  let cLoop : NativeCertificate (fun x => IndexFold.run body (count x) (initial x))
-      encIn (encPair encNat encB) := ⟨_, _, hloop⟩
-  let P : ι → ℕ := fun x => cn.time x + cn.space x + (encIn x).length + ci.time x + ci.space x +
-    2 * S_st x + 2 * (1 * ((encNat (count x)).length + 1) ^ 2) + P_cb x + Q x +
-    2 * (encNat (count x)).length + 1
-  have hP_pb : PolyBounded (fun x => (encIn x).length) P :=
-    ((((((((((hcn.1.add hcn.2).add .self).add hci.1).add hci.2).add
-      ((PolyBounded.const 2).mul hSst_pb)).add ((PolyBounded.const 2).mul hsq_pb)).add
-      hP_cb).add hQ_pb).add ((PolyBounded.const 2).mul hcnt_pb)).add (.const 1))
-  refine ⟨P, hP_pb, (NativeCertificate.snd cLoop).computes.mono_le (fun x => ?_) (fun x => ?_)⟩
-  · have hinit_le := Nat.le_mul_of_pos_left (cn.time x + ((encIn x).length + ci.time x))
-      (Nat.succ_pos (count x))
-    have hstep_le : (S_st x + ((encNat (count x)).length + 1) ^ 2 + (R x + P_cb x)) +
-        S_st x + ((encNat (count x)).length + 1) ^ 2 ≤
-        R x + (2 * S_st x + 2 * (1 * ((encNat (count x)).length + 1) ^ 2) + P_cb x) := by omega
-    have hmul_le := Nat.add_le_add hinit_le (Nat.mul_le_mul_left (count x + 1) hstep_le)
-    rw [← Nat.mul_add] at hmul_le
-    exact hmul_le.trans (Nat.mul_le_mul_left (count x + 1) (by dsimp only [P]; omega))
-  · dsimp only [NativeCertificate.snd_space, cLoop, S_st, P]; omega
-
 private def mapRangeStep {γ δ : Type} (f : γ × ℕ → δ)
     (p : ℕ × ((ℕ × γ) × List δ)) : (ℕ × γ) × List δ :=
   if decide (p.1 < p.2.1.1) then (p.2.1, p.2.2 ++ [f (p.2.1.2, min p.2.1.1 p.1)]) else p.2
diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean
index bc66c7cfc..d6fb6e70b 100644
--- a/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean
+++ b/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean
@@ -219,17 +219,21 @@ def branchNeutralScope (n' : ℕ) (eqs' : List (List (List ℕ))) :
     Fin eqs'.length ⊕ Fin n' → Finset (Fin n') :=
   withNeutralScope fun i => equationScope (HeavyBranchFold.toFinsetEquation n' eqs'[i])
 
-private theorem foldl_max_le_iff {l : List ℕ} {init B : ℕ} :
+theorem foldl_max_le_iff {l : List ℕ} {init B : ℕ} :
     l.foldl max init ≤ B ↔ init ≤ B ∧ ∀ x ∈ l, x ≤ B := by
   induction l generalizing init with
   | nil => simp only [List.foldl_nil, List.not_mem_nil, IsEmpty.forall_iff, implies_true, and_true]
   | cons a as ih =>
     simp only [List.foldl_cons, ih, Nat.max_le, List.mem_cons, forall_eq_or_imp, and_assoc]
 
-private theorem le_foldl_max_init (init : ℕ) (l : List ℕ) : init ≤ l.foldl max init :=
+theorem foldl_max_le {l : List ℕ} {init B : ℕ} (hinit : init ≤ B) (hl : ∀ x ∈ l, x ≤ B) :
+    l.foldl max init ≤ B :=
+  foldl_max_le_iff.mpr ⟨hinit, hl⟩
+
+theorem le_foldl_max_init (init : ℕ) (l : List ℕ) : init ≤ l.foldl max init :=
   (foldl_max_le_iff.mp le_rfl).1
 
-private theorem le_foldl_max_of_mem {init : ℕ} {l : List ℕ} {x : ℕ} (hx : x ∈ l) :
+theorem le_foldl_max_of_mem {init : ℕ} {l : List ℕ} {x : ℕ} (hx : x ∈ l) :
     x ≤ l.foldl max init := (foldl_max_le_iff.mp le_rfl).2 x hx
 
 theorem checkVarsLt_eq_true_iff {n : ℕ} {sys : List (List (List ℕ))} :
diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
index 8ad23e017..0e9d4fa9f 100644
--- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
+++ b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
@@ -538,13 +538,6 @@ private theorem scopeWidthOn_le_mul (N k maxTerms : ℕ) (eq : List (List ℕ))
     _ ≤ eq.length * k := List.length_flatMap_le hdeg
     _ ≤ maxTerms * k := Nat.mul_le_mul_right k hlen
 
-private theorem foldl_max_le_of_forall {l : List ℕ} {init B : ℕ} (hi : init ≤ B)
-    (hl : ∀ x ∈ l, x ≤ B) : l.foldl max init ≤ B := by
-  induction l generalizing init with
-  | nil => exact hi
-  | cons a as ih =>
-    exact ih (max_le hi (hl a List.mem_cons_self)) fun x hx => hl x (List.mem_cons_of_mem a hx)
-
 private theorem compiled_system_incidence_bounds (k C_B β_B : ℕ) :
     ∃ C_inc : ℕ, 12 ≤ C_inc ∧ ∀ {N m B : ℕ} {sys : List (List (List ℕ))},
       2 ≤ N → B ≤ C_B * Nat.clog 2 N ^ β_B → m ≤ B * N →
@@ -573,7 +566,7 @@ private theorem compiled_system_incidence_bounds (k C_B β_B : ℕ) :
     Nat.pow_le_pow_right hlam1 (by omega)
   have hw_le : branchMaxFactorWidth N sys ≤ C_inc * lam ^ (2 * β_B + 4) := by
     unfold branchMaxFactorWidth
-    refine foldl_max_le_of_forall (Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1) fun w hw => ?_
+    refine foldl_max_le (Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1) fun w hw => ?_
     obtain ⟨eq, heq, rfl⟩ := List.mem_map.mp hw
     have h1 := (hsc_all eq heq).trans (hT_le.trans (Nat.mul_le_mul_left _ hpow_step))
     dsimp only [C_inc]; nlinarith
diff --git a/Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean b/Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean
index 29e88c199..a96e34279 100644
--- a/Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean
+++ b/Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean
@@ -70,66 +70,6 @@ namespace Cslib.Logic.PL.CNF.GreedyContext
 open Finset Cslib.BitString Cslib.GenericRAM Turing.MultiTapeTM
 variable {C : Type} {encC : C ↪ List Bool}
 
-private def candRowOfState (s : ℕ × SelectBestAcc) : List Bool :=
-  materializeTestRow s.2.1.1 (decodeTestTuple s.2.1.1 s.2.1.2 s.1)
-
-private theorem computableInPolyTime_candRowOfState :
-    ComputableInPolyTime candRowOfState (encPair encNat encSelectBestAcc) encBits := by
-  unfold candRowOfState encSelectBestAcc
-  let encRest := encPair (encList encBits) (encOption (encPair encBits encNat))
-  let encAcc := encPair (encPair encUnary encUnary) encRest
-  have hj := ComputableInPolyTime.fst encNat encAcc
-  have hmP := (ComputableInPolyTime.fst (encPair encUnary encUnary) encRest).comp
-    (ComputableInPolyTime.snd encNat encAcc)
-  have hm := (ComputableInPolyTime.fst encUnary encUnary).comp hmP
-  have hP := (ComputableInPolyTime.snd encUnary encUnary).comp hmP
-  exact computableInPolyTime_materializeTestRow' hm (computableInPolyTime_decodeTestTuple' hm hP hj)
-
-private def augCandidateRows (s : ℕ × SelectBestAcc) : List (List Bool) :=
-  s.2.2.1 ++ [candRowOfState s]
-
-private theorem computableInPolyTime_augCandidateRows :
-    ComputableInPolyTime augCandidateRows (encPair encNat encSelectBestAcc) (encList encBits) := by
-  unfold augCandidateRows
-  have hcand := computableInPolyTime_candRowOfState
-  unfold encSelectBestAcc at hcand ⊢
-  let encRest := encPair (encList encBits) (encOption (encPair encBits encNat))
-  have hrows := (ComputableInPolyTime.fst (encList encBits) _).comp
-    ((ComputableInPolyTime.snd (encPair encUnary encUnary) encRest).comp
-      (ComputableInPolyTime.snd encNat (encPair (encPair encUnary encUnary) encRest)))
-  exact (ComputableInPolyTime.snoc encBits).comp (hrows.prod hcand)
-
-private def finishSelectBestStep (p : (ℕ × SelectBestAcc) × ℕ) : SelectBestAcc :=
-  let candRow := candRowOfState p.1
-  let nextBest := p.1.2.2.2.elim (some (candRow, p.2)) fun best =>
-    if decide (p.2 < best.2) then some (candRow, p.2) else some best
-  (p.1.2.1, (p.1.2.2.1, nextBest))
-
-private theorem computableInPolyTime_finishSelectBestStep :
-    ComputableInPolyTime finishSelectBestStep
-      (encPair (encPair encNat encSelectBestAcc) encNat) encSelectBestAcc := by
-  unfold finishSelectBestStep
-  have hcand0 := computableInPolyTime_candRowOfState
-  unfold encSelectBestAcc at hcand0 ⊢
-  let eBest := encPair encBits encNat; let encRest := encPair (encList encBits) (encOption eBest)
-  let encAcc := encPair (encPair encUnary encUnary) encRest
-  let encIn := encPair (encPair encNat encAcc) encNat
-  have hs := ComputableInPolyTime.fst (encPair encNat encAcc) encNat
-  have hval := ComputableInPolyTime.snd (encPair encNat encAcc) encNat
-  have hacc := (ComputableInPolyTime.snd encNat encAcc).comp hs
-  have hmP := (ComputableInPolyTime.fst (encPair encUnary encUnary) encRest).comp hacc
-  have hrest := (ComputableInPolyTime.snd (encPair encUnary encUnary) encRest).comp hacc
-  have hrows := (ComputableInPolyTime.fst (encList encBits) (encOption eBest)).comp hrest
-  have hbestOpt := (ComputableInPolyTime.snd (encList encBits) (encOption eBest)).comp hrest
-  have hsomeCand := (ComputableInPolyTime.optionSome eBest).comp ((hcand0.comp hs).prod hval)
-  refine hmP.prod (hrows.prod
-    (ComputableInPolyTime.optionElimWithInput hbestOpt hsomeCand ?_))
-  have hq_in := ComputableInPolyTime.fst encIn eBest
-  have hq_best := ComputableInPolyTime.snd encIn eBest
-  exact (ComputableInPolyTime.binary_lt' (hval.comp hq_in)
-    ((ComputableInPolyTime.snd encBits encNat).comp hq_best)).ite (hsomeCand.comp hq_in)
-      ((ComputableInPolyTime.optionSome eBest).comp hq_best)
-
 private def augment (s : ℕ × C × SelectBestAcc) : C × List (List Bool) :=
   (s.2.1, augCandidateRows (s.1, s.2.2))
 
@@ -316,21 +256,6 @@ theorem count_greedy_eq_card_sat {V : Type*} [Fintype V] [DecidableEq V]
       #{σ : V → Bool | φ.eval σ = true} :=
   countSys_greedyParityRows_eq_card_sat φ hn hP hinit_len hcount hinit
 
-private theorem exists_mono_poly {α : Type} {size u : α → ℕ} (hu : PolyBounded size u) :
-    ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧ ∀ a, u a ≤ p (size a) := by
-  obtain ⟨c, d, h⟩ := hu.exists_le
-  exact ⟨fun n => c * (n + 1) ^ d, by fun_prop,
-    fun _ _ hxy => Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hxy 1) d), h⟩
-
-private theorem exists_mono_poly_cert {α β : Type} {f : α → β}
-    {ei : α ↪ List Bool} {eo : β ↪ List Bool} (hf : ComputableInPolyTime f ei eo) :
-    ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧
-      ∀ a, (NativeCertificate.ofPolyTime hf).time a ≤ p (ei a).length ∧
-        (NativeCertificate.ofPolyTime hf).space a ≤ p (ei a).length := by
-  have hc := NativeCertificate.ofPolyTime_isPolynomial hf
-  obtain ⟨p, hp, hmono, hle⟩ := exists_mono_poly (hc.1.add hc.2)
-  exact ⟨p, hp, hmono, fun a => ⟨by have := hle a; omega, by have := hle a; omega⟩⟩
-
 private theorem input_le (c : C) (m P : ℕ) (rows : List (List Bool)) :
     (encC c).length ≤ (encInput encC (c, m, P, rows)).length ∧
     m ≤ (encInput encC (c, m, P, rows)).length ∧
diff --git a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
index b9dea3b88..ebc04ecff 100644
--- a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
+++ b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
@@ -795,10 +795,11 @@ open Finset Cslib.BitString Cslib.GenericRAM Turing.MultiTapeTM
 
 /-! ### Native `IndexFold` certificates and `ComputableInO` / `ComputableInPolySpace` bounds -/
 
-private def candRowOfState (s : ℕ × SelectBestAcc) : List Bool :=
+/-- Candidate test row decoded and materialized from an `IndexFold` state `(j, acc)`. -/
+@[expose] def candRowOfState (s : ℕ × SelectBestAcc) : List Bool :=
   materializeTestRow s.2.1.1 (decodeTestTuple s.2.1.1 s.2.1.2 s.1)
 
-private theorem computableInPolyTime_candRowOfState :
+theorem computableInPolyTime_candRowOfState :
     ComputableInPolyTime candRowOfState (encPair encNat encSelectBestAcc) encBits := by
   unfold candRowOfState encSelectBestAcc
   let encRest := encPair (encList encBits) (encOption (encPair encBits encNat))
@@ -810,10 +811,11 @@ private theorem computableInPolyTime_candRowOfState :
   have hP := (ComputableInPolyTime.snd encUnary encUnary).comp hmP
   exact computableInPolyTime_materializeTestRow' hm (computableInPolyTime_decodeTestTuple' hm hP hj)
 
-private def augCandidateRows (s : ℕ × SelectBestAcc) : List (List Bool) :=
+/-- Existing parity-test rows extended with the candidate row at `IndexFold` state `s`. -/
+@[expose] def augCandidateRows (s : ℕ × SelectBestAcc) : List (List Bool) :=
   s.2.2.1 ++ [candRowOfState s]
 
-private theorem computableInPolyTime_augCandidateRows :
+theorem computableInPolyTime_augCandidateRows :
     ComputableInPolyTime augCandidateRows (encPair encNat encSelectBestAcc) (encList encBits) := by
   unfold augCandidateRows
   have hcand := computableInPolyTime_candRowOfState
@@ -824,13 +826,14 @@ private theorem computableInPolyTime_augCandidateRows :
       (ComputableInPolyTime.snd encNat (encPair (encPair encUnary encUnary) encRest)))
   exact (ComputableInPolyTime.snoc encBits).comp (hrows.prod hcand)
 
-private def finishSelectBestStep (p : (ℕ × SelectBestAcc) × ℕ) : SelectBestAcc :=
+/-- Update `SelectBestAcc` after evaluating the candidate score `p.2` at `IndexFold` state `p.1`. -/
+@[expose] def finishSelectBestStep (p : (ℕ × SelectBestAcc) × ℕ) : SelectBestAcc :=
   let candRow := candRowOfState p.1
   let nextBest := p.1.2.2.2.elim (some (candRow, p.2)) fun best =>
     if decide (p.2 < best.2) then some (candRow, p.2) else some best
   (p.1.2.1, (p.1.2.2.1, nextBest))
 
-private theorem computableInPolyTime_finishSelectBestStep :
+theorem computableInPolyTime_finishSelectBestStep :
     ComputableInPolyTime finishSelectBestStep
       (encPair (encPair encNat encSelectBestAcc) encNat) encSelectBestAcc := by
   unfold finishSelectBestStep
@@ -981,13 +984,13 @@ noncomputable def greedyParityRowsCertificate {countSys : List (List Bool) → 
 
 /-! ### Live-state length bounds and `ComputableInO` / `ComputableInPolySpace` theorems -/
 
-private theorem exists_mono_poly {α : Type} {size u : α → ℕ} (hu : PolyBounded size u) :
+theorem exists_mono_poly {α : Type} {size u : α → ℕ} (hu : PolyBounded size u) :
     ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧ ∀ a, u a ≤ p (size a) := by
   obtain ⟨c, d, h⟩ := hu.exists_le
   exact ⟨fun n => c * (n + 1) ^ d, by fun_prop,
     fun _ _ hxy => Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hxy 1) d), h⟩
 
-private theorem exists_mono_poly_cert {α β : Type} {f : α → β}
+theorem exists_mono_poly_cert {α β : Type} {f : α → β}
     {ei : α ↪ List Bool} {eo : β ↪ List Bool} (hf : ComputableInPolyTime f ei eo) :
     ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧
       ∀ a, (NativeCertificate.ofPolyTime hf).time a ≤ p (ei a).length ∧
diff --git a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean
index caa116aa9..e5cd7f179 100644
--- a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean
+++ b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean
@@ -478,12 +478,6 @@ def ValidPolyTimeBound (encP : P ↪ List Bool) (NOf BOf : P → ℕ) (k N₀ :
       (encPair encUnary encSys (NOf x.1, sys)).length ≤ polySys (encPair encP encCNF x).length →
       cPoly.time (NOf x.1, sys) ≤ R x
 
-private theorem exists_mono_poly {α : Type} {size u : α → ℕ} (hu : PolyBounded size u) :
-    ∃ p : ℕ → ℕ, Cslib.PolynomiallyBounded p ∧ Monotone p ∧ ∀ a, u a ≤ p (size a) := by
-  obtain ⟨c, d, h⟩ := hu.exists_le
-  exact ⟨fun n => c * (n + 1) ^ d, by fun_prop,
-    fun _ _ hxy => Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hxy 1) d), h⟩
-
 private theorem polyBounded_output_of_space {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool}
     {f : α → β} (c : NativeCertificate f ei eo)
     (hs : PolyBounded (fun a => (ei a).length) c.space) :
diff --git a/Complexity/Computability/PolyTime/CommonCountingAccum.lean b/Complexity/Computability/PolyTime/CommonCountingAccum.lean
index c8d9fbe31..722899fb5 100644
--- a/Complexity/Computability/PolyTime/CommonCountingAccum.lean
+++ b/Complexity/Computability/PolyTime/CommonCountingAccum.lean
@@ -89,6 +89,7 @@ when `w = 0`; clearing theorems hold in any `CommRing K`; and Cramer recovery re
 namespace Cslib.CommonCountingAccum
 
 open Cslib.BitString Cslib.GenericRAM Turing.MultiTapeTM
+open ComputableTidilyInO (length_encNat_mono)
 
 local notation "encJet" => encList (encList encIntBin)
 local notation "encJets" => encList (encList (encList encIntBin))
@@ -450,7 +451,7 @@ theorem jetL1Norm_weightedProdJet_le (J ℓ : ℕ) (w : ℤ) (groups : List JetR
 
 section SharedHelpers
 
-private theorem foldl_keep_fst {ι π α : Type*} (step : π → α → ι → α)
+theorem foldl_keep_fst {ι π α : Type*} (step : π → α → ι → α)
     (par : π) (xs : List ι) (init : α) :
     xs.foldl (fun pa i => (pa.1, step pa.1 pa.2 i)) (par, init) =
       (par, xs.foldl (step par) init) := by
@@ -504,10 +505,11 @@ private theorem length_encJetRows_rangeAddJet_le {J ℓ j N M : ℕ} {f : ℕ 
     (Nat.size_le_size ((natAbs_rowEntry_rangeAddJet_le J ℓ j M f hM j' u').trans
       (Nat.mul_le_mul_right M hj))).trans (Nat.size_mul_le N M)
 
-private def HasPolySpace {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool}
+/-- A native certificate `c` has polynomially bounded workspace in the encoded input length. -/
+def HasPolySpace {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool}
     {f : α → β} (c : NativeCertificate f ei eo) : Prop :=
   PolyBounded (fun a => (ei a).length) c.space
-private theorem polyBounded_length_of_hasPolySpace {α β : Type} {ei : α ↪ List Bool}
+theorem polyBounded_length_of_hasPolySpace {α β : Type} {ei : α ↪ List Bool}
     {eo : β ↪ List Bool} {f : α → β} {c : NativeCertificate f ei eo} (hc : HasPolySpace c) :
     PolyBounded (fun a => (ei a).length) (fun a => (eo (f a)).length) := by
   obtain ⟨c₀, d₀, hs⟩ := hc.exists_le
@@ -515,11 +517,11 @@ private theorem polyBounded_length_of_hasPolySpace {α β : Type} {ei : α ↪ L
   refine .of_forall_le (k * (c₀ + 1)) d₀ fun a => (hl a).trans ?_
   have h1 : 1 ≤ ((ei a).length + 1) ^ d₀ := Nat.one_le_pow _ _ (Nat.succ_pos _)
   have := hs a; nlinarith
-private theorem hasPolySpace_comp {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
+theorem hasPolySpace_comp {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
     {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} {d : NativeCertificate g em eo}
     {c : NativeCertificate f ei em} (hd : HasPolySpace d) (hc : HasPolySpace c) :
     HasPolySpace (d.comp c) := hc.add (hd.comp (polyBounded_length_of_hasPolySpace hc))
-private theorem hasPolySpace_prod {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
+theorem hasPolySpace_prod {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool}
     {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} {c : NativeCertificate f ei em}
     {d : NativeCertificate g ei eo} (hc : HasPolySpace c) (hd : HasPolySpace d) :
     HasPolySpace (c.prod d) := hc.add hd
@@ -541,9 +543,6 @@ private theorem computableInPolySpace_of_inO {α β : Type} {ei : α ↪ List Bo
     Nat.mul_le_mul_left k (Nat.add_le_add_right (hPb x) 1)
   exact ⟨_, b, by dsimp only [b]; fun_prop, htm.mono (fun _ => le_rfl) hk,
     fun x => (hl x).trans (hk x)⟩
-private theorem length_encNat_mono {a b : ℕ} (h : a ≤ b) :
-    (encNat a).length ≤ (encNat b).length := by
-  simpa only [encNat_apply, Nat.size_eq_bits_len] using Nat.size_le_size h
 private theorem pb_aff {ι : Type} {sz f g : ι → ℕ} (a b c : ℕ)
     (hf : PolyBounded sz f) (hg : PolyBounded sz g) :
     PolyBounded sz (fun x => a * f x + b * g x + c) :=
@@ -554,7 +553,7 @@ private theorem polyBounded_jetEncBound {ι : Type} {sz J ℓ K M : ι → ℕ}
     PolyBounded sz (fun x => J x * (2 * (ℓ x * (2 * (K x + M x) + 3)) + 1)) :=
   hJ.mul (((PolyBounded.const 2).mul (hℓ.mul
     (((PolyBounded.const 2).mul (hK.add hM)).add (.const 3)))).add (.const 1))
-private theorem exists_natAbs_rowEntry_le_two_pow {ι γ : Type} {sz : ι → ℕ}
+theorem exists_natAbs_rowEntry_le_two_pow {ι γ : Type} {sz : ι → ℕ}
     {encΓ : γ ↪ List Bool} {f : γ → JetRows} {L : ι → ℕ}
     (hf : PolyBounded (fun y => (encΓ y).length) (fun y => (encJet (f y)).length))
     (hL : PolyBounded sz L) :
@@ -567,7 +566,7 @@ private theorem exists_natAbs_rowEntry_le_two_pow {ι γ : Type} {sz : ι → 
     (Nat.mul_le_mul_left c (Nat.pow_le_pow_left (Nat.add_le_add_right hy 1) d))
   exact (Nat.size_le.mp ((size_natAbs_rowEntry_le_length_encJetRows (f y) j u).trans hout)).le
 
-private theorem computableInO_snd_indexFold {ι β : Type} {encIn : ι ↪ List Bool}
+theorem computableInO_snd_indexFold {ι β : Type} {encIn : ι ↪ List Bool}
     {encB : β ↪ List Bool} {count : ι → ℕ} {initial : ι → β} {body : ℕ × β → β}
     (cn : NativeCertificate count encIn encNat) (ci : NativeCertificate initial encIn encB)
     (cb : NativeCertificate body (encPair encNat encB) encB)
diff --git a/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean
index 243d571e6..a1075f2a1 100644
--- a/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean
+++ b/Complexity/Computability/PolyTime/GreedyLabelSchedule.lean
@@ -563,15 +563,12 @@ public section
 namespace Cslib.BalancedSchedules
 
 open Finset Cslib.GenericRAM Turing.MultiTapeTM
+open ComputableTidilyInO (length_encNat_mono)
 
 private theorem length_encNat_le_self (k : ℕ) : (encNat k).length ≤ k := by
   rw [encNat_apply, Nat.size_eq_bits_len]; exact Nat.size_le_self k
 
 /-- Encoded bit-length bound for an incidence list `edges` with endpoints `< m` and `< n`. -/
-private theorem length_encNat_mono {a b : ℕ} (h : a ≤ b) :
-    (encNat a).length ≤ (encNat b).length := by
-  simpa only [encNat_apply, Nat.size_eq_bits_len] using Nat.size_le_size h
-
 theorem length_encEdges_le_of_lt {n m : ℕ} {edges : List (ℕ × ℕ)}
     (h : ∀ e ∈ edges, e.1 < m ∧ e.2 < n) :
     (encList (encPair encNat encNat) edges).length ≤
diff --git a/Complexity/Computability/PolyTime/GreedySlotScore.lean b/Complexity/Computability/PolyTime/GreedySlotScore.lean
index d3b6ce937..fbe118c49 100644
--- a/Complexity/Computability/PolyTime/GreedySlotScore.lean
+++ b/Complexity/Computability/PolyTime/GreedySlotScore.lean
@@ -85,6 +85,7 @@ normalizers `numEdges * C` or `Q * n` by `1`.
 namespace Cslib.BalancedSchedules
 
 open Finset Cslib.GenericRAM Turing.MultiTapeTM
+open ComputableTidilyInO (length_encNat_mono)
 open scoped BigOperators
 
 /-! ### Section 1: Radix-`r` candidate word decoder and bijections -/
@@ -215,10 +216,6 @@ theorem mem_candidateScheduleList {r : ℕ} (hr : 1 ≤ r) (Q : ℕ) (a : Fin Q
   rw [wordToSchedule_decodeLabelWord_eq_finFunctionFinEquiv_symm hr Q j]
   exact Equiv.symm_apply_apply _ _
 
-private theorem length_encNat_mono {a b : ℕ} (h : a ≤ b) :
-    (encNat a).length ≤ (encNat b).length := by
-  simpa only [encNat_apply, Nat.size_eq_bits_len] using Nat.size_le_size h
-
 /-- Encoded bit-length bound for any word of length `Q` with digits `< max r 1`. -/
 theorem length_encList_word_le {Q r : ℕ} {w : List ℕ} (hlen : w.length = Q)
     (hw : ∀ x ∈ w, x < max r 1) :
@@ -936,6 +933,7 @@ end
 public section
 namespace Cslib.BalancedSchedules
 open Finset Cslib.GenericRAM Turing.MultiTapeTM
+open ComputableTidilyInO (length_encNat_mono)
 
 /-- All-prefix live-state bit-length bound for the inner `IndexFold.run selectSlotStep` loop across
 every visited prefix `j ≤ r ^ Q` (never multiplying workspace by `r ^ Q`). -/
diff --git a/Complexity/Computability/PolyTime/ParityFactorEval.lean b/Complexity/Computability/PolyTime/ParityFactorEval.lean
index 6b0c8cf66..c2b9cdde7 100644
--- a/Complexity/Computability/PolyTime/ParityFactorEval.lean
+++ b/Complexity/Computability/PolyTime/ParityFactorEval.lean
@@ -1049,7 +1049,7 @@ private theorem listAppend_polytime {β : Type} {encB : β ↪ List Bool} {l r :
   (show ComputableInPolyTime (fun p : List β × List β => p.1 ++ p.2)
     (encPair (encList encB) (encList encB)) (encList encB) by fun_prop).comp (hl.prod hr)
 
-private theorem intBin_pow_polytime {base : α → ℤ} {exp : α → ℕ}
+theorem intBin_pow_polytime {base : α → ℤ} {exp : α → ℕ}
     (hb : ComputableInPolyTime base encIn encIntBin)
     (he : ComputableInPolyTime exp encIn encUnary) :
     ComputableInPolyTime (fun x => base x ^ exp x) encIn encIntBin :=
diff --git a/Complexity/Computability/PolyTime/SparseMonomialJet.lean b/Complexity/Computability/PolyTime/SparseMonomialJet.lean
index 4e2a0e9b0..8b1886fb2 100644
--- a/Complexity/Computability/PolyTime/SparseMonomialJet.lean
+++ b/Complexity/Computability/PolyTime/SparseMonomialJet.lean
@@ -945,13 +945,6 @@ open Turing MultiTapeTM MultiTapeTM.ComputableInPolyTime
 
 variable {α : Type} {encIn : α ↪ List Bool}
 
-private theorem intBin_pow_polytime {base : α → ℤ} {exp : α → ℕ}
-    (hb : ComputableInPolyTime base encIn encIntBin)
-    (he : ComputableInPolyTime exp encIn encUnary) :
-    ComputableInPolyTime (fun x => base x ^ exp x) encIn encIntBin :=
-  (show ComputableInPolyTime (fun p : ℤ × ℕ => p.1 ^ p.2)
-    (encPair encIntBin encUnary) encIntBin by fun_prop).comp (hb.prod he)
-
 private theorem intBin_sum_polytime :
     ComputableInPolyTime List.sum (encList encIntBin) encIntBin := by fun_prop