diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
index 100ae21c74..a343a0a4be 100644
--- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
+++ b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
@@ -112,7 +112,7 @@ formulas (`leafDensityRatio k N * N < ψ.length`, including `[[]]` at `N = 0`) t
 `sparseCNFDeclaredCounter` backed by `branchedPolyCounter`. -/
 def branchedSparseCNFDeclaredCounter (k N₀_leaf N₀_top N₀_branch : ℕ)
     (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) : ℕ :=
-  let N := x.1.2; let B := leafDensityRatio k N; let ψ := x.2
+  let ((_, N), ψ) := x; let B := leafDensityRatio k N
   if validDeclaredInput k N ψ && decide (B * N < ψ.length) then countCNFExhaustive (N, ψ)
   else sparseCNFDeclaredCounter Prod.snd (fun p : Unit × ℕ => leafDensityRatio k p.2)
     k (max 1 N₀_leaf) (branchedPolyCounter k N₀_top N₀_branch branchEval) x
@@ -236,7 +236,8 @@ theorem computableInPolyTime_leafDensityRatio (k : ℕ) :
 /-- **Unconditional declared-range output cap**: `branchedSparseCNFDeclaredCounter ≤ 2 ^ x.1.2`. -/
 theorem branchedSparseCNFDeclaredCounter_le_two_pow (k N₀_leaf N₀_top N₀_branch : ℕ)
     (branchEval : BranchEvalInput → ℕ) (x : (Unit × ℕ) × CNF ℕ) :
-    branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ x.1.2 := by
+    let ((_, N), _) := x
+    branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ N := by
   unfold branchedSparseCNFDeclaredCounter; dsimp only; split_ifs
   · rw [countCNFExhaustive_eq_modelCountOn_range, CNF.modelCountOn]
     refine (Finset.card_filter_le _ _).trans ?_
@@ -311,7 +312,7 @@ theorem branchedSparseCNFDeclaredCounter_exhaustive_eq_modelCountOn
     (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : CNF ℕ)
     (hw : ∀ cl ∈ ψ, cl.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) :
     branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch
-        (fun inp => countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) =
+        (fun ((n', _), _, _, eqs') => countSystemExhaustive (n', eqs')) ((c, N), ψ) =
       ψ.modelCountOn (Finset.range N) :=
   branchedSparseCNFDeclaredCounter_eq_modelCountOn
     (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub
@@ -322,7 +323,7 @@ theorem branchedSparseCNFLeafCounter_exhaustive_eq_modelCount
     (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : CNF ℕ)
     (hw : ∀ cl ∈ ψ, cl.length ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) :
     branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch
-        (fun inp => countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) =
+        (fun ((n', _), _, _, eqs') => countSystemExhaustive (n', eqs')) ((c, N), ψ) =
       ψ.modelCount :=
   branchedSparseCNFLeafCounter_eq_modelCount
     (fun n' eqs' _ => countSystemExhaustive_eq_rootCount n' eqs') c N ψ hw hsub
@@ -988,15 +989,17 @@ theorem exists_threshold_branchedSparseCNF_time_bound (k N₀_top N₀_branch :
     (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) :
     ∃ N_min : ℕ, 16384 ≤ N_min ∧ ∀ N₀_leaf : ℕ, N_min ≤ N₀_leaf →
       ∃ C_t d_t A_t : ℕ, 1 ≤ A_t ∧
-        ∀ x : (Unit × ℕ) × CNF ℕ, x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 →
-          ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
-              cBranch hbound).time x : ℝ) ≤
-            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧
-          ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
-              cBranch hbound).time x : ℝ) ≤
-            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := by
+        ∀ x : (Unit × ℕ) × CNF ℕ,
+          let ((_, N), ψ) := x
+          ψ.length ≤ leafOccBound k N * N + 1 →
+            ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
+                cBranch hbound).time x : ℝ) ≤
+              (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+                (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) ∧
+            ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
+                cBranch hbound).time x : ℝ) ≤
+              (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+                (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by
   obtain ⟨N_sys, C_sys, d_sys, A_sys, hNsys16, hSysT⟩ :=
     polySys_time_bound_of_branchPolylog k N₀_top N₀_branch cBranch hbound hbr_time
   obtain ⟨C_B, hCB⟩ := exists_leafDensityRatio_le_mul_clog_pow k; set β_B := 2 * (max 2 k - 1)
@@ -1156,15 +1159,17 @@ theorem exists_branchedSparseCNF_time_bound (k N₀_branch : ℕ)
     (hs_br : PolyBounded (fun x => (encBranchEvalInput x).length) cBranch.space)
     (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) :
     ∃ N₀_leaf N₀_top C_t d_t A_t : ℕ, 1 ≤ A_t ∧
-      ∀ x : (Unit × ℕ) × CNF ℕ, x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 →
-        ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
-            cBranch hbound).time x : ℝ) ≤
-          (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-            (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧
-        ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
-            cBranch hbound).time x : ℝ) ≤
-          (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
-            (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := by
+      ∀ x : (Unit × ℕ) × CNF ℕ,
+        let ((_, N), ψ) := x
+        ψ.length ≤ leafOccBound k N * N + 1 →
+          ((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch
+              cBranch hbound).time x : ℝ) ≤
+            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) ∧
+          ((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch
+              cBranch hbound).time x : ℝ) ≤
+            (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t *
+              (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale N) := by
   obtain ⟨N_min, _, hBound⟩ :=
     exists_threshold_branchedSparseCNF_time_bound k 0 N₀_branch cBranch hbound hs_br hbr_time
   obtain ⟨C_t, d_t, A_t, hA, hT⟩ := hBound N_min le_rfl
diff --git a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean
index e5cd7f1798..7f7c78bd9e 100644
--- a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean
+++ b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean
@@ -93,8 +93,9 @@ def IsCompiledSparseSystem (k N maxEqs maxTerms : ℕ) (sys : List (List (List 
 /-- Evaluates `polyCounter (N, compileParitySystemBounded k ψ rows)` when `rows.length ≤ 6 * N`. -/
 def compiledRowCounter (k : ℕ) (polyCounter : ℕ × List (List (List ℕ)) → ℕ)
     (q : (ℕ × CNF ℕ) × List (List Bool)) : ℕ :=
-  if decide (q.2.length ≤ 6 * q.1.1) then
-    polyCounter (q.1.1, compileParitySystemBounded k q.1.2 q.2)
+  let nψ := q.1
+  if decide (q.2.length ≤ 6 * nψ.1) then
+    polyCounter (nψ.1, compileParitySystemBounded k nψ.2 q.2)
   else 0
 
 /-- Deterministic Section 6.3 fast path: initial Tanner rows via `initialTestsRows`, `3 * N` rounds
diff --git a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean
index 5a7c62acd5..e7885b62e5 100644
--- a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean
+++ b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean
@@ -1222,7 +1222,7 @@ theorem computableInPolyTime_varDegree :
 binary, result in `encOption encNat`) is polynomial-time. -/
 theorem computableInPolyTime_findHeavyVar :
     ComputableInPolyTime
-      (fun p : (ℕ × ℕ) × List (List (List ℕ)) => findHeavyVar p.1.1 p.1.2 p.2)
+      (fun (((n, b), sys) : (ℕ × ℕ) × List (List (List ℕ))) => findHeavyVar n b sys)
       (encPair (encPair encUnary encNat) encSys) (encOption encNat) := by
   have hdeg := computableInPolyTime_varDegree
   have hrange : ComputableInPolyTime
@@ -1235,7 +1235,7 @@ theorem computableInPolyTime_findHeavyVar :
     binary_lt' ((fst _ _).fst'.snd')
       (unary_to_binary.comp (hdeg.comp ((snd _ _).prod ((fst _ _).snd'))))
   have hfind := findWithInput (test := fun x v => decide (x.1.2 < varDegree v x.2)) hrange hpred
-  refine hfind.of_enc_eq fun p => congrArg (encOption encNat) ?_
+  refine hfind.of_enc_eq fun ⟨⟨_, _⟩, _⟩ => congrArg (encOption encNat) ?_
   rw [List.map_id']; rfl
 
 @[fun_prop]
@@ -1250,9 +1250,11 @@ theorem computableInPolyTime_findHeavyVar_apply {α : Type} {encIn : α ↪ List
 /-- Substituting `x_v = val` into a sparse `𝔽₂` equation (`restrictEquation`) is polynomial-time. -/
 theorem computableInPolyTime_restrictEquation :
     ComputableInPolyTime
-      (fun p : (ℕ × Bool) × List (List ℕ) => restrictEquation p.1.1 p.1.2 p.2)
-      (encPair (encPair encNat encBool) encEq) encEq := by
-  unfold restrictEquation; fun_prop
+      (fun (((v, val), eq) : (ℕ × Bool) × List (List ℕ)) => restrictEquation v val eq)
+      (encPair (encPair encNat encBool) encEq) encEq :=
+  (by unfold restrictEquation; fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × Bool) × List (List ℕ) => restrictEquation p.1.1 p.1.2 p.2)
+      (encPair (encPair encNat encBool) encEq) encEq).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop]
 theorem computableInPolyTime_restrictEquation_apply {α : Type} {encIn : α ↪ List Bool}
@@ -1267,10 +1269,14 @@ theorem computableInPolyTime_restrictEquation_apply {α : Type} {encIn : α ↪
 /-- Substituting `x_v = val` across a sparse `𝔽₂` system (`restrictSystem`) is polynomial-time. -/
 theorem computableInPolyTime_restrictSystem :
     ComputableInPolyTime
-      (fun p : (ℕ × Bool) × List (List (List ℕ)) => restrictSystem p.1.1 p.1.2 p.2)
+      (fun (((v, val), sys) : (ℕ × Bool) × List (List (List ℕ))) => restrictSystem v val sys)
       (encPair (encPair encNat encBool) encSys) encSys :=
-  mapWithInput (snd (encPair encNat encBool) encSys)
-    (computableInPolyTime_restrictEquation.comp (((fst _ _).fst').prod (snd _ _)))
+  (mapWithInput
+    (f := fun x a =>
+      (fun (((v, val), eq) : (ℕ × Bool) × List (List ℕ)) => restrictEquation v val eq) (x.1, a))
+    (snd (encPair encNat encBool) encSys)
+    (computableInPolyTime_restrictEquation.comp (((fst _ _).fst').prod (snd _ _)))).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop]
 theorem computableInPolyTime_restrictSystem_apply {α : Type} {encIn : α ↪ List Bool}
diff --git a/Complexity/Computability/PolyTime/Int/Jet.lean b/Complexity/Computability/PolyTime/Int/Jet.lean
index 56a47d1e23..8d2710a84d 100644
--- a/Complexity/Computability/PolyTime/Int/Jet.lean
+++ b/Complexity/Computability/PolyTime/Int/Jet.lean
@@ -274,8 +274,12 @@ local notation "encJet" => encList encIntBin
   unfold add; fun_prop
 
 theorem computableInPolyTime_add :
-    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => add p.1.1 p.1.2 p.2)
-      (encPair (encPair encUnary encJet) encJet) encJet := by fun_prop
+    ComputableInPolyTime
+      (fun (((J, a), b) : (ℕ × List ℤ) × List ℤ) => add J a b)
+      (encPair (encPair encUnary encJet) encJet) encJet :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => add p.1.1 p.1.2 p.2) _ _).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop] theorem computableInPolyTime_sub' {γ : Type} {encIn : γ ↪ List Bool}
     {J : γ → ℕ} {a b : γ → List ℤ} (hJ : ComputableInPolyTime J encIn encUnary)
@@ -288,8 +292,12 @@ theorem computableInPolyTime_add :
       (((ha.comp hx).listGetDWithInput hk 0).prod ((hb.comp hx).listGetDWithInput hk 0)))
 
 theorem computableInPolyTime_sub :
-    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => sub p.1.1 p.1.2 p.2)
-      (encPair (encPair encUnary encJet) encJet) encJet := by fun_prop
+    ComputableInPolyTime
+      (fun (((J, a), b) : (ℕ × List ℤ) × List ℤ) => sub J a b)
+      (encPair (encPair encUnary encJet) encJet) encJet :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × List ℤ) × List ℤ => sub p.1.1 p.1.2 p.2) _ _).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 @[fun_prop] theorem computableInPolyTime_subConst' {γ : Type} {encIn : γ ↪ List Bool}
     {J : γ → ℕ} {c : γ → ℤ} {a : γ → List ℤ} (hJ : ComputableInPolyTime J encIn encUnary)
@@ -299,8 +307,12 @@ theorem computableInPolyTime_sub :
     ((ComputableInPolyTime.snoc encIntBin).comp ((ComputableInPolyTime.const []).prod hc)) ha
 
 theorem computableInPolyTime_subConst :
-    ComputableInPolyTime (fun p : (ℕ × ℤ) × List ℤ => subConst p.1.1 p.1.2 p.2)
-      (encPair (encPair encUnary encIntBin) encJet) encJet := by fun_prop
+    ComputableInPolyTime
+      (fun (((J, c), a) : (ℕ × ℤ) × List ℤ) => subConst J c a)
+      (encPair (encPair encUnary encIntBin) encJet) encJet :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × ℤ) × List ℤ => subConst p.1.1 p.1.2 p.2) _ _).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 /-- Plain polynomial-time combinator for folding `Cslib.mulZJet` over `xs` from
 `Cslib.truncZJet J [1]`, given a polynomial bound `K` on the bit-sizes of the step factors' `ℓ₁`
@@ -311,7 +323,7 @@ theorem computableInPolyTime_foldl_mulZJet {γ α : Type} {encIn : γ ↪ List B
     (hJ : ComputableInPolyTime J encIn encUnary) (hδ : ComputableInPolyTime δ encIn encIntBin)
     (hxs : ComputableInPolyTime xs encIn (encList encA))
     (hfac : ComputableInPolyTime
-      (fun q : ((ℕ × ℤ) × List ℤ) × α => factor q.1.1.1 q.1.1.2 q.2)
+      (fun (((J, δ), _), a) => factor J δ a)
       (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encJet)
     {K : γ → ℕ} (hK : PolyBounded (fun x => (encIn x).length) K)
     (hsz : ∀ x, ∀ a ∈ xs x,
@@ -325,7 +337,8 @@ theorem computableInPolyTime_foldl_mulZJet {γ α : Type} {encIn : γ ↪ List B
       (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encUnary := by fun_prop
   have hqAcc : ComputableInPolyTime (fun q : ((ℕ × ℤ) × List ℤ) × α => q.1.2)
       (encPair (encPair (encPair encUnary encIntBin) encJet) encA) encJet := by fun_prop
-  have hstep := Cslib.computableInPolyTime_mulZJet hqJ hqAcc hfac
+  have hstep := Cslib.computableInPolyTime_mulZJet hqJ hqAcc
+    (hfac.of_enc_eq (g := fun q => factor q.1.1.1 q.1.1.2 q.2) fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl)
   refine ComputableInPolyTime.foldlWith (encA := encA)
     (par := fun x => (J x, δ x)) (list := xs) (init := fun x => Cslib.truncZJet (J x) [1])
     (step := fun par acc a => Cslib.mulZJet par.1 acc (factor par.1 par.2 a))
diff --git a/Complexity/Computability/PolyTime/Int/Table.lean b/Complexity/Computability/PolyTime/Int/Table.lean
index 6c76fc53e9..2366285cab 100644
--- a/Complexity/Computability/PolyTime/Int/Table.lean
+++ b/Complexity/Computability/PolyTime/Int/Table.lean
@@ -174,13 +174,30 @@ theorem computableInPolyTime_rowEntry {rows : α → List (List ℤ)} {i j : α
     (((ComputableInPolyTime.listGetD (encA := encList encIntBin) []).comp
       (hrows.prod hi)).prod hj))
 
+/-- Input triple `((x, i), j)` for `computableInPolyTime_tabulateTable`: outer context `x`, row
+index `i`, and column index `j`. -/
+abbrev TableIndex (α : Type) : Type := (α × ℕ) × ℕ
+
+/-- Context-and-row pair `(x, i)` of a `TableIndex`. -/
+abbrev TableIndex.rowCtx (p : TableIndex α) : α × ℕ := p.1
+
+/-- Outer context `x` of a `TableIndex`. -/
+abbrev TableIndex.ctx (p : TableIndex α) : α := p.rowCtx.1
+
+/-- Row index `i` of a `TableIndex`. -/
+abbrev TableIndex.row (p : TableIndex α) : ℕ := p.rowCtx.2
+
+/-- Column index `j` of a `TableIndex`. -/
+abbrev TableIndex.col (p : TableIndex α) : ℕ := p.2
+
 /-- Tabulating an `r × c` table of binary integers from unary dimensions `(r, c)` is computable
 in polynomial time. -/
 @[fun_prop]
 theorem computableInPolyTime_tabulateTable {r c : α → ℕ} {g : α → ℕ → ℕ → ℤ}
     (hr : ComputableInPolyTime r encIn encUnary)
     (hc : ComputableInPolyTime c encIn encUnary)
-    (hg : ComputableInPolyTime (fun p : (α × ℕ) × ℕ => g p.1.1 p.1.2 p.2)
+    (hg : ComputableInPolyTime
+      (fun p : TableIndex α => g p.ctx p.row p.col)
       (encPair (encPair encIn encUnary) encUnary) encIntBin) :
     ComputableInPolyTime (fun x => tabulateTable (r x) (c x) (g x))
       encIn (encList (encList encIntBin)) :=
diff --git a/Complexity/Computability/PolyTime/JetArray.lean b/Complexity/Computability/PolyTime/JetArray.lean
index 4c9cb52f7f..4cc7db998d 100644
--- a/Complexity/Computability/PolyTime/JetArray.lean
+++ b/Complexity/Computability/PolyTime/JetArray.lean
@@ -918,54 +918,89 @@ theorem zeroJet_polytime :
 
 /-- Direct polynomial-time certificate for `constJet`. -/
 theorem constJet_polytime :
-    ComputableInPolyTime (fun p : (ℕ × ℕ) × ℤ => constJet p.1.1 p.1.2 p.2)
-      (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)) := by fun_prop
+    ComputableInPolyTime
+      (fun (((J, ℓ), c) : (ℕ × ℕ) × ℤ) => constJet J ℓ c)
+      (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × ℕ) × ℤ => constJet p.1.1 p.1.2 p.2) _ _).of_enc_eq
+    fun ⟨⟨_, _⟩, _⟩ => rfl
 
 /-- Direct polynomial-time certificate for `addJet`. -/
 theorem addJet_polytime :
     ComputableInPolyTime
-      (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => addJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      (fun ((((J, ℓ), a), b) : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => addJet J ℓ a b)
       (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin)))
-        (encList (encList encIntBin))) (encList (encList encIntBin)) := by fun_prop
+        (encList (encList encIntBin))) (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime
+      (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => addJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      _ _).of_enc_eq
+    fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl
 
 /-- Direct polynomial-time certificate for `negJet`. -/
 theorem negJet_polytime :
-    ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => negJet p.1.1 p.1.2 p.2)
+    ComputableInPolyTime
+      (fun (((J, ℓ), a) : (ℕ × ℕ) × List (List ℤ)) => negJet J ℓ a)
       (encPair (encPair encUnary encUnary) (encList (encList encIntBin)))
-      (encList (encList encIntBin)) := by fun_prop
+      (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => negJet p.1.1 p.1.2 p.2)
+      _ _).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl
 
 /-- Direct polynomial-time certificate for `subJet`. -/
 theorem subJet_polytime :
     ComputableInPolyTime
-      (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => subJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      (fun ((((J, ℓ), a), b) : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => subJet J ℓ a b)
       (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin)))
-        (encList (encList encIntBin))) (encList (encList encIntBin)) := by fun_prop
+        (encList (encList encIntBin))) (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime
+      (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => subJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      _ _).of_enc_eq
+    fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl
 
 /-- Direct polynomial-time certificate for `smulJet`. -/
 theorem smulJet_polytime :
     ComputableInPolyTime
-      (fun p : ((ℕ × ℕ) × ℤ) × List (List ℤ) => smulJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      (fun ((((J, ℓ), c), a) : ((ℕ × ℕ) × ℤ) × List (List ℤ)) => smulJet J ℓ c a)
       (encPair (encPair (encPair encUnary encUnary) encIntBin) (encList (encList encIntBin)))
-      (encList (encList encIntBin)) := by fun_prop
+      (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime
+      (fun p : ((ℕ × ℕ) × ℤ) × List (List ℤ) => smulJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      _ _).of_enc_eq fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl
 
 /-- Direct polynomial-time certificate for `shiftZJet`. -/
 theorem shiftZJet_polytime :
-    ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftZJet p.1.1 p.1.2 p.2)
+    ComputableInPolyTime
+      (fun (((J, ℓ), a) : (ℕ × ℕ) × List (List ℤ)) => shiftZJet J ℓ a)
       (encPair (encPair encUnary encUnary) (encList (encList encIntBin)))
-      (encList (encList encIntBin)) := by fun_prop
+      (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftZJet p.1.1 p.1.2 p.2)
+      _ _).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl
 
 /-- Direct polynomial-time certificate for `shiftVJet`. -/
 theorem shiftVJet_polytime :
-    ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftVJet p.1.1 p.1.2 p.2)
+    ComputableInPolyTime
+      (fun (((J, ℓ), a) : (ℕ × ℕ) × List (List ℤ)) => shiftVJet J ℓ a)
       (encPair (encPair encUnary encUnary) (encList (encList encIntBin)))
-      (encList (encList encIntBin)) := by fun_prop
+      (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime (fun p : (ℕ × ℕ) × List (List ℤ) => shiftVJet p.1.1 p.1.2 p.2)
+      _ _).of_enc_eq fun ⟨⟨_, _⟩, _⟩ => rfl
 
 /-- Direct polynomial-time certificate for `convJet`. -/
 theorem convJet_polytime :
     ComputableInPolyTime
-      (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => convJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      (fun ((((J, ℓ), a), b) : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ)) => convJet J ℓ a b)
       (encPair (encPair (encPair encUnary encUnary) (encList (encList encIntBin)))
-        (encList (encList encIntBin))) (encList (encList encIntBin)) := by fun_prop
+        (encList (encList encIntBin))) (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime
+      (fun p : ((ℕ × ℕ) × List (List ℤ)) × List (List ℤ) => convJet p.1.1.1 p.1.1.2 p.1.2 p.2)
+      _ _).of_enc_eq
+    fun ⟨⟨⟨_, _⟩, _⟩, _⟩ => rfl
 
 end PolyTime
 
diff --git a/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean b/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean
index d42c1b4b83..f141d3b6c6 100644
--- a/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean
+++ b/Complexity/Computability/PolyTime/LinearAlgebra/ReplacementDesignBuilder.lean
@@ -523,10 +523,12 @@ def ReplacementDesignData.equivTuple : ReplacementDesignData ≃ ReplacementDesi
   toFun d := ((d.varGroups, d.factorGroups, d.incidences),
     (d.copyCount, d.placements, d.measurementMatrix),
     (d.groupMeasurementMatrices, d.denom, d.replacementRows))
-  invFun t :=
-    { varGroups := t.1.1, factorGroups := t.1.2.1, incidences := t.1.2.2,
-      copyCount := t.2.1.1, placements := t.2.1.2.1, measurementMatrix := t.2.1.2.2,
-      groupMeasurementMatrices := t.2.2.1, denom := t.2.2.2.1, replacementRows := t.2.2.2.2 }
+  invFun := fun ((varGroups, factorGroups, incidences),
+      (copyCount, placements, measurementMatrix),
+      (groupMeasurementMatrices, denom, replacementRows)) =>
+    { varGroups, factorGroups, incidences,
+      copyCount, placements, measurementMatrix,
+      groupMeasurementMatrices, denom, replacementRows }
   left_inv d := by cases d; rfl
   right_inv _ := rfl
 
diff --git a/Complexity/Computability/PolyTime/ParityFactorEval.lean b/Complexity/Computability/PolyTime/ParityFactorEval.lean
index c2b9cdde7f..2d33391169 100644
--- a/Complexity/Computability/PolyTime/ParityFactorEval.lean
+++ b/Complexity/Computability/PolyTime/ParityFactorEval.lean
@@ -136,7 +136,8 @@ def polyMul (p q : List ℤ) : List ℤ := mulZJet (p.length + q.length) p q
 
 /-- Single Horner-division step for monic division by $Y^2 - Y$. -/
 def ParityFactorEval.divModByHStep (state : List ℤ × (ℤ × ℤ)) (c : ℤ) : List ℤ × (ℤ × ℤ) :=
-  (state.2.2 :: state.1, (c, state.2.1 + state.2.2))
+  let ab := state.2
+  (ab.2 :: state.1, (c, ab.1 + ab.2))
 
 /-- Monic division of `p` by $h(Y) = Y^2 - Y$ with linear remainder `(a, b)`. -/
 def divModByH (p : List ℤ) : List ℤ × (ℤ × ℤ) :=
@@ -231,9 +232,10 @@ theorem polyNorm1_polyMul_le (p q : List ℤ) :
 
 /-- Polynomial division identity for `divModByH` dividing by $X^2 - X$. -/
 theorem ofCoeffList_divModByH (p : List ℤ) :
+    let rem := (divModByH p).2
     ofCoeffList p =
       ofCoeffList (divModByH p).1 * (X ^ 2 - X) +
-        (C (divModByH p).2.1 + C (divModByH p).2.2 * X) := by
+        (C rem.1 + C rem.2 * X) := by
   induction p with
   | nil => simp only [divModByH, List.reverse_nil, List.foldl_nil, ofCoeffList_nil, zero_mul,
       map_zero, add_zero]
@@ -269,7 +271,8 @@ private lemma foldl_divModByHStep_bounds (w : List ℤ) :
 
 /-- Linear remainder magnitude bound for `divModByH` ([OpenAI2026ETH], Lemma B.1). -/
 theorem natAbs_divModByH_snd_le (p : List ℤ) :
-    (divModByH p).2.1.natAbs ≤ polyNorm1 p ∧ (divModByH p).2.2.natAbs ≤ polyNorm1 p := by
+    let rem := (divModByH p).2
+    rem.1.natAbs ≤ polyNorm1 p ∧ rem.2.natAbs ≤ polyNorm1 p := by
   have h := (foldl_divModByHStep_bounds p.reverse).2.1; rw [polyNorm1_reverse] at h
   change (divModByH p).2.1.natAbs + (divModByH p).2.2.natAbs ≤ polyNorm1 p at h; omega
 
@@ -283,8 +286,9 @@ theorem polyNorm1_divModByH_fst_le (p : List ℤ) :
 /-- `divModByH` computes the exact monic quotient and remainder on division by
 `Polynomial.hPoly = X ^ 2 - X`. -/
 theorem divByMonic_and_modByMonic_hPoly_ofCoeffList (p : List ℤ) :
+    let rem := (divModByH p).2
     ofCoeffList p /ₘ hPoly = ofCoeffList (divModByH p).1 ∧
-      ofCoeffList p %ₘ hPoly = C (divModByH p).2.1 + C (divModByH p).2.2 * X := by
+      ofCoeffList p %ₘ hPoly = C rem.1 + C rem.2 * X := by
   refine div_modByMonic_unique _ _ monic_hPoly ⟨?_, ?_⟩
   · rw [hPoly, ofCoeffList_divModByH p]; ring
   · have hr : C (divModByH p).2.1 + C (divModByH p).2.2 * X =
@@ -1341,9 +1345,13 @@ private theorem parityFactorCols_polytime {J ℓ : α → ℕ} {Δ : α → ℤ}
 and binary $(\Delta, \text{yJet})$. -/
 theorem evalParityFactorJet_polytime :
     ComputableInPolyTime
-      (fun p : (ℕ × ℕ) × (ℤ × List ℤ) => evalParityFactorJet p.1.1 p.1.2 p.2.1 p.2.2)
+      (fun (((J, ℓ), (Δ, yJet)) : (ℕ × ℕ) × (ℤ × List ℤ)) => evalParityFactorJet J ℓ Δ yJet)
       (encPair (encPair encUnary encUnary) (encPair encIntBin (encList encIntBin)))
-      (encList (encList encIntBin)) := by fun_prop
+      (encList (encList encIntBin)) :=
+  (by fun_prop :
+    ComputableInPolyTime
+      (fun p : (ℕ × ℕ) × (ℤ × List ℤ) => evalParityFactorJet p.1.1 p.1.2 p.2.1 p.2.2)
+      _ _).of_enc_eq fun ⟨⟨_, _⟩, _, _⟩ => rfl
 
 end PolyTime