diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildEntries.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildEntries.lean
index bb3b4b2d1..985186911 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildEntries.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildEntries.lean
@@ -15,7 +15,7 @@ import Mathlib.Data.List.GetD
 # The entries of the child networks from their descriptors
 
 A child network of the contraction recursion of [OpenAI2026ETH] (`ModeSplitting.child`, §D.4.6,
-p. 63) is carried natively as a network of vertex descriptors (`VertexDesc`) with port lists. This
+p. 63) is carried natively as a network of vertex descriptors (`VertexDesc T`) with port lists. This
 file proves that such a network has the contraction of the child, once each descriptor reads its
 ports in the right order.
 
@@ -230,7 +230,8 @@ valuation `i < a`, `L = 2 ^ a` slots, `2 ^ (i + 1)` tiles and `p` exponents per
 of `q` against `g`, an interpolation value mapping to `ζ`, and the dense exponents of `β` at `q`.
 Then along a ring map `ψ` from `A_p`, at the packet's precision, to `R`, the descriptor's entry at
 the bits on its ports is the child's entry. -/
-theorem map_val_entry_child_inr [DecidableEq V] (β : P × Fin (2 ^ (i + 1)) × Fin p → ℕ) (g : G)
+theorem map_val_entry_child_inr [DecidableEq V] {T : Type} {ev : T → List Bool → List ℕ}
+    (β : P × Fin (2 ^ (i + 1)) × Fin p → ℕ) (g : G)
     (q : P)
     (cs : List ({e // (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti
         hti').group (N.src e) = g} ⊕
@@ -246,7 +247,7 @@ theorem map_val_entry_child_inr [DecidableEq V] (β : P × Fin (2 ^ (i + 1)) ×
         (N.src e) = g} ⊕
       {e // (cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').group
         (N.tgt e) = g} → Bool) :
-    ψ (val c.p c.fl (VertexDesc.entry
+    ψ (val c.p c.fl (VertexDesc.entry ev
         (.inr (c, cs.map fun e => (e.isLeft, slot (Sum.elim Subtype.val Subtype.val e)), βd))
         (cs.map y))) =
       ((cauchyModeSplitting side hsrc htgt horient hslot hia κ ζ hp ht hti hti').child β g).tensor
@@ -257,10 +258,10 @@ theorem map_val_entry_child_inr [DecidableEq V] (β : P × Fin (2 ^ (i + 1)) ×
     intro x hx
     obtain ⟨e, -, rfl⟩ := List.mem_map.mp hx
     exact hslot _
-  have key := VertexDesc.map_val_entry_inr (c, cs.map fun e => (e.isLeft,
+  have key := VertexDesc.map_val_entry_inr ev (c, cs.map fun e => (e.isLeft,
     slot (Sum.elim Subtype.val Subtype.val e)), βd) (cs.map y) ψ hp κ hL hia htiles ht hti hti'
     hports
-  have hgoal : ψ (val c.p c.fl (VertexDesc.entry (.inr (c, cs.map fun e => (e.isLeft,
+  have hgoal : ψ (val c.p c.fl (VertexDesc.entry ev (.inr (c, cs.map fun e => (e.isLeft,
     slot (Sum.elim Subtype.val Subtype.val e)), βd)) (cs.map y))) = _ := key
   rw [hgoal]
   dsimp only
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean
index 62bfd5130..d998f60fc 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/DescribedLift.lean
@@ -24,7 +24,7 @@ import Mathlib.Data.List.Sort
 
 The contraction recursion of [OpenAI2026ETH] (§D.4, pp. 57–64) is proved correct over the valuation
 ring `O = ℤ_(2)[U] / (f)`, while the native algorithm carries networks of descriptors
-(`DescribedNetwork VertexDesc`) and computes with coefficient lists in
+(`DescribedNetwork (VertexDesc T)`) and computes with coefficient lists in
 `A_p = (ℤ / 2 ^ p)[U] / (f)`. This file gives the network over `O` that a described network stands
 for.
 
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean
index aab15a930..71713d2ae 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContraction.lean
@@ -22,17 +22,19 @@ import Mathlib.Data.List.GetD
 
 The recursion of Theorem D.1 of [OpenAI2026ETH] (Appendix D.4.7, p. 64), as a depth-first stack
 recursion (`Cslib.GenericRAM.StackRecursion.Scheme`) over *calls*. A call
-(`FastContraction.Call`) is a described network (`DescribedNetwork VertexDesc`) whose first `r`
-vertices are its rows, with the schedule's scale `s` (the number of edges of the root, since the
-machine sees no other size), its depth `d`, an edge bound, its precision `p` and the coefficients
-`fl` of the modulus `f`.
+(`FastContraction.Call T`) is a described network (`DescribedNetwork (VertexDesc T)`) whose first
+`r` vertices are its rows, with the schedule's scale `s` (the number of edges of the root, since
+the machine sees no other size), its depth `d`, an edge bound, its precision `p` and the
+coefficients `fl` of the modulus `f`. The vertices of the input network have descriptors of a type
+`T`, read by an entry procedure `ev : T → List Bool → List ℕ` (`VertexDesc.entry ev`); only the
+leaves and the correctness statement read them, so the recursion is the same for every `T`.
 
 **Active calls and leaves.** A call with `M` edges is *active* (`FastContraction.active`) when the
 schedule makes it an active call (`ContractionSchedule.callParams`, with `a = slotBits s d`,
 `u = taper s d` and `h = ⌈3 M / u⌉`), its parameters satisfy the hypotheses of Lemma D.5, its
 degrees are at most `degreeBound s`, the `M (2 L - 1) + 1` interpolation points are distinct
 residues (`n ≤ 2 ^ e` for `e = deg f`), and `M` is below its edge bound. Every other call is a leaf,
-evaluated by direct summation over the coefficient lists of `A_p` (`FastContraction.leafValue`).
+evaluated by direct summation over the coefficient lists of `A_p` (`FastContraction.leafValue ev`).
 A child receives its parent's number of edges as its bound, so the recursion terminates, as
 `TensorNetwork.contractRec` does; a child that is not smaller is a leaf.
 
@@ -93,13 +95,15 @@ open GaloisRingArith ChildCursor NativeRecovery ContractionSchedule NativeChild
 coefficients `fl` of the modulus and the number `r` of rows. -/
 abbrev Params : Type := ℕ × ℕ × ℕ × ℕ × List ℕ × ℕ
 
-/-- **A call** of the recursion: its parameters and its network, whose first `r` vertices are its
-rows. -/
-abbrev Call : Type := Params × DescribedNetwork VertexDesc
+/-- **A call** of the recursion: its parameters and its network over root descriptors `T`, whose
+first `r` vertices are its rows. -/
+abbrev Call (T : Type) : Type := Params × DescribedNetwork (VertexDesc T)
+
+variable {T : Type}
 
 namespace Call
 
-variable (x : Call)
+variable (x : Call T)
 
 /-- The scale `s` of the schedule. -/
 abbrev scale : ℕ := x.1.1
@@ -114,7 +118,7 @@ abbrev fl : List ℕ := x.1.2.2.2.2.1
 /-- The number of rows. -/
 abbrev rows : ℕ := x.1.2.2.2.2.2
 /-- The network. -/
-abbrev net : DescribedNetwork VertexDesc := x.2
+abbrev net : DescribedNetwork (VertexDesc T) := x.2
 /-- The number `M` of edges. -/
 abbrev edges : ℕ := x.2.numEdges
 
@@ -122,7 +126,9 @@ end Call
 
 /-! ### The data of a call -/
 
-variable (x : Call)
+variable (ev : T → List Bool → List ℕ)
+
+variable (x : Call T)
 
 /-- The packets have `2 ^ a` slots, `a = slotBits s d`. -/
 @[expose] def slots : ℕ := slotBits x.scale x.depth
@@ -145,7 +151,7 @@ points are distinct residues (`n ≤ 2 ^ e`), and it has fewer edges than its bo
     x.edges < x.bound)
 
 /-- An active call has fewer edges than its bound. -/
-theorem edges_lt_bound_of_active {x : Call} (h : active x = true) : x.edges < x.bound := by
+theorem edges_lt_bound_of_active {x : Call T} (h : active x = true) : x.edges < x.bound := by
   simp only [active, decide_eq_true_eq] at h
   exact h.2.2.2.2.2.2
 
@@ -169,7 +175,7 @@ of rows is stored in binary and the packing lists one word per row. -/
 @[expose] def rowCap : ℕ := min x.rows x.net.vertices.length
 
 /-- The cap on the rows is inactive when there are at most as many rows as vertices. -/
-theorem rowCap_eq {x : Call} (h : x.rows ≤ x.net.vertices.length) : rowCap x = x.rows :=
+theorem rowCap_eq {x : Call T} (h : x.rows ≤ x.net.vertices.length) : rowCap x = x.rows :=
   min_eq_left h
 
 /-- **The packing of Lemma D.3**, natively (`nativeParentPacking`, `r = 64`), with the rows
@@ -179,7 +185,7 @@ capped (`FastContraction.rowCap`). -/
 
 /-- The packing is the native packing of the rows when there are at most as many rows as
 vertices. -/
-theorem packing_eq {x : Call} (h : x.rows ≤ x.net.vertices.length) :
+theorem packing_eq {x : Call T} (h : x.rows ≤ x.net.vertices.length) :
     packing x = nativeParentPacking x.rows (slots x) x.net := by
   rw [packing, rowCap_eq h]
 
@@ -226,16 +232,16 @@ the stored values. -/
 
 /-- **The value of a leaf**: direct summation in `A_p`. -/
 @[expose] def leafValue : List ℕ :=
-  DescribedNetwork.sumValue SumOps.galois VertexDesc.entry (x.prec, x.fl) x.net
+  DescribedNetwork.sumValue SumOps.galois (VertexDesc.entry ev) (x.prec, x.fl) x.net
 
 /-! ### The scheme -/
 
-variable (mk : Call → State → ℕ × DescribedNetwork VertexDesc)
+variable (mk : Call T → State → ℕ × DescribedNetwork (VertexDesc T))
 
 /-- **The child call** at a cursor state `c = (i, k, β, g)`: the rows and the network given by the
 child builder `mk`, at depth `d + 1`, with the parent's number of edges as its bound and the
 node's precision `p_i`. -/
-@[expose] def child (c : State) : Call :=
+@[expose] def child (c : State) : Call T :=
   ((x.scale, x.depth + 1, x.edges, nodePrec x c.1, x.fl, (mk x c).1), (mk x c).2)
 
 /-- The accumulator of a call: the cursor state of the next child, if any, and the accumulator of
@@ -243,9 +249,9 @@ the cursor. -/
 abbrev Frame : Type := Option State × Acc (List ℕ)
 
 /-- **The recursion as a stack recursion**, with values tagged by the depth. -/
-@[expose] def scheme : Scheme Call Frame (ℕ × List ℕ) where
+@[expose] def scheme : Scheme (Call T) Frame (ℕ × List ℕ) where
   isLeaf x := !active x
-  leaf x := (x.depth, leafValue x)
+  leaf x := (x.depth, leafValue ev x)
   start x := (some (cursorStart (weights x)), (one x.fl, zero x.fl, []))
   next x a := a.1.map (child x mk)
   absorb x a y := match a.1 with
@@ -257,18 +263,19 @@ abbrev Frame : Type := Option State × Acc (List ℕ)
 
 /-- **The value of a call**, by well-founded recursion on the edge bound: the leaf value, or the
 recovery from the values of the children. -/
-@[expose] def value (x : Call) : List ℕ :=
+@[expose] def value (x : Call T) : List ℕ :=
   if _h : active x = true then
     finishValue x (runLoop x fun c => value (child x mk c))
-  else leafValue x
+  else leafValue ev x
 termination_by x.bound
 decreasing_by exact edges_lt_bound_of_active _h
 
-theorem value_of_active {x : Call} (h : active x = true) :
-    value mk x = finishValue x (runLoop x fun c => value mk (child x mk c)) := by
+theorem value_of_active {x : Call T} (h : active x = true) :
+    value ev mk x = finishValue x (runLoop x fun c => value ev mk (child x mk c)) := by
   rw [value, dite_eq_left h]
 
-theorem value_of_not_active {x : Call} (h : active x = false) : value mk x = leafValue x := by
+theorem value_of_not_active {x : Call T} (h : active x = false) :
+    value ev mk x = leafValue ev x := by
   rw [value, dite_eq_right (by simp [h])]
 
 /-! ### Derivations -/
@@ -370,12 +377,12 @@ values `vals` of the earlier children absorbed. -/
 
 /-- **The loop of an active call walks its children**: from `start`, the `c`-th frame asks for the
 child at the `c`-th cursor state, absorbing it gives the next frame, and the last frame stops. -/
-theorem walk {x : Call} (h : active x = true) (vals : State → List ℕ) :
-    frameAt x vals 0 = (scheme mk).start x ∧
-      (∀ c < (children x).length, (scheme mk).next x (frameAt x vals c) =
+theorem walk {x : Call T} (h : active x = true) (vals : State → List ℕ) :
+    frameAt x vals 0 = (scheme ev mk).start x ∧
+      (∀ c < (children x).length, (scheme ev mk).next x (frameAt x vals c) =
         some (child x mk ((children x).getD c (0, 0, [], 0)))) ∧
-      (scheme mk).next x (frameAt x vals (children x).length) = none ∧
-      (∀ c < (children x).length, (scheme mk).absorb x (frameAt x vals c)
+      (scheme ev mk).next x (frameAt x vals (children x).length) = none ∧
+      (∀ c < (children x).length, (scheme ev mk).absorb x (frameAt x vals c)
         (x.depth + 1, vals ((children x).getD c (0, 0, [], 0))) = frameAt x vals (c + 1)) ∧
       runLoop x vals = (frameAt x vals (children x).length).2 := by
   have hM := one_le_edges_of_active h
@@ -406,34 +413,35 @@ theorem walk {x : Call} (h : active x = true) (vals : State → List ℕ) :
 
 /-- The invariant of the derivation from a root `x₀` at depth `0`: the only node at depth `0` is
 the root, and a value tagged `0` is the root's value. -/
-@[expose] def inv (x₀ : Call) : Invariant Call Frame (ℕ × List ℕ) :=
-  ⟨fun x => x.depth = 0 → x = x₀, fun _ _ => True, fun y => y.1 = 0 → y.2 = value mk x₀⟩
+@[expose] def inv (x₀ : Call T) : Invariant (Call T) Frame (ℕ × List ℕ) :=
+  ⟨fun x => x.depth = 0 → x = x₀, fun _ _ => True, fun y => y.1 = 0 → y.2 = value ev mk x₀⟩
 
 /-- **Derivations of the values.** Every call satisfying the invariant of a root `x₀` has a
 derivation of its tagged value. -/
-theorem exists_eval (x₀ : Call) (x : Call) (hx : (inv mk x₀).node x) :
-    ∃ n h, (scheme mk).Eval (inv mk x₀) x (x.depth, value mk x) n h := by
-  refine Scheme.exists_eval_of_measure (R := scheme mk) (I := inv mk x₀) Call.bound
-    (fun x => (x.depth, value mk x)) (fun x _ hl => ?_) (fun x _ hl => ?_) (fun x hx h0 => ?_) x hx
+theorem exists_eval (x₀ : Call T) (x : Call T) (hx : (inv ev mk x₀).node x) :
+    ∃ n h, (scheme ev mk).Eval (inv ev mk x₀) x (x.depth, value ev mk x) n h := by
+  refine Scheme.exists_eval_of_measure (R := scheme ev mk) (I := inv ev mk x₀) Call.bound
+    (fun x => (x.depth, value ev mk x)) (fun x _ hl => ?_) (fun x _ hl => ?_)
+    (fun x hx h0 => ?_) x hx
   · have hl' : active x = false := by simpa [scheme] using hl
-    simp [scheme, value_of_not_active mk hl']
+    simp [scheme, value_of_not_active ev mk hl']
   · have hl' : active x = true := by simpa [scheme] using hl
-    obtain ⟨h0, hnext, hdone, habs, hfin⟩ := walk mk hl' fun c => value mk (child x mk c)
-    refine ⟨(children x).length, frameAt x fun c => value mk (child x mk c),
+    obtain ⟨h0, hnext, hdone, habs, hfin⟩ := walk ev mk hl' fun c => value ev mk (child x mk c)
+    refine ⟨(children x).length, frameAt x fun c => value ev mk (child x mk c),
       fun c => child x mk ((children x).getD c (0, 0, [], 0)), h0, hnext, hdone,
       fun c hc => habs c hc,
       fun c _ => ⟨trivial, fun h => absurd h (by simp [child]), edges_lt_bound_of_active hl'⟩, ?_⟩
     simp only [scheme, Prod.mk.injEq, true_and]
-    rw [value_of_active mk hl', hfin]
+    rw [value_of_active ev mk hl', hfin]
   · simp only at h0
     rw [hx h0]
 
 /-- **A tagged value returned by the run is the root's value**, for any fuel: if the root is at
 depth `0` and the run returns `(0, y)`, then `y` is the value of the root. -/
-theorem eq_value_of_run {J : Type} {fuel : J → ℕ} {root : J → Call} {a : J} {y : List ℕ}
-    (hroot : (root a).depth = 0) (hrun : (scheme mk).run fuel root a = some (0, y)) :
-    y = value mk (root a) := by
-  obtain ⟨n, h, he⟩ := exists_eval mk (root a) (root a) fun _ => rfl
+theorem eq_value_of_run {J : Type} {fuel : J → ℕ} {root : J → Call T} {a : J} {y : List ℕ}
+    (hroot : (root a).depth = 0) (hrun : (scheme ev mk).run fuel root a = some (0, y)) :
+    y = value ev mk (root a) := by
+  obtain ⟨n, h, he⟩ := exists_eval ev mk (root a) (root a) fun _ => rfl
   rw [hroot] at he
   exact Scheme.value_of_run_eq_some he hrun rfl
 
@@ -527,30 +535,30 @@ theorem val_table_runLoop (h : active x = true) (vals : State → List ℕ) {j :
 /-- **The correctness of one active call** for a well-formedness predicate `WF`: at a well-formed
 active call, if the values `vals` of the children are their contractions in `A_{p_i}`, then the
 recovered value is the contraction of the call's network in `A_p`. -/
-@[expose] def StepCorrect (WF : Call → Prop) : Prop :=
+@[expose] def StepCorrect (WF : Call T → Prop) : Prop :=
   ∀ x, WF x → active x = true → ∀ vals : State → List ℕ,
     (∀ c ∈ children x, val (nodePrec x c.1) x.fl (vals c) =
-      (mk x c).2.contraction fun t bs => val (nodePrec x c.1) x.fl (VertexDesc.entry t bs)) →
+      (mk x c).2.contraction fun t bs => val (nodePrec x c.1) x.fl (VertexDesc.entry ev t bs)) →
     val x.prec x.fl (finishValue x (runLoop x vals)) =
-      x.net.contraction fun t bs => val x.prec x.fl (VertexDesc.entry t bs)
+      x.net.contraction fun t bs => val x.prec x.fl (VertexDesc.entry ev t bs)
 
 /-- **Well-formedness passes to the children** of an active call. -/
-@[expose] def WFChildren (WF : Call → Prop) : Prop :=
+@[expose] def WFChildren (WF : Call T → Prop) : Prop :=
   ∀ x, WF x → active x = true → ∀ c ∈ children x, WF (child x mk c)
 
 /-- **Correctness of the recursion.** If the step of an active call is correct and
 well-formedness passes to the children, every well-formed call computes the contraction of its
 network in `A_p`. -/
-theorem val_value {WF : Call → Prop} (hstep : StepCorrect mk WF) (hwf : WFChildren mk WF)
-    (x : Call) (hx : WF x) :
-    val x.prec x.fl (value mk x) =
-      x.net.contraction fun t bs => val x.prec x.fl (VertexDesc.entry t bs) := by
+theorem val_value {WF : Call T → Prop} (hstep : StepCorrect ev mk WF) (hwf : WFChildren mk WF)
+    (x : Call T) (hx : WF x) :
+    val x.prec x.fl (value ev mk x) =
+      x.net.contraction fun t bs => val x.prec x.fl (VertexDesc.entry ev t bs) := by
   induction hb : x.bound using Nat.strong_induction_on generalizing x with
   | _ b ih =>
   cases ha : active x
-  · rw [value_of_not_active mk ha]
-    exact DescribedNetwork.val_sumValue_galois VertexDesc.entry (x.prec, x.fl) x.net
-  · rw [value_of_active mk ha]
+  · rw [value_of_not_active ev mk ha]
+    exact DescribedNetwork.val_sumValue_galois (VertexDesc.entry ev) (x.prec, x.fl) x.net
+  · rw [value_of_active ev mk ha]
     refine hstep x hx ha _ fun c hc => ?_
     exact ih _ (hb ▸ edges_lt_bound_of_active ha) (child x mk c) (hwf x hx ha c hc) rfl
 
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionDerivation.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionDerivation.lean
index 7d1f9b0e8..fdf577631 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionDerivation.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionDerivation.lean
@@ -58,43 +58,44 @@ namespace Cslib.Circuits.Frontier.FastContraction
 
 open ChildCursor Cslib.GenericRAM Cslib.GenericRAM.StackRecursion
 
-variable (mk : Call → State → ℕ × DescribedNetwork VertexDesc)
+variable {T : Type} (ev : T → List Bool → List ℕ)
+  (mk : Call T → State → ℕ × DescribedNetwork (VertexDesc T))
 
 /-- **The calls reached from a root** `x₀`: the root, and the children of reached active calls. -/
-inductive Reach (x₀ : Call) : Call → Prop
+inductive Reach (x₀ : Call T) : Call T → Prop
   /-- The root is reached. -/
   | root : Reach x₀ x₀
   /-- The children of a reached active call are reached. -/
-  | step {x : Call} (c : State) : Reach x₀ x → active x = true → c ∈ children x →
+  | step {x : Call T} (c : State) : Reach x₀ x → active x = true → c ∈ children x →
       Reach x₀ (child x mk c)
 
 /-- **The invariant of the derivations from a root** `x₀`: the reached calls, the frames of reached
 active calls along their children, and the tagged values of reached calls. -/
-@[expose] def reachInv (x₀ : Call) : Invariant Call Frame (ℕ × List ℕ) where
+@[expose] def reachInv (x₀ : Call T) : Invariant (Call T) Frame (ℕ × List ℕ) where
   node := Reach mk x₀
   frame x a := Reach mk x₀ x ∧ active x = true ∧
-    ∃ c ≤ (children x).length, a = frameAt x (fun c => value mk (child x mk c)) c
-  value y := ∃ x, Reach mk x₀ x ∧ y = (x.depth, value mk x)
+    ∃ c ≤ (children x).length, a = frameAt x (fun c => value ev mk (child x mk c)) c
+  value y := ∃ x, Reach mk x₀ x ∧ y = (x.depth, value ev mk x)
 
-variable {mk} {x₀ : Call}
+variable {ev mk} {x₀ : Call T}
 
 namespace Reach
 
 /-- Reached calls keep the scale of the root. -/
-theorem scale_eq {x : Call} (h : Reach mk x₀ x) : x.scale = x₀.scale := by
+theorem scale_eq {x : Call T} (h : Reach mk x₀ x) : x.scale = x₀.scale := by
   induction h with
   | root => rfl
   | step c _ _ _ ih => exact ih
 
 /-- Reached calls keep the modulus of the root. -/
-theorem fl_eq {x : Call} (h : Reach mk x₀ x) : x.fl = x₀.fl := by
+theorem fl_eq {x : Call T} (h : Reach mk x₀ x) : x.fl = x₀.fl := by
   induction h with
   | root => rfl
   | step c _ _ _ ih => exact ih
 
 /-- **The bound plus the depth does not increase** along the recursion: a child's bound is its
 parent's number of edges, which is below the parent's bound at an active call. -/
-theorem bound_add_depth_le {x : Call} (h : Reach mk x₀ x) :
+theorem bound_add_depth_le {x : Call T} (h : Reach mk x₀ x) :
     x.bound + x.depth ≤ x₀.bound + x₀.depth := by
   induction h with
   | root => exact le_rfl
@@ -106,7 +107,7 @@ theorem bound_add_depth_le {x : Call} (h : Reach mk x₀ x) :
 
 /-- **A reached active call lies above depth `B - 1`**, for the root's bound `B` plus its depth:
 it has an edge and fewer edges than its bound. -/
-theorem depth_add_two_le_of_active {x : Call} (h : Reach mk x₀ x) (ha : active x = true) :
+theorem depth_add_two_le_of_active {x : Call T} (h : Reach mk x₀ x) (ha : active x = true) :
     x.depth + 2 ≤ x₀.bound + x₀.depth := by
   have h1 := h.bound_add_depth_le
   have h2 := edges_lt_bound_of_active ha
@@ -114,13 +115,13 @@ theorem depth_add_two_le_of_active {x : Call} (h : Reach mk x₀ x) (ha : active
   omega
 
 /-- Reached calls lie at or below the root's depth. -/
-theorem depth_le {x : Call} (h : Reach mk x₀ x) : x₀.depth ≤ x.depth := by
+theorem depth_le {x : Call T} (h : Reach mk x₀ x) : x₀.depth ≤ x.depth := by
   induction h with
   | root => exact le_rfl
   | step c _ _ _ ih => change x₀.depth ≤ _ + 1; omega
 
 /-- A reached call at the root's depth is the root. -/
-theorem eq_root_of_depth_le {x : Call} (h : Reach mk x₀ x) (hd : x.depth ≤ x₀.depth) :
+theorem eq_root_of_depth_le {x : Call T} (h : Reach mk x₀ x) (hd : x.depth ≤ x₀.depth) :
     x = x₀ := by
   cases h with
   | root => rfl
@@ -133,40 +134,40 @@ end Reach
 
 /-- The derivation hypotheses of a reached active call: its frames along its children, which are
 reached, smaller in the bound and one level deeper, and its value from the last frame. -/
-private theorem reach_call {x : Call} (hx : Reach mk x₀ x) (ha : active x = true) :
-    ∃ (acc : ℕ → Frame) (child' : ℕ → Call), acc 0 = (scheme mk).start x ∧
-      (∀ c < (children x).length, (scheme mk).next x (acc c) = some (child' c)) ∧
-      (scheme mk).next x (acc (children x).length) = none ∧
-      (∀ c < (children x).length, (scheme mk).absorb x (acc c)
-        ((child' c).depth, value mk (child' c)) = acc (c + 1)) ∧
-      (∀ c < (children x).length, (reachInv mk x₀).frame x (acc c) ∧
+private theorem reach_call {x : Call T} (hx : Reach mk x₀ x) (ha : active x = true) :
+    ∃ (acc : ℕ → Frame) (child' : ℕ → Call T), acc 0 = (scheme ev mk).start x ∧
+      (∀ c < (children x).length, (scheme ev mk).next x (acc c) = some (child' c)) ∧
+      (scheme ev mk).next x (acc (children x).length) = none ∧
+      (∀ c < (children x).length, (scheme ev mk).absorb x (acc c)
+        ((child' c).depth, value ev mk (child' c)) = acc (c + 1)) ∧
+      (∀ c < (children x).length, (reachInv ev mk x₀).frame x (acc c) ∧
         Reach mk x₀ (child' c) ∧ (child' c).bound < x.bound ∧ (child' c).depth = x.depth + 1) ∧
-      (x.depth, value mk x) = (scheme mk).finish x (acc (children x).length) := by
-  obtain ⟨h0, hnext, hdone, habs, hfin⟩ := walk mk ha fun c => value mk (child x mk c)
-  refine ⟨frameAt x fun c => value mk (child x mk c),
+      (x.depth, value ev mk x) = (scheme ev mk).finish x (acc (children x).length) := by
+  obtain ⟨h0, hnext, hdone, habs, hfin⟩ := walk ev mk ha fun c => value ev mk (child x mk c)
+  refine ⟨frameAt x fun c => value ev mk (child x mk c),
     fun c => child x mk ((children x).getD c (0, 0, [], 0)), h0, hnext, hdone,
     fun c hc => habs c hc, fun c hc => ⟨⟨hx, ha, c, hc.le, rfl⟩, ?_, ?_, rfl⟩, ?_⟩
   · exact Reach.step _ hx ha (List.getD_eq_getElem _ _ hc ▸ List.getElem_mem hc)
   · exact edges_lt_bound_of_active ha
   · simp only [scheme, Prod.mk.injEq, true_and]
-    rw [value_of_active mk ha, hfin]
+    rw [value_of_active ev mk ha, hfin]
 
 /-- The leaves and values of a derivation over the reached calls. -/
-private theorem reach_leaf {x : Call} (hl : (scheme mk).isLeaf x = true) :
-    (x.depth, value mk x) = (scheme mk).leaf x := by
+private theorem reach_leaf {x : Call T} (hl : (scheme ev mk).isLeaf x = true) :
+    (x.depth, value ev mk x) = (scheme ev mk).leaf x := by
   have hl' : active x = false := by simpa [scheme] using hl
-  simp [scheme, value_of_not_active mk hl']
+  simp [scheme, value_of_not_active ev mk hl']
 
-private theorem active_of_isLeaf_eq_false {x : Call} (hl : (scheme mk).isLeaf x = false) :
+private theorem active_of_isLeaf_eq_false {x : Call T} (hl : (scheme ev mk).isLeaf x = false) :
     active x = true := by simpa [scheme] using hl
 
 /-- **A derivation of the root with its height.** A root at depth `0` with edge bound `B` has a
 derivation of its tagged value over the reached calls with at most `B` stack levels, for every
 child builder. -/
 theorem exists_eval_reachInv (hx₀ : x₀.depth = 0) :
-    ∃ N H, (scheme mk).Eval (reachInv mk x₀) x₀ (0, value mk x₀) N H ∧ H ≤ x₀.bound := by
-  obtain ⟨N, H, he, hH⟩ := Scheme.exists_eval_of_height (R := scheme mk) (I := reachInv mk x₀)
-    Call.bound Call.depth (fun x => (x.depth, value mk x)) x₀.bound (fun x _ hl => reach_leaf hl)
+    ∃ N H, (scheme ev mk).Eval (reachInv ev mk x₀) x₀ (0, value ev mk x₀) N H ∧ H ≤ x₀.bound := by
+  obtain ⟨N, H, he, hH⟩ := Scheme.exists_eval_of_height (R := scheme ev mk) (I := reachInv ev mk x₀)
+    Call.bound Call.depth (fun x => (x.depth, value ev mk x)) x₀.bound (fun x _ hl => reach_leaf hl)
     (fun x hx hl => by
       have ha := active_of_isLeaf_eq_false hl
       have hd := (show Reach mk x₀ x from hx).depth_add_two_le_of_active ha
@@ -182,10 +183,11 @@ value over the reached calls with at most `Nat.recursionBound b D 0` nodes and `
 theorem exists_eval_reachInv_count (hx₀ : x₀.depth = 0) (D : ℕ) (b : ℕ → ℕ)
     (hcnt : ∀ x, Reach mk x₀ x → active x = true →
       x.depth < D ∧ (children x).length ≤ b x.depth) :
-    ∃ N H, (scheme mk).Eval (reachInv mk x₀) x₀ (0, value mk x₀) N H ∧
+    ∃ N H, (scheme ev mk).Eval (reachInv ev mk x₀) x₀ (0, value ev mk x₀) N H ∧
       N ≤ Nat.recursionBound b D 0 ∧ H ≤ D := by
-  obtain ⟨N, H, he, hN, hH⟩ := Scheme.exists_eval_of_counted (R := scheme mk) (I := reachInv mk x₀)
-    Call.bound Call.depth (fun x => (x.depth, value mk x)) b D (fun x _ hl => reach_leaf hl)
+  obtain ⟨N, H, he, hN, hH⟩ := Scheme.exists_eval_of_counted (R := scheme ev mk)
+    (I := reachInv ev mk x₀)
+    Call.bound Call.depth (fun x => (x.depth, value ev mk x)) b D (fun x _ hl => reach_leaf hl)
     (fun x hx hl => by
       have ha := active_of_isLeaf_eq_false hl
       obtain ⟨hd, hb⟩ := hcnt x hx ha
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean
index 5a9865f61..46dd54e3e 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean
@@ -17,11 +17,11 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
 # The leaves of the fast contraction algorithm
 
 The cost of the leaves of the native recursion of Theorem D.1 of [OpenAI2026ETH]
-(`Cslib.Circuits.Frontier.FastContraction.leafCertificate`), the leaf clause of the resource
-analysis `Cslib.Complexity.CountingSimulation.FastAnalysis`. A leaf sums directly over the `2 ^ M`
-edge assignments of a call with `M` edges (§D.4.7, p. 64), and the entry of a packet vertex costs
-`(m + 2) ^ L` for `m` target modes and `L` row ports, the source's `exp(O(L log s))` (§D.4.6,
-p. 63).
+(`Cslib.Circuits.Frontier.FastContraction.leafCertificate`, over tables), the leaf clause of the
+resource analysis `Cslib.Complexity.CountingSimulation.FastAnalysis`. A leaf sums directly over the
+`2 ^ M` edge assignments of a call with `M` edges (§D.4.7, p. 64), and the entry of a packet vertex
+costs `(m + 2) ^ L` for `m` target modes and `L` row ports, the source's `exp(O(L log s))`
+(§D.4.6, p. 63).
 
 **The cost of a leaf** (`FastContraction.leafCertificate_le`): with at most `R` target modes and
 `Λ` row ports per vertex, time `K (n + R + 1) ^ K 2 ^ M (R + 2) ^ Λ` and space `K (n + R + 1) ^ K`
@@ -74,12 +74,18 @@ namespace FastContraction
 open GaloisRingArith NativePacket ChildCursor NativeRecovery ContractionSchedule NativeChild
   Cslib.GenericRAM Cslib.GenericRAM.StackRecursion Turing.MultiTapeTM
 
+variable {T : Type}
+
 /-! ### Encoded lengths -/
 
+section Lengths
+
+variable (encT : T ↪ List Bool)
+
 /-- The scale, the precision and the coefficients of the modulus are at most the encoded length
 of a call. -/
-theorem scale_add_prec_add_length_fl_le (x : Call) :
-    x.scale + x.prec + x.fl.length ≤ (encCall x).length := by
+theorem scale_add_prec_add_length_fl_le (x : Call T) :
+    x.scale + x.prec + x.fl.length ≤ (encCall encT x).length := by
   have h := length_le_length_encList encNat x.fl
   obtain ⟨⟨s, d, b, p, fl, r⟩, D⟩ := x
   simp only [Call.scale, Call.prec, Call.fl, encCall, encParams, length_encPair, encUnary_apply,
@@ -87,32 +93,37 @@ theorem scale_add_prec_add_length_fl_le (x : Call) :
   omega
 
 /-- The network of a call is at most its encoded length. -/
-theorem length_net_le (x : Call) :
-    (DescribedNetwork.encDescribed VertexDesc.enc x.net).length ≤ (encCall x).length := by
+theorem length_net_le (x : Call T) :
+    (DescribedNetwork.encDescribed (VertexDesc.enc encT) x.net).length ≤
+      (encCall encT x).length := by
   obtain ⟨p, D⟩ := x
   simp only [Call.net, encCall, length_encPair]
   omega
 
 /-- A vertex of a call is at most its encoded length. -/
-theorem length_vertex_le {x : Call} {v : List ℕ × VertexDesc} (hv : v ∈ x.net.vertices) :
-    (encPair (encList encNat) VertexDesc.enc v).length ≤ (encCall x).length := by
-  have h := length_le_encList_of_mem (encPair (encList encNat) VertexDesc.enc) hv
-  have h2 : (encList (encPair (encList encNat) VertexDesc.enc) x.net.vertices).length ≤
-      (DescribedNetwork.encDescribed VertexDesc.enc x.net).length := by
-    change _ ≤ (encPair encUnary (encList (encPair (encList encNat) VertexDesc.enc))
+theorem length_vertex_le {x : Call T} {v : List ℕ × VertexDesc T}
+    (hv : v ∈ x.net.vertices) :
+    (encPair (encList encNat) (VertexDesc.enc encT) v).length ≤ (encCall encT x).length := by
+  have h := length_le_encList_of_mem (encPair (encList encNat) (VertexDesc.enc encT)) hv
+  have h2 : (encList (encPair (encList encNat) (VertexDesc.enc encT)) x.net.vertices).length ≤
+      (DescribedNetwork.encDescribed (VertexDesc.enc encT) x.net).length := by
+    change _ ≤ (encPair encUnary (encList (encPair (encList encNat) (VertexDesc.enc encT)))
       (x.net.numEdges, x.net.vertices)).length
     rw [length_encPair]
     dsimp only
     omega
-  have h3 := length_net_le x
+  have h3 := length_net_le encT x
   omega
 
 /-- The number of vertices of a call is at most its encoded length. -/
-theorem length_vertices_le (x : Call) : x.net.vertices.length ≤ (encCall x).length := by
-  have h := DescribedNetwork.length_numEdges_vertices_le (encT := VertexDesc.enc) x.net
-  have h3 := length_net_le x
+theorem length_vertices_le (x : Call T) :
+    x.net.vertices.length ≤ (encCall encT x).length := by
+  have h := DescribedNetwork.length_numEdges_vertices_le (encT := VertexDesc.enc encT) x.net
+  have h3 := length_net_le encT x
   omega
 
+end Lengths
+
 /-! ### The cost of a leaf -/
 
 /-- `c (y + 1) ^ d ≤ c W ^ d` when `y + 1 ≤ W`. -/
@@ -261,25 +272,26 @@ private theorem space_assemble {Sd Si Ss cd dd ci di W A Zb c₁ c₂ E₀ K₁
 whose vertices have at most `R` target modes and at most `Λ` row ports on every bit list on their
 ports, direct summation takes time at most `K (n + R + 1) ^ K 2 ^ M (R + 2) ^ Λ` and space at most
 `K (n + R + 1) ^ K`, whatever the child builder. -/
-theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × DescribedNetwork VertexDesc)
-    (x : Call) (R Λ : ℕ),
+theorem leafCertificate_le : ∃ K : ℕ,
+    ∀ (mk : Call (List ℕ) → State → ℕ × DescribedNetwork (VertexDesc (List ℕ)))
+    (x : Call (List ℕ)) (R Λ : ℕ),
     (∀ v ∈ x.net.vertices, v.2.modes ≤ R ∧
       ∀ bs : List Bool, bs.length = v.1.length → v.2.rowPorts bs ≤ Λ) →
     (leafCertificate mk).time x ≤
-        K * ((encCall x).length + R + 1) ^ K * 2 ^ x.edges * (R + 2) ^ Λ ∧
-      (leafCertificate mk).space x ≤ K * ((encCall x).length + R + 1) ^ K := by
+        K * ((encCall (encList encNat) x).length + R + 1) ^ K * 2 ^ x.edges * (R + 2) ^ Λ ∧
+      (leafCertificate mk).space x ≤ K * ((encCall (encList encNat) x).length + R + 1) ^ K := by
   obtain ⟨K₁, hK₁⟩ := DescribedNetwork.contractionCertificate_le (ops := SumOps.galois)
-    (eval := VertexDesc.entry) (encQ := encPair encUnary (encList encNat))
-    (encY := encList encNat) (encT := VertexDesc.enc) SumOps.galois_polyTime
+    (eval := VertexDesc.entry tableEntry) (encQ := encPair encUnary (encList encNat))
+    (encY := encList encNat) (encT := VertexDesc.enc (encList encNat)) SumOps.galois_polyTime
     VertexDesc.entryCertificate
   obtain ⟨K₂, hK₂⟩ := VertexDesc.entryCertificate_le
-  have hD := NativeCertificate.ofPolyTime_isPolynomial depth_polyTime
-  have hI := NativeCertificate.ofPolyTime_isPolynomial leafInput_polyTime
+  have hD := NativeCertificate.ofPolyTime_isPolynomial (depth_polyTime (encList encNat))
+  have hI := NativeCertificate.ofPolyTime_isPolynomial (leafInput_polyTime (encList encNat))
   obtain ⟨cd, dd, hdt⟩ := hD.1.exists_le
   obtain ⟨cd', dd', hds⟩ := hD.2.exists_le
   obtain ⟨ci, di, hit⟩ := hI.1.exists_le
   obtain ⟨ci', di', his⟩ := hI.2.exists_le
-  obtain ⟨cl, dl, hl⟩ := leafInput_polyTime.polyBounded_length.exists_le
+  obtain ⟨cl, dl, hl⟩ := (leafInput_polyTime (encList encNat)).polyBounded_length.exists_le
   obtain ⟨cp, dp, hp⟩ := PacketCtx.p_polyTime.polyBounded_length.exists_le
   obtain ⟨cf, df, hf⟩ := PacketCtx.fl_polyTime.polyBounded_length.exists_le
   obtain ⟨ct, dt, ht⟩ := VertexDesc.tableEntry_polyTime.polyBounded_length.exists_le
@@ -293,22 +305,22 @@ theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × De
       (K₁ * c₁ ^ K₁ + K₂ * c₂ ^ K₂) + cd' + ci' := ⟨_, rfl⟩
   obtain ⟨Dg, hDg⟩ : ∃ Dg, Dg = 1 + E₀ * (K₁ + K₂) + dd + di + dd' + di' := ⟨_, rfl⟩
   refine ⟨G + Dg, fun mk x R Λ hRΛ => ?_⟩
-  obtain ⟨n, hn⟩ : ∃ n, n = (encCall x).length := ⟨_, rfl⟩
+  obtain ⟨n, hn⟩ : ∃ n, n = (encCall (encList encNat) x).length := ⟨_, rfl⟩
   obtain ⟨W, hW⟩ : ∃ W, W = n + R + 1 := ⟨_, rfl⟩
   rw [← hn, show n + R + 1 = W from hW.symm]
   have hW1 : 1 ≤ W := by omega
   have hnW : n + 1 ≤ W := by omega
   -- The precision and the modulus of the call.
-  have hpfl := scale_add_prec_add_length_fl_le x
+  have hpfl := scale_add_prec_add_length_fl_le (encList encNat) x
   rw [← hn] at hpfl
   -- Every vertex and bit list on its ports is at most `3 n + 1` long.
-  have hq (v : List ℕ × VertexDesc) (hv : v ∈ x.net.vertices) (bs : List Bool)
+  have hq (v : List ℕ × VertexDesc (List ℕ)) (hv : v ∈ x.net.vertices) (bs : List Bool)
       (hbs : bs.length = v.1.length) :
-      (encPair VertexDesc.enc encBits (v.2, bs)).length ≤ 3 * n + 1 := by
-    have h1 := length_vertex_le hv
+      (encPair (VertexDesc.enc (encList encNat)) encBits (v.2, bs)).length ≤ 3 * n + 1 := by
+    have h1 := length_vertex_le (encList encNat) hv
     have h2 := length_le_length_encList encNat v.1
     rw [length_encPair] at h1 ⊢
-    change 2 * (VertexDesc.enc v.2).length + 1 + bs.length ≤ 3 * n + 1
+    change 2 * (VertexDesc.enc (encList encNat) v.2).length + 1 + bs.length ≤ 3 * n + 1
     omega
   -- The reduced coefficient lists.
   obtain ⟨Rv, hRv⟩ : ∃ Rv, Rv = n * (2 * n + 3) +
@@ -320,13 +332,13 @@ theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × De
     have : x.fl.length * (2 * x.prec + 3) ≤ n * (2 * n + 3) :=
       Nat.mul_le_mul (by omega) (by omega)
     omega
-  have hpacket (v : List ℕ × VertexDesc) (hv : v ∈ x.net.vertices) (d : PacketDesc)
+  have hpacket (v : List ℕ × VertexDesc (List ℕ)) (hv : v ∈ x.net.vertices) (d : PacketDesc)
       (hd : v.2 = .inr d) :
       ∀ y, SumOps.galois.Reduced (d.1.p, d.1.fl) y → (encList encNat y).length ≤ Rv := by
     intro y hy
     have h := SumOps.length_encList_le_of_galois_reduced hy
     simp only at h
-    have h1 := length_vertex_le hv
+    have h1 := length_vertex_le (encList encNat) hv
     rw [length_encPair, hd, length_encSum] at h1
     simp only [Sum.elim_inr] at h1
     have h2 : (PacketCtx.enc d.1).length ≤ n := by
@@ -349,7 +361,7 @@ theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × De
       bs.length = v.1.length →
       VertexDesc.entryCertificate.time (v.2, bs) ≤ K₂ * (R + 2) ^ Λ * Zb ^ K₂ ∧
         VertexDesc.entryCertificate.space (v.2, bs) ≤ K₂ * Zb ^ K₂ ∧
-        (encList encNat (VertexDesc.entry v.2 bs)).length ≤ Rv := by
+        (encList encNat (VertexDesc.entry tableEntry v.2 bs)).length ≤ Rv := by
     intro v hv bs hbs
     have hlen := hq v hv bs hbs
     obtain ⟨hmodes, hrows⟩ := hRΛ v hv
@@ -360,7 +372,8 @@ theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × De
       · exact hpacket v hv d hd
     obtain ⟨hT, hS⟩ := hK₂ (v.2, bs) Rv hRLE
     dsimp only at hT hS
-    have hZ : (encPair VertexDesc.enc encBits (v.2, bs)).length + v.2.modes + Rv + 2 ≤ Zb := by
+    have hZ : (encPair (VertexDesc.enc (encList encNat)) encBits (v.2, bs)).length + v.2.modes +
+        Rv + 2 ≤ Zb := by
       omega
     refine ⟨hT.trans ?_, hS.trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hZ _)), ?_⟩
     · refine Nat.mul_le_mul (Nat.mul_le_mul_left _ ?_) (Nat.pow_le_pow_left hZ _)
@@ -369,30 +382,33 @@ theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × De
       · have := ht (v.2, bs)
         rw [hd] at this
         refine this.trans ?_
-        have h3 : (encPair VertexDesc.enc encBits (Sum.inl t, bs)).length + 1 ≤ 3 * n + 2 := by
+        have h3 : (encPair (VertexDesc.enc (encList encNat)) encBits (Sum.inl t, bs)).length + 1 ≤
+            3 * n + 2 := by
           rw [← hd]; omega
-        calc ct * ((encPair VertexDesc.enc encBits (Sum.inl t, bs)).length + 1) ^ dt
+        calc ct * ((encPair (VertexDesc.enc (encList encNat)) encBits (Sum.inl t, bs)).length
+              + 1) ^ dt
             ≤ ct * (3 * n + 2) ^ dt := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left h3 _)
           _ ≤ Rv := by omega
-      · exact hpacket v hv d hd _ (VertexDesc.reduced_entry_inr d bs)
+      · exact hpacket v hv d hd _ (VertexDesc.reduced_entry_inr tableEntry d bs)
   obtain ⟨hsT, hsS⟩ := hK₁ ((x.prec, x.fl), x.net) (K₂ * (R + 2) ^ Λ * Zb ^ K₂) (K₂ * Zb ^ K₂) Rv
     Rv hentry hred
   -- Polynomial pieces against `W`.
-  have hk : x.net.vertices.length + 1 ≤ W := by have := length_vertices_le x; omega
+  have hk : x.net.vertices.length + 1 ≤ W := by have := length_vertices_le (encList encNat) x; omega
   have hRvW : Rv ≤ cR * W ^ e := by
     rw [hRv, hcR, he]; exact rv_le hnW
   have hWE : W ^ e ≤ W ^ E₀ := Nat.pow_le_pow_right hW1 (by omega)
-  have hA1 : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) VertexDesc.enc
-      ((x.prec, x.fl), x.net)).length + Rv + Rv + 1 ≤ c₁ * W ^ E₀ := by
-    have h1 : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) VertexDesc.enc
-        ((x.prec, x.fl), x.net)).length ≤ cl * W ^ dl :=
+  have hA1 : (DescribedNetwork.encInput (encPair encUnary (encList encNat))
+      (VertexDesc.enc (encList encNat)) ((x.prec, x.fl), x.net)).length + Rv + Rv + 1 ≤
+        c₁ * W ^ E₀ := by
+    have h1 : (DescribedNetwork.encInput (encPair encUnary (encList encNat))
+        (VertexDesc.enc (encList encNat)) ((x.prec, x.fl), x.net)).length ≤ cl * W ^ dl :=
       (hl x).trans (by rw [← hn]; exact mul_pow_le_of_le hnW)
     rw [hc₁]
     exact sum_le_of_le hW1 h1 (by omega) (hRvW.trans (Nat.mul_le_mul_left _ hWE))
   have hZW : Zb ≤ c₂ * W ^ E₀ := by
     rw [hc₂, hZb]
     exact zb_le hW1 (by omega) (hRvW.trans (Nat.mul_le_mul_left _ hWE)) (by omega)
-  have hnW' : (encCall x).length + 1 ≤ W := by omega
+  have hnW' : (encCall (encList encNat) x).length + 1 ≤ W := by omega
   have hdt' := (hdt x).trans (mul_pow_le_of_le (c := cd) (d := dd) hnW')
   have hit' := (hit x).trans (mul_pow_le_of_le (c := ci) (d := di) hnW')
   have hds' := (hds x).trans (mul_pow_le_of_le (c := cd') (d := dd') hnW')
@@ -415,7 +431,7 @@ theorem leafCertificate_le : ∃ K : ℕ, ∀ (mk : Call → State → ℕ × De
 `2 ^ a` and distinct among its row ports. So it has at most `2 ^ (⌊log₂ s⌋ / 32768) p` target modes
 and at most `2 ^ (⌊log₂ s⌋ / 32768)` row ports (`modes_le_of_packetShape`,
 `rowPorts_le_of_packetShape`). -/
-def PacketShape (x : Call) : Prop :=
+def PacketShape (x : Call T) : Prop :=
   ∀ v ∈ x.net.vertices, ∀ d : PacketDesc, v.2 = .inr d →
     d.1.i < d.1.a ∧ d.1.a ≤ Nat.log 2 x.scale / 32768 ∧ d.1.tiles = 2 ^ (d.1.i + 1) ∧
       d.1.nb ≤ x.prec ∧ (∀ y ∈ d.2.1, y.2 < 2 ^ d.1.a) ∧ ((d.2.1.filter (·.1)).map (·.2)).Nodup
@@ -431,7 +447,7 @@ theorem packetShape_root (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) : PacketS
 vertex keeps its descriptor, at a precision that only grows, and a new packet has `a` slot bits
 (`slotBits_le`), `i < a` (the valuation of its node), `2 ^ (i + 1)` tiles, the child's precision
 as its number of exponents per tile, and the slots of the packing, distinct within a packet. -/
-theorem packetShape_child {x : Call} (hx : WF x) (ha : active x = true) (hs : PacketShape x)
+theorem packetShape_child {x : Call T} (hx : WF x) (ha : active x = true) (hs : PacketShape x)
     {c : State} (hc : c ∈ children x) : PacketShape (child x nativeMk c) := by
   -- The builder at a cursor state of a well-formed active call: the uncapped native child.
   have hmk : (nativeMk x c).2 = nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0))
@@ -484,7 +500,7 @@ theorem two_pow_log_div_le (s : ℕ) : 2 ^ (Nat.log 2 s / 32768) ≤ s + 1 := by
       _ ≤ s + 1 := Nat.le_succ s
 
 /-- **The target modes of a call with the packet shape**: at most `2 ^ (⌊log₂ s⌋ / 32768) p`. -/
-theorem modes_le_of_packetShape {x : Call} (hs : PacketShape x) {v : List ℕ × VertexDesc}
+theorem modes_le_of_packetShape {x : Call T} (hs : PacketShape x) {v : List ℕ × VertexDesc T}
     (hv : v ∈ x.net.vertices) : v.2.modes ≤ 2 ^ (Nat.log 2 x.scale / 32768) * x.prec := by
   rcases hd : v.2 with t | d
   · simp [VertexDesc.modes]
@@ -499,7 +515,7 @@ theorem modes_le_of_packetShape {x : Call} (hs : PacketShape x) {v : List ℕ ×
 
 /-- **The row ports of a call with the packet shape**: at most `2 ^ (⌊log₂ s⌋ / 32768)`, since
 the slots of the row ports of a packet are distinct and below `2 ^ a`. -/
-theorem rowPorts_le_of_packetShape {x : Call} (hs : PacketShape x) {v : List ℕ × VertexDesc}
+theorem rowPorts_le_of_packetShape {x : Call T} (hs : PacketShape x) {v : List ℕ × VertexDesc T}
     (hv : v ∈ x.net.vertices) (bs : List Bool) :
     v.2.rowPorts bs ≤ 2 ^ (Nat.log 2 x.scale / 32768) := by
   rcases hd : v.2 with t | d
@@ -525,28 +541,32 @@ length `n` with `M` edges, scale `s` and precision `p` with the packet shape, wr
 `A = 2 ^ (⌊log₂ s⌋ / 32768)`, direct summation takes time at most
 `K (n + 1) ^ K 2 ^ M (A p + 2) ^ A` and space at most `K (n + 1) ^ K`. -/
 theorem leafCertificate_le_of_packetShape : ∃ K : ℕ,
-    ∀ (mk : Call → State → ℕ × DescribedNetwork VertexDesc) (x : Call), PacketShape x →
-      (leafCertificate mk).time x ≤ K * ((encCall x).length + 1) ^ K * 2 ^ x.edges *
+    ∀ (mk : Call (List ℕ) → State → ℕ × DescribedNetwork (VertexDesc (List ℕ)))
+      (x : Call (List ℕ)), PacketShape x →
+      (leafCertificate mk).time x ≤ K * ((encCall (encList encNat) x).length + 1) ^ K *
+          2 ^ x.edges *
           (2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 2) ^ 2 ^ (Nat.log 2 x.scale / 32768) ∧
-        (leafCertificate mk).space x ≤ K * ((encCall x).length + 1) ^ K := by
+        (leafCertificate mk).space x ≤ K * ((encCall (encList encNat) x).length + 1) ^ K := by
   obtain ⟨K, hK⟩ := leafCertificate_le
   refine ⟨2 * K, fun mk x hs => ?_⟩
   obtain ⟨hT, hS⟩ := hK mk x (2 ^ (Nat.log 2 x.scale / 32768) * x.prec)
     (2 ^ (Nat.log 2 x.scale / 32768)) fun v hv =>
       ⟨modes_le_of_packetShape hs hv, fun bs _ => rowPorts_le_of_packetShape hs hv bs⟩
-  have hn := scale_add_prec_add_length_fl_le x
+  have hn := scale_add_prec_add_length_fl_le (encList encNat) x
   have hA := two_pow_log_div_le x.scale
-  have hR : (encCall x).length + 2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 1 ≤
-      ((encCall x).length + 1) ^ 2 := by
+  have hR : (encCall (encList encNat) x).length + 2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 1 ≤
+      ((encCall (encList encNat) x).length + 1) ^ 2 := by
     have : 2 ^ (Nat.log 2 x.scale / 32768) * x.prec ≤
-        ((encCall x).length + 1) * (encCall x).length := Nat.mul_le_mul (by omega) (by omega)
+        ((encCall (encList encNat) x).length + 1) * (encCall (encList encNat) x).length :=
+      Nat.mul_le_mul (by omega) (by omega)
     nlinarith
-  have hpow : K * ((encCall x).length + 2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 1) ^ K ≤
-      2 * K * ((encCall x).length + 1) ^ (2 * K) :=
-    calc _ ≤ K * (((encCall x).length + 1) ^ 2) ^ K :=
+  have hpow :
+      K * ((encCall (encList encNat) x).length + 2 ^ (Nat.log 2 x.scale / 32768) * x.prec + 1) ^ K ≤
+        2 * K * ((encCall (encList encNat) x).length + 1) ^ (2 * K) :=
+    calc _ ≤ K * (((encCall (encList encNat) x).length + 1) ^ 2) ^ K :=
           Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hR _)
-      _ = K * ((encCall x).length + 1) ^ (2 * K) := by rw [← pow_mul]
-      _ ≤ 2 * K * ((encCall x).length + 1) ^ (2 * K) :=
+      _ = K * ((encCall (encList encNat) x).length + 1) ^ (2 * K) := by rw [← pow_mul]
+      _ ≤ 2 * K * ((encCall (encList encNat) x).length + 1) ^ (2 * K) :=
           Nat.mul_le_mul_right _ (by omega)
   exact ⟨hT.trans (Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hpow)), hS.trans hpow⟩
 
@@ -634,18 +654,19 @@ provided that from `s₀` on it has at most `leafSize m` edges and precision at
 `s₀` on, `2 ^ M ≤ 2 ^ (C s / √⌊log₂ s⌋)` and the packet factor is subexponential
 (`exists_packetFactor_le`). -/
 theorem exists_leafCertificate_le (C c s₀ : ℕ) : ∃ K : ℕ,
-    ∀ (mk : Call → State → ℕ × DescribedNetwork VertexDesc) (s : ℕ) (x : Call), 2 ≤ s →
+    ∀ (mk : Call (List ℕ) → State → ℕ × DescribedNetwork (VertexDesc (List ℕ))) (s : ℕ)
+      (x : Call (List ℕ)), 2 ≤ s →
       s ≤ x.scale → x.scale ≤ C * s → PacketShape x → x.edges ≤ 2 * x.scale →
       (s₀ ≤ s → x.edges ≤ leafSize x.scale ∧ x.prec ≤ x.scale ^ c) →
       (leafCertificate mk).time x ≤
-          K * ((encCall x).length + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧
-        (leafCertificate mk).space x ≤ K * ((encCall x).length + 1) ^ K := by
+          K * ((encCall (encList encNat) x).length + 1) ^ K * 2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧
+        (leafCertificate mk).space x ≤ K * ((encCall (encList encNat) x).length + 1) ^ K := by
   obtain ⟨K₀, hK₀⟩ := leafCertificate_le_of_packetShape
   obtain ⟨K₁, hK₁⟩ := exists_packetFactor_le C c
   obtain ⟨Ks, hKs⟩ : ∃ Ks, Ks = K₀ * 2 ^ (2 * (C * s₀)) * (C * s₀ + 2) ^ (C * s₀) := ⟨_, rfl⟩
   refine ⟨Ks + K₀ + C * s₀ + C + K₁, fun mk s x hs hsm hmC hshape hM hbig => ?_⟩
   obtain ⟨hT, hS⟩ := hK₀ mk x hshape
-  set n := (encCall x).length with hn
+  set n := (encCall (encList encNat) x).length with hn
   set K := Ks + K₀ + C * s₀ + C + K₁ with hK
   set S := Nat.sqrt (Nat.log 2 s) with hSdef
   have hS1 : 1 ≤ S := Nat.one_le_sqrt_log_two hs
@@ -659,7 +680,7 @@ theorem exists_leafCertificate_le (C c s₀ : ℕ) : ∃ K : ℕ,
   rcases lt_or_ge s s₀ with hsmall | hlarge
   · -- Below `s₀`: constants and a polynomial.
     have hmC' : x.scale ≤ C * s₀ := hmC.trans (Nat.mul_le_mul_left _ hsmall.le)
-    have hp : x.prec ≤ n := by have := scale_add_prec_add_length_fl_le x; omega
+    have hp : x.prec ≤ n := by have := scale_add_prec_add_length_fl_le (encList encNat) x; omega
     have h2M : 2 ^ x.edges ≤ 2 ^ (2 * (C * s₀)) :=
       Nat.pow_le_pow_right (by norm_num) (by omega)
     have hbase : A * x.prec + 2 ≤ (C * s₀ + 2) * (n + 1) := by
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean
index 922fff07f..0f1c09927 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionMachine.lean
@@ -26,7 +26,10 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFr
 # The native machine of the fast contraction algorithm
 
 The stack recursion of `Cslib.Circuits.Frontier.FastContraction.scheme` as one native machine for
-the contraction modulo `2 ^ P` of an explicit network `(r, G)`, with the precision `P` in binary.
+the contraction modulo `2 ^ P` of an explicit network `(r, G)`, with the precision `P` in binary:
+the root descriptors are tables (`T = List ℕ`), read by the entry procedure `tableEntry`. The
+encodings, the root network (`FastContraction.rootNet`) and its polynomial-time construction are
+stated for every type of root descriptors.
 
 **The root.** The precision is first capped at the encoded length of the network
 (`ExplicitTensorNetwork.capPrecision`), which does not change the residue. The root call
@@ -81,6 +84,8 @@ namespace Cslib.Circuits.Frontier.FastContraction
 open GaloisRingArith ChildCursor Cslib.GenericRAM Cslib.GenericRAM.StackRecursion
   Turing.MultiTapeTM
 
+variable {T : Type}
+
 /-! ### Encodings -/
 
 /-- The encoding of the parameters of a call: the scale, the depth, the edge bound and the
@@ -90,9 +95,10 @@ abbrev encParams : Params ↪ List Bool :=
   encPair encUnary (encPair encUnary (encPair encUnary (encPair encUnary
     (encPair (encList encNat) encNat))))
 
-/-- The encoding of a call: its parameters and its network. -/
-abbrev encCall : Call ↪ List Bool :=
-  encPair encParams (DescribedNetwork.encDescribed VertexDesc.enc)
+/-- The encoding of a call: its parameters and its network, with the root descriptors encoded by
+`encT`. -/
+abbrev encCall (encT : T ↪ List Bool) : Call T ↪ List Bool :=
+  encPair encParams (DescribedNetwork.encDescribed (VertexDesc.enc encT))
 
 /-- The encoding of a frame: the cursor state and the accumulator, in binary. -/
 abbrev encFrame : Frame ↪ List Bool :=
@@ -104,41 +110,47 @@ abbrev encValue : ℕ × List ℕ ↪ List Bool := encPair encUnary (encList enc
 
 /-! ### The leaves -/
 
+variable (encT : T ↪ List Bool)
+
 /-- The depth of a call is polynomial-time. -/
-theorem depth_polyTime : ComputableInPolyTime Call.depth encCall encUnary := by
+theorem depth_polyTime : ComputableInPolyTime (Call.depth (T := T)) (encCall encT) encUnary := by
   unfold Call.depth; fun_prop
 
 /-- The input of direct summation at a call, `((p, fl), D)`, is polynomial-time. -/
 theorem leafInput_polyTime :
-    ComputableInPolyTime (fun x : Call => ((x.prec, x.fl), x.net)) encCall
-      (DescribedNetwork.encInput (encPair encUnary (encList encNat)) VertexDesc.enc) := by
+    ComputableInPolyTime (fun x : Call T => ((x.prec, x.fl), x.net)) (encCall encT)
+      (DescribedNetwork.encInput (encPair encUnary (encList encNat)) (VertexDesc.enc encT)) := by
   unfold Call.prec Call.fl Call.net; fun_prop
 
-variable (mk : Call → State → ℕ × DescribedNetwork VertexDesc)
+variable (mk : Call (List ℕ) → State → ℕ × DescribedNetwork (VertexDesc (List ℕ)))
 
-/-- **The leaf certificate**: direct summation over the coefficient lists of `A_p`, with the native
-evaluator of the vertex descriptors, tagged with the depth. -/
-@[expose] noncomputable def leafCertificate : NativeCertificate (scheme mk).leaf encCall encValue :=
-  ((NativeCertificate.ofPolyTime depth_polyTime).prod
-    ((DescribedNetwork.contractionCertificate VertexDesc.entry SumOps.galois_polyTime
-      VertexDesc.entryCertificate).comp (NativeCertificate.ofPolyTime leafInput_polyTime))).congr
+/-- **The leaf certificate** over tables: direct summation over the coefficient lists of `A_p`,
+with the native evaluator of the vertex descriptors, tagged with the depth. -/
+@[expose] noncomputable def leafCertificate :
+    NativeCertificate (scheme tableEntry mk).leaf (encCall (encList encNat)) encValue :=
+  ((NativeCertificate.ofPolyTime (depth_polyTime (encList encNat))).prod
+    ((DescribedNetwork.contractionCertificate (VertexDesc.entry tableEntry)
+      SumOps.galois_polyTime VertexDesc.entryCertificate).comp
+      (NativeCertificate.ofPolyTime (leafInput_polyTime (encList encNat))))).congr
     fun _ => rfl
 
 /-- The time of a leaf: the depth, the input of direct summation, and direct summation. -/
-theorem leafCertificate_time (x : Call) :
+theorem leafCertificate_time (x : Call (List ℕ)) :
     (leafCertificate mk).time x =
-      (NativeCertificate.ofPolyTime depth_polyTime).time x +
-        ((NativeCertificate.ofPolyTime leafInput_polyTime).time x +
-          (DescribedNetwork.contractionCertificate VertexDesc.entry SumOps.galois_polyTime
-            VertexDesc.entryCertificate).time ((x.prec, x.fl), x.net)) := rfl
+      (NativeCertificate.ofPolyTime (depth_polyTime (encList encNat))).time x +
+        ((NativeCertificate.ofPolyTime (leafInput_polyTime (encList encNat))).time x +
+          (DescribedNetwork.contractionCertificate (VertexDesc.entry tableEntry)
+            SumOps.galois_polyTime VertexDesc.entryCertificate).time ((x.prec, x.fl), x.net)) :=
+  rfl
 
 /-- The space of a leaf. -/
-theorem leafCertificate_space (x : Call) :
+theorem leafCertificate_space (x : Call (List ℕ)) :
     (leafCertificate mk).space x =
-      (NativeCertificate.ofPolyTime depth_polyTime).space x +
-        ((NativeCertificate.ofPolyTime leafInput_polyTime).space x +
-          (DescribedNetwork.contractionCertificate VertexDesc.entry SumOps.galois_polyTime
-            VertexDesc.entryCertificate).space ((x.prec, x.fl), x.net)) := rfl
+      (NativeCertificate.ofPolyTime (depth_polyTime (encList encNat))).space x +
+        ((NativeCertificate.ofPolyTime (leafInput_polyTime (encList encNat))).space x +
+          (DescribedNetwork.contractionCertificate (VertexDesc.entry tableEntry)
+            SumOps.galois_polyTime VertexDesc.entryCertificate).space ((x.prec, x.fl), x.net)) :=
+  rfl
 
 /-! ### The root -/
 
@@ -188,13 +200,14 @@ theorem irreducible_modulus (m : ℕ) :
   simpa [Polynomial.map_add, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_one,
     Cslib.trinomial] using Cslib.irreducible_trinomial (modulusExp m)
 
-/-- **The tables of an explicit network as vertex descriptors.** -/
-@[expose] def rootNet (G : ExplicitTensorNetwork ℕ) : DescribedNetwork VertexDesc :=
+/-- **The root descriptors of a network as vertex descriptors**; for an explicit network, its
+tables. -/
+@[expose] def rootNet (G : DescribedNetwork T) : DescribedNetwork (VertexDesc T) :=
   ⟨G.numEdges, G.vertices.map fun v => (v.1, .inl v.2)⟩
 
 /-- **The root call** of a capped input `(p, r, G)`: scale `m`, depth `0`, edge bound `m + 1`,
 precision `p`, the modulus and the tables of `G`. -/
-@[expose] def root (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) : Call :=
+@[expose] def root (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) : Call (List ℕ) :=
   ((q.2.2.numEdges, 0, q.2.2.numEdges + 1, q.1, modulus q.2.2.numEdges, q.2.1), rootNet q.2.2)
 
 /-- The constant of the clock. -/
@@ -207,7 +220,7 @@ precision `p`, the modulus and the tables of `G`. -/
 /-- **The root computes the contraction of `G`**: in `A_p`, the contraction of the tables read as
 constants is the image of the contraction of `G`. -/
 theorem val_rootNet (p : ℕ) (fl : List ℕ) (G : ExplicitTensorNetwork ℕ) :
-    (rootNet G).contraction (fun t bs => val p fl (VertexDesc.entry t bs)) =
+    (rootNet G).contraction (fun t bs => val p fl (VertexDesc.entry tableEntry t bs)) =
       (G.contraction : Ring p fl) := by
   rw [← DescribedNetwork.contraction_entry]
   have h := DescribedNetwork.map_contraction (Nat.castRingHom (Ring p fl))
@@ -287,33 +300,34 @@ private theorem network_polyTime :
   (ComputableInPolyTime.snd encNat ExplicitTensorNetwork.encExplicitNetwork).comp
     (ComputableInPolyTime.snd encUnary (encPair encNat ExplicitTensorNetwork.encExplicitNetwork))
 
-/-- **The tables as descriptors are polynomial-time.** -/
-theorem rootNet_polyTime : ComputableInPolyTime rootNet ExplicitTensorNetwork.encExplicitNetwork
-    (DescribedNetwork.encDescribed VertexDesc.enc) := by
-  have hpair : ComputableInPolyTime (DescribedNetwork.equivProd (T := List ℕ))
-      ExplicitTensorNetwork.encExplicitNetwork
-      (encPair encUnary (encList (encPair (encList encNat) (encList encNat)))) :=
+/-- **The root descriptors as vertex descriptors are polynomial-time.** -/
+theorem rootNet_polyTime :
+    ComputableInPolyTime rootNet (DescribedNetwork.encDescribed encT)
+      (DescribedNetwork.encDescribed (VertexDesc.enc encT)) := by
+  have hpair : ComputableInPolyTime (DescribedNetwork.equivProd (T := T))
+      (DescribedNetwork.encDescribed encT)
+      (encPair encUnary (encList (encPair (encList encNat) encT))) :=
     ComputableInPolyTime.of_eq fun _ => rfl
   have hm := (ComputableInPolyTime.fst _ _).comp hpair
   have hvs := (ComputableInPolyTime.snd _ _).comp hpair
-  have hv : ComputableInPolyTime (fun q : ExplicitTensorNetwork ℕ × (List ℕ × List ℕ) =>
-      (q.2.1, (Sum.inl q.2.2 : VertexDesc)))
-      (encPair ExplicitTensorNetwork.encExplicitNetwork (encPair (encList encNat) (encList encNat)))
-      (encPair (encList encNat) VertexDesc.enc) :=
+  have hv : ComputableInPolyTime (fun q : DescribedNetwork T × (List ℕ × T) =>
+      (q.2.1, (Sum.inl q.2.2 : VertexDesc T)))
+      (encPair (DescribedNetwork.encDescribed encT) (encPair (encList encNat) encT))
+      (encPair (encList encNat) (VertexDesc.enc encT)) :=
     ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)).prod
       ((ComputableInPolyTime.sumInl _ _).comp
         ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd _ _)))
-  have hmap := ComputableInPolyTime.mapWithInput (f := fun _ v => (v.1, (Sum.inl v.2 : VertexDesc)))
-    hvs hv
-  have hout : ComputableInPolyTime (DescribedNetwork.equivProd (T := VertexDesc)).symm
-      (encPair encUnary (encList (encPair (encList encNat) VertexDesc.enc)))
-      (DescribedNetwork.encDescribed VertexDesc.enc) :=
+  have hmap := ComputableInPolyTime.mapWithInput
+    (f := fun _ v => (v.1, (Sum.inl v.2 : VertexDesc T))) hvs hv
+  have hout : ComputableInPolyTime (DescribedNetwork.equivProd (T := VertexDesc T)).symm
+      (encPair encUnary (encList (encPair (encList encNat) (VertexDesc.enc encT))))
+      (DescribedNetwork.encDescribed (VertexDesc.enc encT)) :=
     ComputableInPolyTime.of_eq fun _ => rfl
   exact (hout.comp (hm.prod hmap)).of_enc_eq fun _ => rfl
 
 /-- **The root call is polynomial-time**, from a capped input. -/
 theorem root_polyTime : ComputableInPolyTime root ExplicitTensorNetwork.encContractionInput
-    encCall := by
+    (encCall (encList encNat)) := by
   have hp := ComputableInPolyTime.fst encUnary (encPair encNat
     ExplicitTensorNetwork.encExplicitNetwork)
   have hr := (ComputableInPolyTime.fst encNat ExplicitTensorNetwork.encExplicitNetwork).comp
@@ -321,7 +335,7 @@ theorem root_polyTime : ComputableInPolyTime root ExplicitTensorNetwork.encContr
   exact (edges_polyTime.prod ((ComputableInPolyTime.const 0).prod
     ((ComputableInPolyTime.unary_add' edges_polyTime (ComputableInPolyTime.const 1)).prod
       (hp.prod ((modulus_polyTime.comp edges_polyTime).prod hr))))).prod
-    (rootNet_polyTime.comp network_polyTime)
+    ((rootNet_polyTime (encList encNat)).comp network_polyTime)
 
 /-- **The clock is polynomial-time**, from a capped input. -/
 theorem fuel_polyTime : ComputableInPolyTime fuel ExplicitTensorNetwork.encContractionInput
@@ -337,7 +351,7 @@ theorem fuel_polyTime : ComputableInPolyTime fuel ExplicitTensorNetwork.encContr
 constant coordinate of a returned root value modulo `2 ^ p` if the run returns a value tagged
 `0`, and direct summation otherwise. -/
 @[expose] noncomputable def fastValue (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) : ℕ :=
-  ((scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
+  ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
     (q.2.2.contraction % 2 ^ q.1)
     fun v => if v.1 = 0 then v.2.getD 0 0 % 2 ^ (ExplicitTensorNetwork.capPrecision q).1
       else q.2.2.contraction % 2 ^ q.1
@@ -345,23 +359,26 @@ constant coordinate of a returned root value modulo `2 ^ p` if the run returns a
 /-- **The machine is correct on well-formed inputs**, for every fuel. If the step of an active
 call is correct and well-formedness passes to the children, then on every input whose root is
 well-formed the result is the contraction modulo `2 ^ P`. -/
-theorem fastValue_eq {WF : Call → Prop} (hstep : StepCorrect mk WF) (hwf : WFChildren mk WF)
+theorem fastValue_eq {WF : Call (List ℕ) → Prop} (hstep : StepCorrect tableEntry mk WF)
+    (hwf : WFChildren mk WF)
     (q : ℕ × ℕ × ExplicitTensorNetwork ℕ)
     (hroot : WF (root (ExplicitTensorNetwork.capPrecision q))) :
     fastValue mk q = q.2.2.contraction % 2 ^ q.1 := by
   unfold fastValue
-  rcases hrun : (scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q) with _ | ⟨t, y⟩
+  rcases hrun : (scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q) with
+    _ | ⟨t, y⟩
   · rfl
   · simp only [Option.elim_some]
     split_ifs with ht
     · subst ht
-      have hy := eq_value_of_run mk (fuel := fuel) (root := root) rfl hrun
+      have hy := eq_value_of_run tableEntry mk (fuel := fuel) (root := root) rfl hrun
       have hval : val (ExplicitTensorNetwork.capPrecision q).1
           (modulus (ExplicitTensorNetwork.capPrecision q).2.2.numEdges) y =
           (rootNet (ExplicitTensorNetwork.capPrecision q).2.2).contraction fun t bs =>
             val (ExplicitTensorNetwork.capPrecision q).1
               (modulus (ExplicitTensorNetwork.capPrecision q).2.2.numEdges)
-              (VertexDesc.entry t bs) := hy ▸ val_value mk hstep hwf _ hroot
+              (VertexDesc.entry tableEntry t bs) :=
+        hy ▸ val_value tableEntry mk hstep hwf _ hroot
       rw [val_rootNet] at hval
       rw [getD_mod_of_val_eq (modulus_ne_nil _) hval]
       exact ExplicitTensorNetwork.contraction_mod_two_pow_min q.1 q.2.2
@@ -379,8 +396,9 @@ variable {mk}
 /-- **The clocked run** from a capped input, as one native machine, given polynomial-time
 components of the scheme. -/
 @[expose] noncomputable def runCertificate
-    (hpoly : (scheme mk).PolyTime encCall encFrame encValue) :
-    NativeCertificate ((scheme mk).run fuel root) ExplicitTensorNetwork.encContractionInput
+    (hpoly : (scheme tableEntry mk).PolyTime (encCall (encList encNat)) encFrame encValue) :
+    NativeCertificate ((scheme tableEntry mk).run fuel root)
+      ExplicitTensorNetwork.encContractionInput
       (encOption encValue) :=
   Scheme.certificate hpoly (leafCertificate mk) (NativeCertificate.ofPolyTime fuel_polyTime)
     (NativeCertificate.ofPolyTime root_polyTime)
@@ -409,7 +427,7 @@ theorem tag_polyTime :
 /-- **The fast machine**: cap the precision and run the recursion; on a value tagged `0`, read
 off its constant coordinate, and otherwise sum directly. It computes `fastValue`. -/
 @[expose] noncomputable def fastCertificate
-    (hpoly : (scheme mk).PolyTime encCall encFrame encValue) :
+    (hpoly : (scheme tableEntry mk).PolyTime (encCall (encList encNat)) encFrame encValue) :
     NativeCertificate (fastValue mk) encInput encNat :=
   (NativeCertificate.option
     ((runCertificate hpoly).comp
@@ -421,19 +439,20 @@ off its constant coordinate, and otherwise sum directly. It computes `fastValue`
         (NativeCertificate.ofPolyTime (ComputableInPolyTime.fst encInput encValue))))).congr
     fun q => by
       simp only [fastValue, Function.comp_apply]
-      cases (scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q) with
+      cases (scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q) with
       | none => rfl
       | some v => simp only [Option.elim_some, decide_eq_true_eq]
 
 /-- The time of the fast machine, unfolded: the capped run twice, the input, and the decoding or
 direct summation. -/
-theorem fastCertificate_time (hpoly : (scheme mk).PolyTime encCall encFrame encValue)
+theorem fastCertificate_time
+    (hpoly : (scheme tableEntry mk).PolyTime (encCall (encList encNat)) encFrame encValue)
     (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) :
     (fastCertificate hpoly).time q =
       2 * ((NativeCertificate.ofPolyTime ExplicitTensorNetwork.capPrecision_polyTime).time q +
         (runCertificate hpoly).time (ExplicitTensorNetwork.capPrecision q)) +
       (encInput q).length +
-      ((scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
+      ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
         (ExplicitTensorNetwork.directContractionBinaryCertificate.time q) fun v =>
           (NativeCertificate.ofPolyTime tag_polyTime).time (q, v) +
             if decide (v.1 = 0) = true then
@@ -443,13 +462,14 @@ theorem fastCertificate_time (hpoly : (scheme mk).PolyTime encCall encFrame encV
               ExplicitTensorNetwork.directContractionBinaryCertificate.time q := rfl
 
 /-- The space of the fast machine, unfolded. -/
-theorem fastCertificate_space (hpoly : (scheme mk).PolyTime encCall encFrame encValue)
+theorem fastCertificate_space
+    (hpoly : (scheme tableEntry mk).PolyTime (encCall (encList encNat)) encFrame encValue)
     (q : ℕ × ℕ × ExplicitTensorNetwork ℕ) :
     (fastCertificate hpoly).space q =
       2 * ((NativeCertificate.ofPolyTime ExplicitTensorNetwork.capPrecision_polyTime).space q +
         (runCertificate hpoly).space (ExplicitTensorNetwork.capPrecision q)) +
       (encInput q).length +
-      ((scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
+      ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
         (ExplicitTensorNetwork.directContractionBinaryCertificate.space q) fun v =>
           (NativeCertificate.ofPolyTime tag_polyTime).space (q, v) +
             if decide (v.1 = 0) = true then
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionPolyTime.lean
index 4d83637e2..a96d7467e 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionPolyTime.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionPolyTime.lean
@@ -36,10 +36,12 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeRadix
 /-!
 # The components of the native contraction recursion in polynomial time
 
-The scheme `Cslib.Circuits.Frontier.FastContraction.scheme mk` of the contraction recursion of
+The scheme `Cslib.Circuits.Frontier.FastContraction.scheme ev mk` of the contraction recursion of
 [OpenAI2026ETH] has polynomial-time components (`Cslib.GenericRAM.StackRecursion.Scheme.PolyTime`)
-for the encodings `FastContraction.encCall`, `encFrame` and `encValue` whenever the child builder
-`mk` is polynomial-time (`FastContraction.scheme_polyTime`). The native child builder is
+for the encodings `FastContraction.encCall encT`, `encFrame` and `encValue` whenever the child
+builder `mk` is polynomial-time (`FastContraction.scheme_polyTime`), for every type `T` of root
+descriptors with an encoding `encT` and every entry procedure `ev`: the leaf test does not
+evaluate an entry, and the descriptors are only copied. The native child builder is
 (`FastContraction.nativeMk_polyTime`), so the scheme of `FastContraction.nativeMk` has
 polynomial-time components (`FastContraction.scheme_nativeMk_polyTime`).
 
@@ -190,53 +192,57 @@ namespace Cslib.Circuits.Frontier.FastContraction
 open GaloisRingArith ChildCursor NativeRecovery ContractionSchedule NativeChild
   Cslib.GenericRAM Cslib.GenericRAM.StackRecursion
 
+variable {T : Type} {encT : T ↪ List Bool}
+
 /-! ### The parameters of a call -/
 
 /-- The scale is polynomial-time. -/
-theorem scale_polyTime : ComputableInPolyTime Call.scale encCall encUnary := by
+theorem scale_polyTime : ComputableInPolyTime Call.scale (encCall encT) encUnary := by
   unfold Call.scale; fun_prop
 
 /-- The edge bound is polynomial-time. -/
-theorem bound_polyTime : ComputableInPolyTime Call.bound encCall encUnary := by
+theorem bound_polyTime : ComputableInPolyTime Call.bound (encCall encT) encUnary := by
   unfold Call.bound; fun_prop
 
 /-- The precision is polynomial-time. -/
-theorem prec_polyTime : ComputableInPolyTime Call.prec encCall encUnary := by
+theorem prec_polyTime : ComputableInPolyTime Call.prec (encCall encT) encUnary := by
   unfold Call.prec; fun_prop
 
 /-- The coefficients of the modulus are polynomial-time. -/
-theorem fl_polyTime : ComputableInPolyTime Call.fl encCall (encList encNat) := by
+theorem fl_polyTime : ComputableInPolyTime Call.fl (encCall encT) (encList encNat) := by
   unfold Call.fl; fun_prop
 
 /-- The number of rows is polynomial-time. -/
-theorem rows_polyTime : ComputableInPolyTime Call.rows encCall encNat := by
+theorem rows_polyTime : ComputableInPolyTime Call.rows (encCall encT) encNat := by
   unfold Call.rows; fun_prop
 
 /-- The network is polynomial-time. -/
 theorem net_polyTime :
-    ComputableInPolyTime Call.net encCall (DescribedNetwork.encDescribed VertexDesc.enc) := by
+    ComputableInPolyTime Call.net (encCall encT)
+      (DescribedNetwork.encDescribed (VertexDesc.enc encT)) := by
   unfold Call.net; fun_prop
 
 /-- The number of edges is polynomial-time, in unary. -/
-theorem edges_polyTime : ComputableInPolyTime Call.edges encCall encUnary :=
+theorem edges_polyTime : ComputableInPolyTime Call.edges (encCall encT) encUnary :=
   DescribedNetwork.numEdges_polyTime.comp net_polyTime
 
 /-- The vertices are polynomial-time. -/
-theorem vertices_polyTime : ComputableInPolyTime (fun x : Call => x.net.vertices) encCall
-    (encList (encPair (encList encNat) VertexDesc.enc)) :=
+theorem vertices_polyTime : ComputableInPolyTime (fun x : Call T => x.net.vertices) (encCall encT)
+    (encList (encPair (encList encNat) (VertexDesc.enc encT))) :=
   DescribedNetwork.vertices_polyTime.comp net_polyTime
 
 /-! ### The schedule of a call -/
 
 /-- The number of label coordinates is polynomial-time. -/
-theorem slots_polyTime : ComputableInPolyTime slots encCall encUnary :=
-  slotBits_polyTime.comp (scale_polyTime.prod depth_polyTime)
+theorem slots_polyTime : ComputableInPolyTime slots (encCall encT) encUnary :=
+  slotBits_polyTime.comp (scale_polyTime.prod (depth_polyTime encT))
 
 /-- `2 ^ a ≤ s + 1` at every call. -/
-theorem two_pow_slots_le (x : Call) : 2 ^ slots x ≤ x.scale + 1 := two_pow_slotBits_le _ _
+theorem two_pow_slots_le (x : Call T) : 2 ^ slots x ≤ x.scale + 1 := two_pow_slotBits_le _ _
 
 /-- The number `2 ^ a` of slots is polynomial-time, in unary. -/
-theorem twoPowSlots_polyTime : ComputableInPolyTime (fun x => 2 ^ slots x) encCall encUnary :=
+theorem twoPowSlots_polyTime : ComputableInPolyTime (fun x => 2 ^ slots x)
+    (encCall encT) encUnary :=
   ComputableInPolyTime.binary_to_unary_bounded
     (ComputableInPolyTime.binary_two_pow.comp slots_polyTime)
     (ComputableInPolyTime.unary_add' scale_polyTime (ComputableInPolyTime.const 1))
@@ -244,27 +250,27 @@ theorem twoPowSlots_polyTime : ComputableInPolyTime (fun x => 2 ^ slots x) encCa
 
 /-- The number `2 ^ (a + 1)` of grid indices is polynomial-time, in unary. -/
 theorem twoPowSlotsSucc_polyTime :
-    ComputableInPolyTime (fun x => 2 ^ (slots x + 1)) encCall encUnary :=
+    ComputableInPolyTime (fun x => 2 ^ (slots x + 1)) (encCall encT) encUnary :=
   (ComputableInPolyTime.unary_add' twoPowSlots_polyTime twoPowSlots_polyTime).of_enc_eq fun x => by
     rw [pow_succ, mul_two]
 
 /-- The number of levels is polynomial-time. -/
-theorem levels_polyTime : ComputableInPolyTime levels encCall encUnary :=
-  taper_polyTime.comp (scale_polyTime.prod depth_polyTime)
+theorem levels_polyTime : ComputableInPolyTime levels (encCall encT) encUnary :=
+  taper_polyTime.comp (scale_polyTime.prod (depth_polyTime encT))
 
 /-- The multiplicity step is polynomial-time. -/
-theorem step_polyTime : ComputableInPolyTime step encCall encUnary :=
-  taperStep_polyTime.comp (scale_polyTime.prod (depth_polyTime.prod edges_polyTime))
+theorem step_polyTime : ComputableInPolyTime step (encCall encT) encUnary :=
+  taperStep_polyTime.comp (scale_polyTime.prod ((depth_polyTime encT).prod edges_polyTime))
 
 /-- The number of interpolation points is polynomial-time, in unary. -/
-theorem numPoints_polyTime : ComputableInPolyTime numPoints encCall encUnary :=
+theorem numPoints_polyTime : ComputableInPolyTime numPoints (encCall encT) encUnary :=
   ComputableInPolyTime.unary_add' (ComputableInPolyTime.unary_mul' edges_polyTime
     (ComputableInPolyTime.unary_sub' (ComputableInPolyTime.unary_mul'
       (ComputableInPolyTime.const 2) twoPowSlots_polyTime) (ComputableInPolyTime.const 1)))
     (ComputableInPolyTime.const 1)
 
 /-- The shift `Δ'` is polynomial-time, in unary. -/
-theorem shift_polyTime : ComputableInPolyTime shift encCall encUnary :=
+theorem shift_polyTime : ComputableInPolyTime shift (encCall encT) encUnary :=
   ComputableInPolyTime.unary_add' (ComputableInPolyTime.unary_add'
     (ComputableInPolyTime.unary_mul' (ComputableInPolyTime.unary_mul'
       (ComputableInPolyTime.unary_mul'
@@ -277,7 +283,7 @@ theorem shift_polyTime : ComputableInPolyTime shift encCall encUnary :=
       (ComputableInPolyTime.unary_add' slots_polyTime (ComputableInPolyTime.const 1)))
 
 /-- The common precision `N = p + Δ'` is polynomial-time, in unary. -/
-theorem wide_polyTime : ComputableInPolyTime wide encCall encUnary :=
+theorem wide_polyTime : ComputableInPolyTime wide (encCall encT) encUnary :=
   ComputableInPolyTime.unary_add' prec_polyTime shift_polyTime
 
 /-! ### Nodes, levels and precisions -/
@@ -290,14 +296,14 @@ private theorem twoVal_le (b d : ℕ) : twoVal b d ≤ b := by
   · exact (List.length_filter_le _ _).trans (List.length_range (n := b)).le
 
 /-- Every level is at most `a + 1`. -/
-theorem level_le (x : Call) (k : ℕ) : level x k ≤ slots x + 1 := twoVal_le _ _
+theorem level_le (x : Call T) (k : ℕ) : level x k ≤ slots x + 1 := twoVal_le _ _
 
 /-- The level of a grid index is polynomial-time, in unary. -/
 theorem level_polyTime :
-    ComputableInPolyTime (fun q : Call × ℕ => level q.1 q.2) (encPair encCall encUnary)
+    ComputableInPolyTime (fun q : Call T × ℕ => level q.1 q.2) (encPair (encCall encT) encUnary)
       encUnary := by
-  have hx := ComputableInPolyTime.fst encCall encUnary
-  have hk := ComputableInPolyTime.snd encCall encUnary
+  have hx := ComputableInPolyTime.fst (encCall encT) encUnary
+  have hk := ComputableInPolyTime.snd (encCall encT) encUnary
   have hL := twoPowSlots_polyTime.comp hx
   have h := computableInPolyTime_twoVal
     (ComputableInPolyTime.unary_add' (slots_polyTime.comp hx) (ComputableInPolyTime.const 1))
@@ -306,49 +312,52 @@ theorem level_polyTime :
   exact h
 
 /-- The nodes of positive multiplicity are polynomial-time, as unary grid indices. -/
-theorem nodes_polyTime : ComputableInPolyTime nodes encCall (encList encUnary) := by
-  have hx := ComputableInPolyTime.fst encCall encUnary
-  have hk := ComputableInPolyTime.snd encCall encUnary
+theorem nodes_polyTime : ComputableInPolyTime nodes (encCall encT) (encList encUnary) := by
+  have hx := ComputableInPolyTime.fst (encCall encT) encUnary
+  have hk := ComputableInPolyTime.snd (encCall encT) encUnary
   have hL := twoPowSlots_polyTime.comp hx
   have hmult := computableInPolyTime_mult (slots_polyTime.comp hx) hL (levels_polyTime.comp hx)
     (step_polyTime.comp hx) hk
-  have htest : ComputableInPolyTime (fun q : Call × ℕ =>
+  have htest : ComputableInPolyTime (fun q : Call T × ℕ =>
       decide (q.2 ≠ 2 ^ slots q.1 ∧ 0 < mult (slots q.1) (levels q.1) (step q.1) q.2))
-      (encPair encCall encUnary) encBool :=
+      (encPair (encCall encT) encUnary) encBool :=
     (ComputableInPolyTime.bool_and' (ComputableInPolyTime.bool_not.comp
       (ComputableInPolyTime.decide_eq' hk hL))
       (ComputableInPolyTime.unary_lt' (ComputableInPolyTime.const 0) hmult)).of_enc_eq fun q => by
       simp only [Function.comp_apply, Bool.decide_and, decide_not]
   have h := ComputableInPolyTime.filterWithInput
-    (test := fun (x : Call) k =>
+    (test := fun (x : Call T) k =>
       decide (k ≠ 2 ^ slots x ∧ 0 < mult (slots x) (levels x) (step x) k))
     (ComputableInPolyTime.range.comp twoPowSlotsSucc_polyTime) htest
   exact h
 
 /-- The grid index of the `i`-th node is polynomial-time, in unary. -/
 theorem node_polyTime :
-    ComputableInPolyTime (fun q : Call × ℕ => (nodes q.1).getD q.2 0) (encPair encCall encUnary)
+    ComputableInPolyTime (fun q : Call T × ℕ => (nodes q.1).getD q.2 0)
+      (encPair (encCall encT) encUnary)
       encUnary := by
   have h := ComputableInPolyTime.listGetDWithInput
-    (nodes_polyTime.comp (ComputableInPolyTime.fst encCall encUnary))
-    (ComputableInPolyTime.snd encCall encUnary) 0
+    (nodes_polyTime.comp (ComputableInPolyTime.fst (encCall encT) encUnary))
+    (ComputableInPolyTime.snd (encCall encT) encUnary) 0
   exact h
 
 /-- The level of the `i`-th node is polynomial-time, in unary. -/
 theorem nodeLevel_polyTime :
-    ComputableInPolyTime (fun q : Call × ℕ => level q.1 ((nodes q.1).getD q.2 0))
-      (encPair encCall encUnary) encUnary := by
-  have h := level_polyTime.comp ((ComputableInPolyTime.fst encCall encUnary).prod node_polyTime)
+    ComputableInPolyTime (fun q : Call T × ℕ => level q.1 ((nodes q.1).getD q.2 0))
+      (encPair (encCall encT) encUnary) encUnary := by
+  have h := level_polyTime.comp
+      ((ComputableInPolyTime.fst (encCall encT) encUnary).prod node_polyTime)
   exact h
 
 /-- The number `2 ^ (v₂ t + 1)` of tiles of the `i`-th node is polynomial-time, in unary. -/
 theorem tiles_polyTime :
-    ComputableInPolyTime (fun q : Call × ℕ => 2 ^ (level q.1 ((nodes q.1).getD q.2 0) + 1))
-      (encPair encCall encUnary) encUnary := by
+    ComputableInPolyTime (fun q : Call T × ℕ => 2 ^ (level q.1 ((nodes q.1).getD q.2 0) + 1))
+      (encPair (encCall encT) encUnary) encUnary := by
   have hv := ComputableInPolyTime.binary_two_pow.comp
-    (ComputableInPolyTime.unary_add' nodeLevel_polyTime (ComputableInPolyTime.const 1))
+    (ComputableInPolyTime.unary_add' (nodeLevel_polyTime (encT := encT))
+      (ComputableInPolyTime.const 1))
   have hb := ComputableInPolyTime.unary_mul' (ComputableInPolyTime.const 4)
-    (twoPowSlots_polyTime.comp (ComputableInPolyTime.fst encCall encUnary))
+    (twoPowSlots_polyTime.comp (ComputableInPolyTime.fst (encCall encT) encUnary))
   have h := ComputableInPolyTime.binary_to_unary_bounded hv hb fun q => by
     simp only [Function.comp_apply]
     calc 2 ^ (level q.1 ((nodes q.1).getD q.2 0) + 1) ≤ 2 ^ (slots q.1 + 2) :=
@@ -359,12 +368,12 @@ theorem tiles_polyTime :
 
 /-- **The precision of the `i`-th node is polynomial-time**, in unary. -/
 theorem nodePrec_polyTime :
-    ComputableInPolyTime (fun q : Call × ℕ => nodePrec q.1 q.2) (encPair encCall encUnary)
+    ComputableInPolyTime (fun q : Call T × ℕ => nodePrec q.1 q.2) (encPair (encCall encT) encUnary)
       encUnary := by
-  have hx := ComputableInPolyTime.fst encCall encUnary
+  have hx := ComputableInPolyTime.fst (encCall encT) encUnary
   have hpow : ComputableInPolyTime
-      (fun q : Call × ℕ => 2 ^ (slots q.1 - level q.1 ((nodes q.1).getD q.2 0)))
-      (encPair encCall encUnary) encUnary := by
+      (fun q : Call T × ℕ => 2 ^ (slots q.1 - level q.1 ((nodes q.1).getD q.2 0)))
+      (encPair (encCall encT) encUnary) encUnary := by
     have h := ComputableInPolyTime.binary_to_unary_bounded (ComputableInPolyTime.binary_two_pow.comp
       (ComputableInPolyTime.unary_sub' (slots_polyTime.comp hx) nodeLevel_polyTime))
       (twoPowSlots_polyTime.comp hx)
@@ -381,47 +390,49 @@ theorem nodePrec_polyTime :
 /-! ### The packing and the weights -/
 
 /-- The capped number of rows is polynomial-time, in unary. -/
-theorem rowCap_polyTime : ComputableInPolyTime rowCap encCall encUnary :=
+theorem rowCap_polyTime : ComputableInPolyTime rowCap (encCall encT) encUnary :=
   (ComputableInPolyTime.binary_min_unary.comp
     (((ComputableInPolyTime.length_list _).comp vertices_polyTime).prod rows_polyTime)).of_enc_eq
     fun x => by simp only [Function.comp_apply, rowCap, min_comm]
 
 /-- **The packing is polynomial-time** on every call. -/
-theorem packing_polyTime : ComputableInPolyTime packing encCall PacketPacking.encNativePacking :=
+theorem packing_polyTime : ComputableInPolyTime packing
+    (encCall encT) PacketPacking.encNativePacking :=
   computableInPolyTime_nativeParentPacking rowCap_polyTime slots_polyTime net_polyTime
 
 /-- **The number of packets is polynomial-time**, in unary, on every call: there are at most
 `M (2 ^ a) ^ 12 ≤ M (s + 1) ^ 12` of them (`NativeChild.numPackets_nativeParentPacking_le`). -/
 theorem packets_polyTime :
-    ComputableInPolyTime (fun x : Call => (packing x).2.1) encCall encUnary :=
+    ComputableInPolyTime (fun x : Call T => (packing x).2.1) (encCall encT) encUnary :=
   computableInPolyTime_numPackets_nativeParentPacking rowCap_polyTime slots_polyTime
     twoPowSlots_polyTime net_polyTime
 
 /-- **The weights of the modes of the `i`-th node are polynomial-time.** -/
 theorem weights_polyTime :
-    ComputableInPolyTime (fun q : Call × ℕ => weights q.1 q.2) (encPair encCall encUnary)
+    ComputableInPolyTime (fun q : Call T × ℕ => weights q.1 q.2) (encPair (encCall encT) encUnary)
       (encList encNat) := by
-  have hx := ComputableInPolyTime.fst encCall encUnary
-  have hp := nodePrec_polyTime
+  have hx := ComputableInPolyTime.fst (encCall encT) encUnary
+  have hp := nodePrec_polyTime (encT := encT)
   have hlen := ComputableInPolyTime.unary_mul' (packets_polyTime.comp hx)
     (ComputableInPolyTime.unary_mul' tiles_polyTime hp)
-  have hj := ComputableInPolyTime.snd (encPair encCall encUnary) encUnary
-  have hpj := hp.comp (ComputableInPolyTime.fst (encPair encCall encUnary) encUnary)
-  have hf : ComputableInPolyTime (fun r : (Call × ℕ) × ℕ => r.2 % nodePrec r.1.1 r.1.2 + 1)
-      (encPair (encPair encCall encUnary) encUnary) encNat := by
+  have hj := ComputableInPolyTime.snd (encPair (encCall encT) encUnary) encUnary
+  have hpj := hp.comp (ComputableInPolyTime.fst (encPair (encCall encT) encUnary) encUnary)
+  have hf : ComputableInPolyTime (fun r : (Call T × ℕ) × ℕ => r.2 % nodePrec r.1.1 r.1.2 + 1)
+      (encPair (encPair (encCall encT) encUnary) encUnary) encNat := by
     have h := ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.unary_add'
       (ComputableInPolyTime.unary_mod.comp (hj.prod hpj)) (ComputableInPolyTime.const 1))
     exact h
   have h := ComputableInPolyTime.mapWithInput
-    (f := fun (q : Call × ℕ) j => j % nodePrec q.1 q.2 + 1)
+    (f := fun (q : Call T × ℕ) j => j % nodePrec q.1 q.2 + 1)
     (ComputableInPolyTime.range.comp hlen) hf
   exact h
 
 /-- The number of modes of the `i`-th node is polynomial-time, in unary. -/
 theorem weightsLength_polyTime :
-    ComputableInPolyTime (fun q : Call × ℕ => (weights q.1 q.2).length) (encPair encCall encUnary)
+    ComputableInPolyTime (fun q : Call T × ℕ => (weights q.1 q.2).length)
+      (encPair (encCall encT) encUnary)
       encUnary := by
-  have h := (ComputableInPolyTime.length_list _).comp weights_polyTime
+  have h := (ComputableInPolyTime.length_list _).comp (weights_polyTime (encT := encT))
   exact h
 
 /-! ### Points and the table -/
@@ -444,46 +455,47 @@ theorem digits_polyTime :
   exact h
 
 /-- **The interpolation points are polynomial-time.** -/
-theorem points_polyTime : ComputableInPolyTime points encCall (encList (encList encNat)) := by
-  have hf : ComputableInPolyTime (fun r : Call × ℕ => digits r.1.fl.length r.2)
-      (encPair encCall encUnary) (encList encNat) := by
+theorem points_polyTime : ComputableInPolyTime points (encCall encT)
+    (encList (encList encNat)) := by
+  have hf : ComputableInPolyTime (fun r : Call T × ℕ => digits r.1.fl.length r.2)
+      (encPair (encCall encT) encUnary) (encList encNat) := by
     have h := digits_polyTime.comp ((((ComputableInPolyTime.length_list _).comp fl_polyTime).comp
-      (ComputableInPolyTime.fst encCall encUnary)).prod (ComputableInPolyTime.snd _ _))
+      (ComputableInPolyTime.fst (encCall encT) encUnary)).prod (ComputableInPolyTime.snd _ _))
     exact h
-  have h := ComputableInPolyTime.mapWithInput (f := fun (x : Call) k => digits x.fl.length k)
+  have h := ComputableInPolyTime.mapWithInput (f := fun (x : Call T) k => digits x.fl.length k)
     (ComputableInPolyTime.range.comp numPoints_polyTime) hf
   exact h
 
 /-- **The table of native recovery is polynomial-time**, from a call and the stored values. -/
 theorem table_polyTime :
-    ComputableInPolyTime (fun q : Call × List (List ℕ) => table q.1 q.2)
-      (encPair encCall (encList (encList encNat))) (encList (encList (encList encNat))) := by
-  let e := encPair encCall (encList (encList encNat))
-  have hx := ComputableInPolyTime.fst encCall (encList (encList encNat))
+    ComputableInPolyTime (fun q : Call T × List (List ℕ) => table q.1 q.2)
+      (encPair (encCall encT) (encList (encList encNat))) (encList (encList (encList encNat))) := by
+  let e := encPair (encCall encT) (encList (encList encNat))
+  have hx := ComputableInPolyTime.fst (encCall encT) (encList (encList encNat))
   have hx' := hx.comp (ComputableInPolyTime.fst e encUnary)
-  have hV' := (ComputableInPolyTime.snd encCall (encList (encList encNat))).comp
+  have hV' := (ComputableInPolyTime.snd (encCall encT) (encList (encList encNat))).comp
     (ComputableInPolyTime.fst e encUnary)
   have hk := ComputableInPolyTime.snd e encUnary
   have hn := numPoints_polyTime.comp hx'
   have hmem := ComputableInPolyTime.decide_mem (nodes_polyTime.comp hx') hk
   have hidx := ComputableInPolyTime.idxOfWithInput (nodes_polyTime.comp hx') hk
-  have hdrop : ComputableInPolyTime (fun r : (Call × List (List ℕ)) × ℕ =>
+  have hdrop : ComputableInPolyTime (fun r : (Call T × List (List ℕ)) × ℕ =>
       r.1.2.drop ((nodes r.1.1).idxOf r.2 * numPoints r.1.1)) (encPair e encUnary)
       (encList (encList encNat)) :=
     .of_tidy (ComputableTidilyInPolyTime.listDropWithInput hV'.tidy
       (ComputableInPolyTime.unary_mul' hidx hn).tidy)
-  have htake : ComputableInPolyTime (fun r : (Call × List (List ℕ)) × ℕ =>
+  have htake : ComputableInPolyTime (fun r : (Call T × List (List ℕ)) × ℕ =>
       (r.1.2.drop ((nodes r.1.1).idxOf r.2 * numPoints r.1.1)).take (numPoints r.1.1))
       (encPair e encUnary) (encList (encList encNat)) :=
     .of_tidy (ComputableTidilyInPolyTime.listTakeWithInput hdrop.tidy hn.tidy)
-  have hf : ComputableInPolyTime (fun r : (Call × List (List ℕ)) × ℕ =>
+  have hf : ComputableInPolyTime (fun r : (Call T × List (List ℕ)) × ℕ =>
       if r.2 ∈ nodes r.1.1 then
         (r.1.2.drop ((nodes r.1.1).idxOf r.2 * numPoints r.1.1)).take (numPoints r.1.1)
       else []) (encPair e encUnary) (encList (encList encNat)) := by
     have h := ComputableInPolyTime.ite hmem htake (ComputableInPolyTime.const [])
     refine h.of_enc_eq fun r => ?_
     simp only [Function.comp_apply, decide_eq_true_eq]
-  have h := ComputableInPolyTime.mapWithInput (f := fun (q : Call × List (List ℕ)) k =>
+  have h := ComputableInPolyTime.mapWithInput (f := fun (q : Call T × List (List ℕ)) k =>
       if k ∈ nodes q.1 then
         (q.2.drop ((nodes q.1).idxOf k * numPoints q.1)).take (numPoints q.1) else [])
     (ComputableInPolyTime.range.comp (twoPowSlotsSucc_polyTime.comp hx)) hf
@@ -492,7 +504,7 @@ theorem table_polyTime :
 /-! ### Active calls -/
 
 /-- Whether a call is active, as a conjunction of tests. -/
-theorem active_eq (x : Call) : active x =
+theorem active_eq (x : Call T) : active x =
     (decide (leafSize x.scale < x.edges) && decide (1 ≤ levels x) && decide (levels x ≤ x.edges) &&
       decide (levels x ≤ slots x) &&
       x.net.vertices.all (fun v => decide (v.1.length ≤ degreeBound x.scale)) &&
@@ -500,9 +512,10 @@ theorem active_eq (x : Call) : active x =
   simp only [active, Bool.decide_and, List.all_eq, decide_eq_true_eq, Bool.and_assoc]
 
 /-- **Whether a call is active is polynomial-time.** -/
-theorem active_polyTime : ComputableInPolyTime active encCall encBool := by
-  have hdeg : ComputableInPolyTime (fun x : Call =>
-      x.net.vertices.all (fun v => decide (v.1.length ≤ degreeBound x.scale))) encCall encBool :=
+theorem active_polyTime : ComputableInPolyTime active (encCall encT) encBool := by
+  have hdeg : ComputableInPolyTime (fun x : Call T =>
+      x.net.vertices.all (fun v => decide (v.1.length ≤ degreeBound x.scale)))
+        (encCall encT) encBool :=
     ComputableInPolyTime.allWithInput vertices_polyTime
       (ComputableInPolyTime.binary_le' (ComputableInPolyTime.unary_to_binary.comp
         ((ComputableInPolyTime.length_list _).comp ((ComputableInPolyTime.fst _ _).comp
@@ -528,27 +541,28 @@ theorem active_polyTime : ComputableInPolyTime active encCall encBool := by
 
 section Scheme
 
-variable (mk : Call → State → ℕ × DescribedNetwork VertexDesc)
+variable (ev : T → List Bool → List ℕ) (mk : Call T → State → ℕ × DescribedNetwork (VertexDesc T))
 
 /-- **The leaf test is polynomial-time.** -/
-theorem isLeaf_polyTime : ComputableInPolyTime (scheme mk).isLeaf encCall encBool := by
-  have h := ComputableInPolyTime.bool_not.comp active_polyTime
+theorem isLeaf_polyTime : ComputableInPolyTime (scheme ev mk).isLeaf (encCall encT) encBool := by
+  have h := ComputableInPolyTime.bool_not.comp (active_polyTime (encT := encT))
   exact h
 
 /-- **The initial accumulator is polynomial-time.** -/
-theorem start_polyTime : ComputableInPolyTime (scheme mk).start encCall encFrame := by
-  have hlen : ComputableInPolyTime (fun x : Call => (weights x 0).length) encCall encUnary := by
+theorem start_polyTime : ComputableInPolyTime (scheme ev mk).start (encCall encT) encFrame := by
+  have hlen : ComputableInPolyTime (fun x : Call T => (weights x 0).length)
+      (encCall encT) encUnary := by
     have h := weightsLength_polyTime.comp
-      ((ComputableInPolyTime.id' (encIn := encCall)).prod (ComputableInPolyTime.const 0))
+      ((ComputableInPolyTime.id' (encIn := (encCall encT))).prod (ComputableInPolyTime.const 0))
     exact h
-  have hst : ComputableInPolyTime (fun x : Call => cursorStart (weights x)) encCall
+  have hst : ComputableInPolyTime (fun x : Call T => cursorStart (weights x)) (encCall encT)
       (encPair encUnary (encPair encUnary (encPair (encList encNat) encUnary))) :=
     (ComputableInPolyTime.const 0).prod ((ComputableInPolyTime.const 0).prod
       ((ComputableInPolyTime.replicate hlen (ComputableInPolyTime.const 0)).prod
         (ComputableInPolyTime.const 0)))
-  have hst' : ComputableInPolyTime (fun x : Call => cursorStart (weights x)) encCall
+  have hst' : ComputableInPolyTime (fun x : Call T => cursorStart (weights x)) (encCall encT)
       ChildCursor.encState := hst
-  have h : ComputableInPolyTime (scheme mk).start encCall
+  have h : ComputableInPolyTime (scheme ev mk).start (encCall encT)
       (encPair (encOption ChildCursor.encState)
         (encPair (encList encNat) (encPair (encList encNat) (encList (encList encNat))))) :=
     ((ComputableInPolyTime.optionSome _).comp hst').prod
@@ -576,26 +590,27 @@ private theorem stateGroup_polyTime :
     ComputableInPolyTime (fun c : State => c.2.2.2) ChildCursor.encState encUnary := by
   unfold ChildCursor.encState; fun_prop
 
-variable {mk}
+variable {ev mk}
 
 /-- **The child call at a cursor state is polynomial-time**, given a polynomial-time builder. -/
 theorem child_polyTime
-    (hmk : ComputableInPolyTime (fun q : Call × State => mk q.1 q.2)
-      (encPair encCall ChildCursor.encState)
-      (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc))) :
-    ComputableInPolyTime (fun q : Call × State => child q.1 mk q.2)
-      (encPair encCall ChildCursor.encState) encCall := by
-  have hx := ComputableInPolyTime.fst encCall ChildCursor.encState
-  have ht := stateNode_polyTime.comp (ComputableInPolyTime.snd encCall ChildCursor.encState)
-  have hprec : ComputableInPolyTime (fun q : Call × State => nodePrec q.1 q.2.1)
-      (encPair encCall ChildCursor.encState) encUnary := by
+    (hmk : ComputableInPolyTime (fun q : Call T × State => mk q.1 q.2)
+      (encPair (encCall encT) ChildCursor.encState)
+      (encPair encNat (DescribedNetwork.encDescribed (VertexDesc.enc encT)))) :
+    ComputableInPolyTime (fun q : Call T × State => child q.1 mk q.2)
+      (encPair (encCall encT) ChildCursor.encState) (encCall encT) := by
+  have hx := ComputableInPolyTime.fst (encCall encT) ChildCursor.encState
+  have ht := stateNode_polyTime.comp (ComputableInPolyTime.snd (encCall encT) ChildCursor.encState)
+  have hprec : ComputableInPolyTime (fun q : Call T × State => nodePrec q.1 q.2.1)
+      (encPair (encCall encT) ChildCursor.encState) encUnary := by
     have h := nodePrec_polyTime.comp (hx.prod ht)
     exact h
-  have h : ComputableInPolyTime (fun q : Call × State => child q.1 mk q.2)
-      (encPair encCall ChildCursor.encState)
+  have h : ComputableInPolyTime (fun q : Call T × State => child q.1 mk q.2)
+      (encPair (encCall encT) ChildCursor.encState)
       (encPair (encPair encUnary (encPair encUnary (encPair encUnary (encPair encUnary
-        (encPair (encList encNat) encNat))))) (DescribedNetwork.encDescribed VertexDesc.enc)) :=
-    ((scale_polyTime.comp hx).prod ((ComputableInPolyTime.unary_add' (depth_polyTime.comp hx)
+        (encPair (encList encNat) encNat)))))
+          (DescribedNetwork.encDescribed (VertexDesc.enc encT))) :=
+    ((scale_polyTime.comp hx).prod ((ComputableInPolyTime.unary_add' ((depth_polyTime encT).comp hx)
       (ComputableInPolyTime.const 1)).prod ((edges_polyTime.comp hx).prod (hprec.prod
         ((fl_polyTime.comp hx).prod ((ComputableInPolyTime.fst _ _).comp hmk)))))).prod
       ((ComputableInPolyTime.snd _ _).comp hmk)
@@ -603,133 +618,139 @@ theorem child_polyTime
 
 /-- **Child generation is polynomial-time**, given a polynomial-time builder. -/
 theorem next_polyTime
-    (hmk : ComputableInPolyTime (fun q : Call × State => mk q.1 q.2)
-      (encPair encCall ChildCursor.encState)
-      (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc))) :
-    ComputableInPolyTime (fun p : Call × Frame => (scheme mk).next p.1 p.2)
-      (encPair encCall encFrame) (encOption encCall) := by
-  have hc : ComputableInPolyTime (fun p : Call × Frame => p.2.1) (encPair encCall encFrame)
+    (hmk : ComputableInPolyTime (fun q : Call T × State => mk q.1 q.2)
+      (encPair (encCall encT) ChildCursor.encState)
+      (encPair encNat (DescribedNetwork.encDescribed (VertexDesc.enc encT)))) :
+    ComputableInPolyTime (fun p : Call T × Frame => (scheme ev mk).next p.1 p.2)
+      (encPair (encCall encT) encFrame) (encOption (encCall encT)) := by
+  have hc : ComputableInPolyTime (fun p : Call T × Frame => p.2.1) (encPair (encCall encT) encFrame)
       (encOption ChildCursor.encState) :=
-    (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd encCall encFrame)
-  have hbody : ComputableInPolyTime (fun r : (Call × Frame) × State => some (child r.1.1 mk r.2))
-      (encPair (encPair encCall encFrame) ChildCursor.encState) (encOption encCall) := by
-    have h := (ComputableInPolyTime.optionSome encCall).comp ((child_polyTime hmk).comp
-      (((ComputableInPolyTime.fst encCall encFrame).comp (ComputableInPolyTime.fst _ _)).prod
+    (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd (encCall encT) encFrame)
+  have hbody : ComputableInPolyTime (fun r : (Call T × Frame) × State => some (child r.1.1 mk r.2))
+      (encPair (encPair (encCall encT) encFrame) ChildCursor.encState)
+        (encOption (encCall encT)) := by
+    have h := (ComputableInPolyTime.optionSome (encCall encT)).comp ((child_polyTime hmk).comp
+      (((ComputableInPolyTime.fst (encCall encT) encFrame).comp (ComputableInPolyTime.fst _ _)).prod
         (ComputableInPolyTime.snd _ _)))
     exact h
   have h := ComputableInPolyTime.optionElimWithInput
-    (body := fun (p : Call × Frame) (c : State) => some (child p.1 mk c)) hc
-    (ComputableInPolyTime.const (encOut := encOption encCall) none) hbody
+    (body := fun (p : Call T × Frame) (c : State) => some (child p.1 mk c)) hc
+    (ComputableInPolyTime.const (encOut := encOption (encCall encT)) none) hbody
   refine h.of_enc_eq fun p => ?_
   rcases p with ⟨x, _ | c, acc⟩ <;> rfl
 
-variable (mk)
+variable (ev mk)
 
 /-- The inputs of `absorb` at a cursor state: the call, its frame, the child's value and the
 state. -/
-private abbrev AbsorbIn : Type := ((Call × Frame) × (ℕ × List ℕ)) × State
+private abbrev AbsorbIn (T : Type) : Type := ((Call T × Frame) × (ℕ × List ℕ)) × State
 
 /-- The encoding of `AbsorbIn`. -/
-private abbrev encAbsorbIn : AbsorbIn ↪ List Bool :=
-  encPair (encPair (encPair encCall encFrame) encValue) ChildCursor.encState
+private abbrev encAbsorbIn (encT : T ↪ List Bool) : AbsorbIn T ↪ List Bool :=
+  encPair (encPair (encPair (encCall encT) encFrame) encValue) ChildCursor.encState
 
 /-- The call of an input of `absorb`. -/
 private theorem absorbCall_polyTime :
-    ComputableInPolyTime (fun r : AbsorbIn => r.1.1.1) encAbsorbIn encCall :=
-  (ComputableInPolyTime.fst encCall encFrame).comp ((ComputableInPolyTime.fst _ encValue).comp
+    ComputableInPolyTime (fun r : AbsorbIn T => r.1.1.1) (encAbsorbIn encT) (encCall encT) :=
+  (ComputableInPolyTime.fst (encCall encT) encFrame).comp
+    ((ComputableInPolyTime.fst _ encValue).comp
     (ComputableInPolyTime.fst _ ChildCursor.encState))
 
 /-- The state of an input of `absorb`. -/
 private theorem absorbState_polyTime :
-    ComputableInPolyTime (fun r : AbsorbIn => r.2) encAbsorbIn ChildCursor.encState :=
+    ComputableInPolyTime (fun r : AbsorbIn T => r.2) (encAbsorbIn encT) ChildCursor.encState :=
   ComputableInPolyTime.snd _ _
 
 /-- **The cursor step of `absorb` is polynomial-time.** -/
 private theorem absorbCursor_polyTime :
-    ComputableInPolyTime (fun r : AbsorbIn => cursorNext (weights r.1.1.1) (nodePrec r.1.1.1)
-      (nodes r.1.1.1).length (numPoints r.1.1.1) 64 r.2) encAbsorbIn (encOption encState) := by
-  have hx := absorbCall_polyTime
-  have hc := absorbState_polyTime
+    ComputableInPolyTime (fun r : AbsorbIn T => cursorNext (weights r.1.1.1) (nodePrec r.1.1.1)
+      (nodes r.1.1.1).length (numPoints r.1.1.1) 64 r.2) (encAbsorbIn encT)
+        (encOption encState) := by
+  have hx := absorbCall_polyTime (encT := encT)
+  have hc := absorbState_polyTime (encT := encT)
   have ht := stateNode_polyTime.comp hc
   have hT := (ComputableInPolyTime.length_list _).comp (nodes_polyTime.comp hx)
   have hn := numPoints_polyTime.comp hx
-  have hwt : ComputableInPolyTime (fun r : AbsorbIn => weights r.1.1.1 r.2.1) encAbsorbIn
+  have hwt : ComputableInPolyTime (fun r : AbsorbIn T => weights r.1.1.1 r.2.1) (encAbsorbIn encT)
       (encList encNat) := by
     have h := weights_polyTime.comp (hx.prod ht)
     exact h
-  have hpt : ComputableInPolyTime (fun r : AbsorbIn => nodePrec r.1.1.1 r.2.1) encAbsorbIn
+  have hpt : ComputableInPolyTime (fun r : AbsorbIn T => nodePrec r.1.1.1 r.2.1) (encAbsorbIn encT)
       encNat := by
     have h := ComputableInPolyTime.unary_to_binary.comp (nodePrec_polyTime.comp (hx.prod ht))
     exact h
-  have hnext : ComputableInPolyTime (fun r : AbsorbIn => (weights r.1.1.1 (r.2.1 + 1)).length)
-      encAbsorbIn encUnary := by
+  have hnext : ComputableInPolyTime (fun r : AbsorbIn T => (weights r.1.1.1 (r.2.1 + 1)).length)
+      (encAbsorbIn encT) encUnary := by
     have h := weightsLength_polyTime.comp
       (hx.prod (ComputableInPolyTime.unary_add' ht (ComputableInPolyTime.const 1)))
     exact h
-  have hin : ComputableInPolyTime (fun r : AbsorbIn =>
+  have hin : ComputableInPolyTime (fun r : AbsorbIn T =>
       (((((nodes r.1.1.1).length, numPoints r.1.1.1, (64 : ℕ)), (weights r.1.1.1 r.2.1,
         nodePrec r.1.1.1 r.2.1, (weights r.1.1.1 (r.2.1 + 1)).length)), r.2) : StepInput))
-      encAbsorbIn (encPair (encPair (encPair encUnary (encPair encUnary encUnary))
+      (encAbsorbIn encT) (encPair (encPair (encPair encUnary (encPair encUnary encUnary))
         (encPair (encList encNat) (encPair encNat encUnary))) ChildCursor.encState) :=
     ((hT.prod (hn.prod (ComputableInPolyTime.const 64))).prod (hwt.prod (hpt.prod hnext))).prod hc
-  have hin' : ComputableInPolyTime (fun r : AbsorbIn =>
+  have hin' : ComputableInPolyTime (fun r : AbsorbIn T =>
       (((((nodes r.1.1.1).length, numPoints r.1.1.1, (64 : ℕ)), (weights r.1.1.1 r.2.1,
         nodePrec r.1.1.1 r.2.1, (weights r.1.1.1 (r.2.1 + 1)).length)), r.2) : StepInput))
-      encAbsorbIn encStepInput := hin
+      (encAbsorbIn encT) encStepInput := hin
   refine (computableInPolyTime_cursorStep.comp hin').of_enc_eq fun r => ?_
   rw [cursorNext_eq_cursorStep]
   rfl
 
 /-- **The accumulator step of `absorb` is polynomial-time.** -/
 private theorem absorbAcc_polyTime :
-    ComputableInPolyTime (fun r : AbsorbIn => absorbAt (weights r.1.1.1) (nodePrec r.1.1.1) 64
+    ComputableInPolyTime (fun r : AbsorbIn T => absorbAt (weights r.1.1.1) (nodePrec r.1.1.1) 64
       (mul (wide r.1.1.1) r.1.1.1.fl) (add (wide r.1.1.1) r.1.1.1.fl) (one r.1.1.1.fl)
-      (zero r.1.1.1.fl) r.2 r.1.1.2.2 r.1.2.2) encAbsorbIn
+      (zero r.1.1.1.fl) r.2 r.1.1.2.2 r.1.2.2) (encAbsorbIn encT)
       (encPair (encList encNat) (encPair (encList encNat) (encList (encList encNat)))) := by
-  have hx := absorbCall_polyTime
-  have hc := absorbState_polyTime
+  have hx := absorbCall_polyTime (encT := encT)
+  have hc := absorbState_polyTime (encT := encT)
   have ht := stateNode_polyTime.comp hc
   have hN := wide_polyTime.comp hx
   have hfl := fl_polyTime.comp hx
-  have hacc : ComputableInPolyTime (fun r : AbsorbIn => r.1.1.2.2) encAbsorbIn
+  have hacc : ComputableInPolyTime (fun r : AbsorbIn T => r.1.1.2.2) (encAbsorbIn encT)
       (encPair (encList encNat) (encPair (encList encNat) (encList (encList encNat)))) :=
-    (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd encCall encFrame).comp
+    (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd (encCall encT) encFrame).comp
       ((ComputableInPolyTime.fst _ encValue).comp
         (ComputableInPolyTime.fst _ ChildCursor.encState)))
   have hprod := (ComputableInPolyTime.fst _ _).comp hacc
   have hsum := (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd _ _).comp hacc)
   have hstored := (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp hacc)
-  have hy : ComputableInPolyTime (fun r : AbsorbIn => r.1.2.2) encAbsorbIn (encList encNat) :=
+  have hy : ComputableInPolyTime (fun r : AbsorbIn T => r.1.2.2) (encAbsorbIn encT)
+      (encList encNat) :=
     (ComputableInPolyTime.snd encUnary (encList encNat)).comp ((ComputableInPolyTime.snd _ _).comp
       (ComputableInPolyTime.fst _ ChildCursor.encState))
   have hpy := computableInPolyTime_mul hN hfl hprod hy
   have hnew := computableInPolyTime_add hN hfl hsum hpy
   have hone := computableInPolyTime_one hfl
   have hzero := computableInPolyTime_zero hfl
-  have hlast : ComputableInPolyTime (fun r : AbsorbIn =>
+  have hlast : ComputableInPolyTime (fun r : AbsorbIn T =>
       (BudgetTuples.budgetNext (weights r.1.1.1 r.2.1) (nodePrec r.1.1.1 r.2.1) r.2.2.2.1).isNone)
-      encAbsorbIn encBool := by
-    have hwt : ComputableInPolyTime (fun r : AbsorbIn => weights r.1.1.1 r.2.1) encAbsorbIn
+      (encAbsorbIn encT) encBool := by
+    have hwt : ComputableInPolyTime (fun r : AbsorbIn T => weights r.1.1.1 r.2.1) (encAbsorbIn encT)
         (encList encNat) := by
       have h := weights_polyTime.comp (hx.prod ht)
       exact h
-    have hpt : ComputableInPolyTime (fun r : AbsorbIn => nodePrec r.1.1.1 r.2.1) encAbsorbIn
+    have hpt : ComputableInPolyTime (fun r : AbsorbIn T => nodePrec r.1.1.1 r.2.1)
+        (encAbsorbIn encT)
         encNat := by
       have h := ComputableInPolyTime.unary_to_binary.comp (nodePrec_polyTime.comp (hx.prod ht))
       exact h
-    have hin : ComputableInPolyTime (fun r : AbsorbIn =>
-        (weights r.1.1.1 r.2.1, nodePrec r.1.1.1 r.2.1, r.2.2.2.1)) encAbsorbIn
+    have hin : ComputableInPolyTime (fun r : AbsorbIn T =>
+        (weights r.1.1.1 r.2.1, nodePrec r.1.1.1 r.2.1, r.2.2.2.1)) (encAbsorbIn encT)
         (encPair (encList encNat) (encPair encNat (encList encNat))) :=
       hwt.prod (hpt.prod (stateExps_polyTime.comp hc))
-    have hin' : ComputableInPolyTime (fun r : AbsorbIn =>
-        (weights r.1.1.1 r.2.1, nodePrec r.1.1.1 r.2.1, r.2.2.2.1)) encAbsorbIn
+    have hin' : ComputableInPolyTime (fun r : AbsorbIn T =>
+        (weights r.1.1.1 r.2.1, nodePrec r.1.1.1 r.2.1, r.2.2.2.1)) (encAbsorbIn encT)
         BudgetTuples.encBudgetInput := hin
     have h := ComputableInPolyTime.bool_not.comp (ComputableInPolyTime.optionIsSome
       (BudgetTuples.computableInPolyTime_budgetNext.comp hin'))
     refine h.of_enc_eq fun r => ?_
     simp only [Function.comp_apply]
     cases BudgetTuples.budgetNext (weights r.1.1.1 r.2.1) (nodePrec r.1.1.1 r.2.1) r.2.2.2.1 <;> rfl
-  have hg : ComputableInPolyTime (fun r : AbsorbIn => decide (r.2.2.2.2 + 1 < 64)) encAbsorbIn
+  have hg : ComputableInPolyTime (fun r : AbsorbIn T => decide (r.2.2.2.2 + 1 < 64))
+      (encAbsorbIn encT)
       encBool :=
     ComputableInPolyTime.unary_lt' (ComputableInPolyTime.unary_add' (stateGroup_polyTime.comp hc)
       (ComputableInPolyTime.const 1)) (ComputableInPolyTime.const 64)
@@ -743,23 +764,23 @@ private theorem absorbAcc_polyTime :
 /-- **Absorbing a child's value is polynomial-time.** -/
 theorem absorb_polyTime :
     ComputableInPolyTime
-      (fun p : (Call × Frame) × (ℕ × List ℕ) => (scheme mk).absorb p.1.1 p.1.2 p.2)
-      (encPair (encPair encCall encFrame) encValue) encFrame := by
-  have hc : ComputableInPolyTime (fun p : (Call × Frame) × (ℕ × List ℕ) => p.1.2.1)
-      (encPair (encPair encCall encFrame) encValue) (encOption ChildCursor.encState) :=
-    (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd encCall encFrame).comp
+      (fun p : (Call T × Frame) × (ℕ × List ℕ) => (scheme ev mk).absorb p.1.1 p.1.2 p.2)
+      (encPair (encPair (encCall encT) encFrame) encValue) encFrame := by
+  have hc : ComputableInPolyTime (fun p : (Call T × Frame) × (ℕ × List ℕ) => p.1.2.1)
+      (encPair (encPair (encCall encT) encFrame) encValue) (encOption ChildCursor.encState) :=
+    (ComputableInPolyTime.fst _ _).comp ((ComputableInPolyTime.snd (encCall encT) encFrame).comp
       (ComputableInPolyTime.fst _ encValue))
-  have hfallback : ComputableInPolyTime (fun p : (Call × Frame) × (ℕ × List ℕ) => p.1.2)
-      (encPair (encPair encCall encFrame) encValue) encFrame :=
-    (ComputableInPolyTime.snd encCall encFrame).comp (ComputableInPolyTime.fst _ encValue)
-  have hbody : ComputableInPolyTime (fun r : AbsorbIn =>
+  have hfallback : ComputableInPolyTime (fun p : (Call T × Frame) × (ℕ × List ℕ) => p.1.2)
+      (encPair (encPair (encCall encT) encFrame) encValue) encFrame :=
+    (ComputableInPolyTime.snd (encCall encT) encFrame).comp (ComputableInPolyTime.fst _ encValue)
+  have hbody : ComputableInPolyTime (fun r : AbsorbIn T =>
       ((cursorNext (weights r.1.1.1) (nodePrec r.1.1.1) (nodes r.1.1.1).length (numPoints r.1.1.1)
         64 r.2, absorbAt (weights r.1.1.1) (nodePrec r.1.1.1) 64
         (mul (wide r.1.1.1) r.1.1.1.fl) (add (wide r.1.1.1) r.1.1.1.fl) (one r.1.1.1.fl)
-        (zero r.1.1.1.fl) r.2 r.1.1.2.2 r.1.2.2) : Frame)) encAbsorbIn encFrame :=
+        (zero r.1.1.1.fl) r.2 r.1.1.2.2 r.1.2.2) : Frame)) (encAbsorbIn encT) encFrame :=
     absorbCursor_polyTime.prod (absorbAcc_polyTime)
   have h := ComputableInPolyTime.optionElimWithInput
-    (body := fun (p : (Call × Frame) × (ℕ × List ℕ)) (c : State) =>
+    (body := fun (p : (Call T × Frame) × (ℕ × List ℕ)) (c : State) =>
       ((cursorNext (weights p.1.1) (nodePrec p.1.1) (nodes p.1.1).length (numPoints p.1.1) 64 c,
         absorbAt (weights p.1.1) (nodePrec p.1.1) 64 (mul (wide p.1.1) p.1.1.fl)
           (add (wide p.1.1) p.1.1.fl) (one p.1.1.fl) (zero p.1.1.fl) c p.1.2.2 p.2.2) : Frame))
@@ -769,33 +790,34 @@ theorem absorb_polyTime :
 
 /-- **The value of a call is polynomial-time.** -/
 theorem finish_polyTime :
-    ComputableInPolyTime (fun p : Call × Frame => (scheme mk).finish p.1 p.2)
-      (encPair encCall encFrame) encValue := by
-  have hx := ComputableInPolyTime.fst encCall encFrame
-  have hV : ComputableInPolyTime (fun p : Call × Frame => p.2.2.2.2) (encPair encCall encFrame)
+    ComputableInPolyTime (fun p : Call T × Frame => (scheme ev mk).finish p.1 p.2)
+      (encPair (encCall encT) encFrame) encValue := by
+  have hx := ComputableInPolyTime.fst (encCall encT) encFrame
+  have hV : ComputableInPolyTime (fun p : Call T × Frame => p.2.2.2.2)
+      (encPair (encCall encT) encFrame)
       (encList (encList encNat)) :=
     (ComputableInPolyTime.snd _ _).comp ((ComputableInPolyTime.snd _ _).comp
-      ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd encCall encFrame)))
-  have htab : ComputableInPolyTime (fun p : Call × Frame => table p.1 p.2.2.2.2)
-      (encPair encCall encFrame) (encList (encList (encList encNat))) := by
+      ((ComputableInPolyTime.snd _ _).comp (ComputableInPolyTime.snd (encCall encT) encFrame)))
+  have htab : ComputableInPolyTime (fun p : Call T × Frame => table p.1 p.2.2.2.2)
+      (encPair (encCall encT) encFrame) (encList (encList (encList encNat))) := by
     have h := table_polyTime.comp (hx.prod hV)
     exact h
   have hrec := computableInPolyTime_recover (prec_polyTime.comp hx) (shift_polyTime.comp hx)
     (fl_polyTime.comp hx) (slots_polyTime.comp hx) (twoPowSlots_polyTime.comp hx)
     (levels_polyTime.comp hx) (step_polyTime.comp hx) (points_polyTime.comp hx) htab
-  have h := (depth_polyTime.comp hx).prod hrec
+  have h := ((depth_polyTime encT).comp hx).prod hrec
   exact h
 
-variable {mk}
+variable {ev mk}
 
 /-- **The components of the scheme are polynomial-time**, for a polynomial-time child builder. -/
 theorem scheme_polyTime
-    (hmk : ComputableInPolyTime (fun q : Call × State => mk q.1 q.2)
-      (encPair encCall ChildCursor.encState)
-      (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc))) :
-    (scheme mk).PolyTime encCall encFrame encValue :=
-  ⟨isLeaf_polyTime mk, start_polyTime mk, next_polyTime hmk, absorb_polyTime mk,
-    finish_polyTime mk⟩
+    (hmk : ComputableInPolyTime (fun q : Call T × State => mk q.1 q.2)
+      (encPair (encCall encT) ChildCursor.encState)
+      (encPair encNat (DescribedNetwork.encDescribed (VertexDesc.enc encT)))) :
+    (scheme ev mk).PolyTime (encCall encT) encFrame encValue :=
+  ⟨isLeaf_polyTime ev mk, start_polyTime ev mk, next_polyTime hmk, absorb_polyTime ev mk,
+    finish_polyTime ev mk⟩
 
 end Scheme
 
@@ -807,11 +829,11 @@ number of vertices and the exponents at the node's precision, so both are polyno
 number `2 ^ a` of slots is at most `s + 1` and the number `2 ^ (v₂ t + 1)` of tiles at most
 `4 (s + 1)`. -/
 theorem nativeMk_polyTime :
-    ComputableInPolyTime (fun q : Call × State => nativeMk q.1 q.2)
-      (encPair encCall ChildCursor.encState)
-      (encPair encNat (DescribedNetwork.encDescribed VertexDesc.enc)) := by
-  have hx := ComputableInPolyTime.fst encCall ChildCursor.encState
-  have hc := ComputableInPolyTime.snd encCall ChildCursor.encState
+    ComputableInPolyTime (fun q : Call T × State => nativeMk q.1 q.2)
+      (encPair (encCall encT) ChildCursor.encState)
+      (encPair encNat (DescribedNetwork.encDescribed (VertexDesc.enc encT))) := by
+  have hx := ComputableInPolyTime.fst (encCall encT) ChildCursor.encState
+  have hc := ComputableInPolyTime.snd (encCall encT) ChildCursor.encState
   have ht := stateNode_polyTime.comp hc
   have hj := statePoint_polyTime.comp hc
   have hβ := stateExps_polyTime.comp hc
@@ -821,42 +843,43 @@ theorem nativeMk_polyTime :
   have hL := twoPowSlots_polyTime.comp hx
   have hfl := fl_polyTime.comp hx
   have hD := net_polyTime.comp hx
-  have hi : ComputableInPolyTime (fun q : Call × State => level q.1 ((nodes q.1).getD q.2.1 0))
-      (encPair encCall ChildCursor.encState) encUnary := by
+  have hi : ComputableInPolyTime (fun q : Call T × State => level q.1 ((nodes q.1).getD q.2.1 0))
+      (encPair (encCall encT) ChildCursor.encState) encUnary := by
     have h := nodeLevel_polyTime.comp (hx.prod ht)
     exact h
   have hT : ComputableInPolyTime
-      (fun q : Call × State => 2 ^ (level q.1 ((nodes q.1).getD q.2.1 0) + 1))
-      (encPair encCall ChildCursor.encState) encUnary := by
+      (fun q : Call T × State => 2 ^ (level q.1 ((nodes q.1).getD q.2.1 0) + 1))
+      (encPair (encCall encT) ChildCursor.encState) encUnary := by
     have h := tiles_polyTime.comp (hx.prod ht)
     exact h
-  have hpt : ComputableInPolyTime (fun q : Call × State => nodePrec q.1 q.2.1)
-      (encPair encCall ChildCursor.encState) encUnary := by
+  have hpt : ComputableInPolyTime (fun q : Call T × State => nodePrec q.1 q.2.1)
+      (encPair (encCall encT) ChildCursor.encState) encUnary := by
     have h := nodePrec_polyTime.comp (hx.prod ht)
     exact h
   have hnode : ComputableInPolyTime
-      (fun q : Call × State => node (slots q.1) ((nodes q.1).getD q.2.1 0))
-      (encPair encCall ChildCursor.encState) encIntBin := by
+      (fun q : Call T × State => node (slots q.1) ((nodes q.1).getD q.2.1 0))
+      (encPair (encCall encT) ChildCursor.encState) encIntBin := by
     have h := ComputableInPolyTime.intBin_subNatNat.comp
       ((ComputableInPolyTime.unary_to_binary.comp (node_polyTime.comp (hx.prod ht))).prod
         (ComputableInPolyTime.unary_to_binary.comp hL))
     refine h.of_enc_eq fun q => ?_
     simp only [Function.comp_apply, node, Int.subNatNat_eq_coe, Nat.cast_pow, Nat.cast_ofNat]
-  have hζ : ComputableInPolyTime (fun q : Call × State => (points q.1).getD q.2.2.1 [])
-      (encPair encCall ChildCursor.encState) (encList encNat) := by
+  have hζ : ComputableInPolyTime (fun q : Call T × State => (points q.1).getD q.2.2.1 [])
+      (encPair (encCall encT) ChildCursor.encState) (encList encNat) := by
     have h := ComputableInPolyTime.listGetDWithInput (points_polyTime.comp hx) hj []
     exact h
   have hcap : ComputableInPolyTime
-      (fun q : Call × State => q.2.2.2.1.map (min · (nodePrec q.1 q.2.1)))
-      (encPair encCall ChildCursor.encState) (encList encUnary) := by
-    have hf : ComputableInPolyTime (fun r : (Call × State) × ℕ => min r.2 (nodePrec r.1.1 r.1.2.1))
-        (encPair (encPair encCall ChildCursor.encState) encNat) encUnary := by
+      (fun q : Call T × State => q.2.2.2.1.map (min · (nodePrec q.1 q.2.1)))
+      (encPair (encCall encT) ChildCursor.encState) (encList encUnary) := by
+    have hf : ComputableInPolyTime
+        (fun r : (Call T × State) × ℕ => min r.2 (nodePrec r.1.1 r.1.2.1))
+        (encPair (encPair (encCall encT) ChildCursor.encState) encNat) encUnary := by
       have h := ComputableInPolyTime.binary_min_unary.comp
         ((hpt.comp (ComputableInPolyTime.fst _ _)).prod (ComputableInPolyTime.snd _ _))
       refine h.of_enc_eq fun r => ?_
       simp only [Function.comp_apply, min_comm]
     have h := ComputableInPolyTime.mapWithInput
-      (f := fun (q : Call × State) (b : ℕ) => min b (nodePrec q.1 q.2.1)) hβ hf
+      (f := fun (q : Call T × State) (b : ℕ) => min b (nodePrec q.1 q.2.1)) hβ hf
     exact h
   have hrows := computableInPolyTime_childRows_nativeParentPacking hr ha hi hD hg
   have hchild := computableInPolyTime_nativeChild_nativeParentPacking hfl ha hL hi hT hpt hnode hζ
@@ -866,7 +889,8 @@ theorem nativeMk_polyTime :
 
 /-- **The components of the native contraction recursion are polynomial-time**: the hypothesis
 `hpoly` of `CountingSimulation.contractionAlgorithmOfNative`. -/
-theorem scheme_nativeMk_polyTime : (scheme nativeMk).PolyTime encCall encFrame encValue :=
+theorem scheme_nativeMk_polyTime (ev : T → List Bool → List ℕ) :
+    (scheme ev (nativeMk (T := T))).PolyTime (encCall encT) encFrame encValue :=
   scheme_polyTime nativeMk_polyTime
 
 end Cslib.Circuits.Frontier.FastContraction
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean
index 2cf1e3f19..388e67f5e 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSchedule.lean
@@ -69,10 +69,12 @@ namespace Cslib.Circuits.Frontier.FastContraction
 
 open ContractionSchedule ChildCursor NativeRecovery NativeChild
 
+variable {T : Type}
+
 /-- **A call on the schedule** of a root with `m` edges, for the constant `C`: it keeps the root's
 scale and modulus, is well-formed, has maximum degree at most `degreeBound m` and fewer edges than
 its bound, and has at most `leafSize m` edges or is an active call of the schedule. -/
-structure OnSchedule (C m : ℕ) (x : Call) : Prop where
+structure OnSchedule (C m : ℕ) (x : Call T) : Prop where
   /-- The scale is the root's number of edges. -/
   scale_eq : x.scale = m
   /-- The modulus is the root's. -/
@@ -95,7 +97,7 @@ theorem four_mul_log_le_length_modulus (m : ℕ) : 4 * Nat.log 2 m ≤ (modulus
   rw [pow_succ] at h1
   omega
 
-variable {C m : ℕ} {x : Call}
+variable {C m : ℕ} {x : Call T}
 
 namespace OnSchedule
 
@@ -202,7 +204,7 @@ end OnSchedule
 
 /-- **Every reached call is on the schedule**, from a root on the schedule, once the schedule's
 certificate holds. -/
-theorem Reach.onSchedule (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) {x₀ : Call}
+theorem Reach.onSchedule (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p) {x₀ : Call T}
     (h₀ : OnSchedule C m x₀) (h : Reach nativeMk x₀ x) : OnSchedule C m x := by
   induction h with
   | root => exact h₀
@@ -211,7 +213,7 @@ theorem Reach.onSchedule (hB : ∀ d M p, Active C m d M p → ActiveBounds C m
 /-- **The root is on the schedule**: a well-formed root with `m` edges, at scale `m` with the
 modulus of `m`, of maximum degree at most `degreeBound m`, with edge bound `m + 1` and precision at
 most `C m` for `1 ≤ C`. -/
-theorem onSchedule_root {x₀ : Call} (hC : 1 ≤ C) (hs : x₀.scale = m) (he : x₀.edges = m)
+theorem onSchedule_root {x₀ : Call T} (hC : 1 ≤ C) (hs : x₀.scale = m) (he : x₀.edges = m)
     (hfl : x₀.fl = modulus m) (hwf : WF x₀)
     (hdeg : ∀ v ∈ x₀.net.vertices, v.1.length ≤ degreeBound m)
     (hb : x₀.bound = m + 1) (hd : x₀.depth = 0) (hp : x₀.prec ≤ C * m) : OnSchedule C m x₀ := by
@@ -257,7 +259,7 @@ theorem length_cursorList_le {ws : ℕ → List ℕ} {ps : ℕ → ℕ} {T n r B
         rw [List.map_const', List.sum_replicate, smul_eq_mul, List.length_range]; ring
 
 /-- The nodes of positive multiplicity are at most `2 ^ (a + 1)`. -/
-theorem length_nodes_le (x : Call) : (nodes x).length ≤ 2 ^ (slots x + 1) :=
+theorem length_nodes_le (x : Call T) : (nodes x).length ≤ 2 ^ (slots x + 1) :=
   (List.length_filter_le _ _).trans List.length_range.le
 
 namespace OnSchedule
@@ -322,9 +324,10 @@ end OnSchedule
 schedule's certificate holds at scale `m ≥ 2`, a root on the schedule at depth `0` has a derivation
 of its tagged value over the reached calls with at most `2 ^ ((245760 C + 37) m / √⌊log₂ m⌋)` nodes
 and `⌊log₂ m⌋` stack levels. -/
-theorem exists_eval_onSchedule (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p)
-    {x₀ : Call} (h₀ : OnSchedule C m x₀) (hd : x₀.depth = 0) (hm : 2 ≤ m) :
-    ∃ N H, (scheme nativeMk).Eval (reachInv nativeMk x₀) x₀ (0, value nativeMk x₀) N H ∧
+theorem exists_eval_onSchedule (ev : T → List Bool → List ℕ)
+    (hB : ∀ d M p, Active C m d M p → ActiveBounds C m d M p)
+    {x₀ : Call T} (h₀ : OnSchedule C m x₀) (hd : x₀.depth = 0) (hm : 2 ≤ m) :
+    ∃ N H, (scheme ev nativeMk).Eval (reachInv ev nativeMk x₀) x₀ (0, value ev nativeMk x₀) N H ∧
       N ≤ 2 ^ ((245760 * C + 37) * m / Nat.sqrt (Nat.log 2 m)) ∧ H ≤ Nat.log 2 m := by
   obtain ⟨N, H, he, hN, hH⟩ := exists_eval_reachInv_count hd (Nat.log 2 m)
     (fun d => 2 ^ (2 * Nat.log 2 m + branchExponent C m d)) fun x hx ha => by
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean
index 76f982e9f..84b65a919 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionShape.lean
@@ -21,8 +21,8 @@ the schedule: they are what makes the calls, frames and values polynomially long
 **The invariant** (`FastContraction.Shape`). A reached call at depth `d` keeps the root's scale and
 modulus, is well-formed, has at most `2 m` edges, precision at most `p₀ + 40 m² d` for the root's
 precision `p₀`, at most `V₀ + m² d` vertices for the root's `V₀` vertices, as many rows (unless it
-is the root), and every vertex descriptor is a table of the root or a packet descriptor whose fields
-are bounded (`FastContraction.PacketBound`). It passes to the native children
+is the root), and every vertex descriptor is a descriptor of the root or a packet descriptor whose
+fields are bounded (`FastContraction.PacketBound`). It passes to the native children
 (`FastContraction.Shape.child`): a child has at most twice the edges of its parent
 (`NativeChild.numEdges_nativeChild_le`), its precision `p_t = p + 8 h 2 ^ (a - i) + 8 M (a + 1)` is
 at most `p + 40 m²` since `2 ^ a ≤ m`, and it adds at most `M (2 ^ a) ^ 12 ≤ m²` packet vertices
@@ -50,6 +50,8 @@ namespace Cslib.Circuits.Frontier.FastContraction
 
 open ContractionSchedule ChildCursor NativeRecovery NativeChild
 
+variable {T : Type}
+
 /-- **A bounded packet descriptor** for a root with modulus `fl` and `m` edges, at precision at most
 `P`, on a vertex with `k` ports: its precision is at most `P` and is its number of exponents per
 tile, its modulus is `fl`, it has `2 ^ a` slots with `a ≤ ⌊log₂ m⌋`, `2 ^ (i + 1)` tiles with
@@ -68,7 +70,7 @@ theorem PacketBound.mono {fl : List ℕ} {m P P' k : ℕ} {d : NativePacket.Pack
 
 /-- **The shape of a call** reached from a root `x₀` with `m` edges, precision `p₀` and `V₀`
 vertices, at depth `d`. -/
-structure Shape (x₀ x : Call) : Prop where
+structure Shape (x₀ x : Call T) : Prop where
   /-- The scale is the root's. -/
   scale_eq : x.scale = x₀.scale
   /-- The modulus is the root's. -/
@@ -91,7 +93,7 @@ structure Shape (x₀ x : Call) : Prop where
       PacketBound x₀.fl x₀.edges (x₀.prec + x.depth * (40 * x₀.edges ^ 2)) v.1.length d
 
 /-- The exponent tuple of a child of an active call has entries below the node's precision. -/
-theorem lt_nodePrec_of_mem_children {x : Call} {c : State} (hc : c ∈ children x) :
+theorem lt_nodePrec_of_mem_children {x : Call T} {c : State} (hc : c ∈ children x) :
     ∀ b ∈ c.2.2.1, b < nodePrec x c.1 := by
   simp only [children, cursorList, nodeBlock, pointBlock, groupBlock, List.mem_flatMap,
     List.mem_range, List.mem_map] at hc
@@ -99,7 +101,7 @@ theorem lt_nodePrec_of_mem_children {x : Call} {c : State} (hc : c ∈ children
   exact fun b hb => BudgetTuples.lt_of_mem_budgetTuples (weights_pos j) hβ hb
 
 /-- The ports of a vertex of a well-formed call are at most its edges. -/
-theorem length_le_edges_of_wf {x : Call} (hx : WF x) {v : List ℕ × VertexDesc}
+theorem length_le_edges_of_wf {x : Call T} (hx : WF x) {v : List ℕ × VertexDesc T}
     (hv : v ∈ x.net.vertices) : v.1.length ≤ x.edges := by
   obtain ⟨k, hk, rfl⟩ := List.getElem_of_mem hv
   have hnd : (x.net.vertices[k]).1.Nodup := nodup_ports hx.2 ⟨k, hk⟩
@@ -111,7 +113,7 @@ theorem length_le_edges_of_wf {x : Call} (hx : WF x) {v : List ℕ × VertexDesc
 
 section Child
 
-variable {x₀ x : Call}
+variable {x₀ x : Call T}
 
 /-- The schedule's numbers at an active call at scale `m`: `a ≤ ⌊log₂ m⌋`, `2 ^ (12 a) ≤ m`,
 `u ≤ ⌊log₂ m⌋ < m`, and `h ≤ 3 M + u`. -/
@@ -183,7 +185,7 @@ theorem level_le_slots_of_mem_children (ha : active x = true) {c : State} (hc :
   omega
 
 /-- The interpolation points are 0/1 lists with `e` coordinates. -/
-theorem getD_points_facts (x : Call) (i : ℕ) :
+theorem getD_points_facts (x : Call T) (i : ℕ) :
     ((points x).getD i []).length ≤ x.fl.length ∧ ∀ z ∈ (points x).getD i [], z ≤ 1 := by
   by_cases hi : i < (points x).length
   · rw [List.getD_eq_getElem _ _ hi]
@@ -195,7 +197,7 @@ theorem getD_points_facts (x : Call) (i : ℕ) :
     simp
 
 /-- The rows of a native child are at most the parent's vertices. -/
-theorem childRows_le (r i : ℕ) (D : DescribedNetwork VertexDesc)
+theorem childRows_le (r i : ℕ) (D : DescribedNetwork (VertexDesc T))
     (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (g : ℕ) :
     childRows r i D pk g ≤ D.vertices.length := by
   unfold childRows
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean
index 0fd1f563a..a4800c808 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionSize.lean
@@ -42,6 +42,8 @@ namespace Cslib.Circuits.Frontier.FastContraction
 
 open Turing.MultiTapeTM NativePacket
 
+variable {T : Type} {encT : T ↪ List Bool}
+
 /-- A number at most `b` has at most `b` binary digits. -/
 theorem length_encNat_le {a b : ℕ} (h : a ≤ b) : (encNat a).length ≤ b := by
   rw [encNat_apply, Nat.size_eq_bits_len]
@@ -91,7 +93,7 @@ theorem two_pow_le_of_le_log {a m : ℕ} (ha : a ≤ Nat.log 2 m) (hm : m ≠ 0)
 modulus has 0/1 coefficients. -/
 theorem length_enc_inr_le {fl : List ℕ} {m P k : ℕ} {d : PacketDesc} (h : PacketBound fl m P k d)
     {B : ℕ} (hB : 2 * (m + 1) * (P + 1) ≤ B) (hfl : fl.length ≤ B) (hfl1 : ∀ z ∈ fl, z ≤ 1)
-    (hk : k ≤ B) : (VertexDesc.enc (.inr d)).length ≤ 200 * (B + 1) ^ 2 := by
+    (hk : k ≤ B) : (VertexDesc.enc encT (.inr d)).length ≤ 200 * (B + 1) ^ 2 := by
   obtain ⟨hp, hnb, hfl', ha, hL, hi, htl, ht, hcols, hζ, hζ1, htags, hslots, hβ, hβ'⟩ := h
   have h2m : 2 * (m + 1) ≤ B := le_trans (Nat.le_mul_of_pos_right _ (by omega)) hB
   have hP1 : P + 1 ≤ B := le_trans (Nat.le_mul_of_pos_left _ (by omega)) hB
@@ -132,14 +134,14 @@ theorem length_enc_inr_le {fl : List ℕ} {m P k : ℕ} {d : PacketDesc} (h : Pa
 bound, precision, number of edges, number of vertices, modulus length, the binary length of its
 rows and its ports are at most `B`, the modulus has 0/1 coefficients, and its descriptors are at
 most `R` long. -/
-theorem length_encCall_le {x : Call} {B R : ℕ} (hs : x.scale ≤ B) (hd : x.depth ≤ B)
+theorem length_encCall_le {x : Call T} {B R : ℕ} (hs : x.scale ≤ B) (hd : x.depth ≤ B)
     (hb : x.bound ≤ B) (hp : x.prec ≤ B) (hfl : x.fl.length ≤ B) (hfl1 : ∀ z ∈ x.fl, z ≤ 1)
     (hr : (encNat x.rows).length ≤ B) (hE : x.edges ≤ B) (hV : x.net.vertices.length ≤ B)
     (hports : ∀ v ∈ x.net.vertices, v.1.length ≤ B ∧ ∀ i ∈ v.1, i ≤ B)
-    (hdesc : ∀ v ∈ x.net.vertices, (VertexDesc.enc v.2).length ≤ R) :
-    (encCall x).length ≤ 64 * (B + 1) ^ 3 + 2 * B * R := by
+    (hdesc : ∀ v ∈ x.net.vertices, (VertexDesc.enc encT v.2).length ≤ R) :
+    (encCall encT x).length ≤ 64 * (B + 1) ^ 3 + 2 * B * R := by
   have h1 := length_encList_le_of_le_one hfl1
-  have hv : ∀ v ∈ x.net.vertices, (encPair (encList encNat) VertexDesc.enc v).length ≤
+  have hv : ∀ v ∈ x.net.vertices, (encPair (encList encNat) (VertexDesc.enc encT) v).length ≤
       2 * (B * (2 * B + 1)) + 1 + R := fun v hv => by
     rw [length_encPair]
     have := (length_encList_le encNat (B := B) fun i hi => length_encNat_le
@@ -180,15 +182,16 @@ theorem length_encList_le_of_reducedAt {p : ℕ} {fl c : List ℕ} (h : ReducedA
     ((h.2 z hz).trans_lt (Nat.pow_lt_pow_right (by norm_num) (Nat.lt_succ_self p)))
 
 /-- **The values of the calls are reduced** at their precision, for every child builder. -/
-theorem reducedAt_value (mk : Call → ChildCursor.State → ℕ × DescribedNetwork VertexDesc)
-    (x : Call) :
-    ReducedAt x.prec x.fl (value mk x) := by
+theorem reducedAt_value (ev : T → List Bool → List ℕ)
+    (mk : Call T → ChildCursor.State → ℕ × DescribedNetwork (VertexDesc T))
+    (x : Call T) :
+    ReducedAt x.prec x.fl (value ev mk x) := by
   cases ha : active x
-  · rw [value_of_not_active mk ha]
-    exact DescribedNetwork.reduced_sumValue (ops := SumOps.galois) (eval := VertexDesc.entry)
+  · rw [value_of_not_active ev mk ha]
+    exact DescribedNetwork.reduced_sumValue (ops := SumOps.galois) (eval := VertexDesc.entry ev)
       (x.prec, x.fl) x.net
-  · rw [value_of_active mk ha, finishValue, NativeRecovery.recover]
-    set W := table x (runLoop x fun c => value mk (child x mk c)).2.2
+  · rw [value_of_active ev mk ha, finishValue, NativeRecovery.recover]
+    set W := table x (runLoop x fun c => value ev mk (child x mk c)).2.2
     have hfold : ∀ (l : List ℕ) (S : List ℕ), ReducedAt (x.prec + shift x) x.fl S →
         ReducedAt (x.prec + shift x) x.fl (l.foldl (fun S k => if k = 2 ^ slots x then S else
           GaloisRingArith.add (x.prec + shift x) x.fl S
@@ -213,12 +216,13 @@ theorem reducedAt_value (mk : Call → ChildCursor.State → ℕ × DescribedNet
     exact Nat.le_of_lt_succ (Nat.lt_succ_of_le (Nat.div_le_of_le_mul (by linarith)))
 
 /-- **The encoded length of a tagged value** of a call. -/
-theorem length_encValue_le (mk : Call → ChildCursor.State → ℕ × DescribedNetwork VertexDesc)
-    (x : Call) :
-    (encValue (x.depth, value mk x)).length ≤
+theorem length_encValue_le (ev : T → List Bool → List ℕ)
+    (mk : Call T → ChildCursor.State → ℕ × DescribedNetwork (VertexDesc T))
+    (x : Call T) :
+    (encValue (x.depth, value ev mk x)).length ≤
       2 * x.depth + 1 + x.fl.length * (2 * (x.prec + 1) + 1) := by
   rw [length_encPair, encUnary_apply, List.length_replicate]
-  have := length_encList_le_of_reducedAt (reducedAt_value mk x)
+  have := length_encList_le_of_reducedAt (reducedAt_value ev mk x)
   simp only at this ⊢
   omega
 
@@ -292,11 +296,11 @@ end Frames
 
 section ActiveFrames
 
-variable {x : Call}
+variable {x : Call T}
 
 /-- The bound `256 (m + 1) ^ 5 (p + 1) + e` on the numbers of the frames of an active call at scale
 `m` with precision `p`. -/
-@[expose] def frameBound (x : Call) : ℕ := 256 * (x.scale + 1) ^ 5 * (x.prec + 1) + x.fl.length
+@[expose] def frameBound (x : Call T) : ℕ := 256 * (x.scale + 1) ^ 5 * (x.prec + 1) + x.fl.length
 
 /-- The numbers of an active call with at most `m` edges at scale `m`. -/
 theorem active_numbers (ha : active x = true) (hM : x.edges ≤ x.scale) :
@@ -431,24 +435,25 @@ end ActiveFrames
 
 section Sizes
 
-variable {x₀ x : Call}
+variable {x₀ x : Call T}
 
 /-- **The sizes of a call of a given shape**: from a root `x₀` at depth `0`, at scale its number
 `m` of edges, with bound `m + 1`, a 0/1 modulus and descriptors at most `200 (Z + 1) ^ 2` long, a
 call of its shape, its tagged value and, if it is active, its frames are at most
 `1000 (Z + 1) ^ 3` long, once `Z` dominates `256 (m + 1) ^ 5 (P + 1) + e` for the precision bound
 `P = p₀ + 40 m² (m + 1)` and the vertices, rows and their growth. -/
-theorem Shape.length_le (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound = x₀.edges + 1)
+theorem Shape.length_le (ev : T → List Bool → List ℕ) (h₀s : x₀.scale = x₀.edges)
+    (h₀b : x₀.bound = x₀.edges + 1)
     (h₀d : x₀.depth = 0) (h : Shape x₀ x) {Z : ℕ}
     (hZ1 : 256 * (x₀.edges + 1) ^ 5 * (x₀.prec + (x₀.edges + 1) * (40 * x₀.edges ^ 2) + 1) +
       x₀.fl.length ≤ Z)
     (hZ2 : x₀.net.vertices.length + (x₀.edges + 1) * x₀.edges ^ 2 + (encNat x₀.rows).length ≤ Z)
     (hfl1 : ∀ z ∈ x₀.fl, z ≤ 1)
-    (hR₀ : ∀ w ∈ x₀.net.vertices, (VertexDesc.enc w.2).length ≤ 200 * (Z + 1) ^ 2) :
-    (encCall x).length ≤ 1000 * (Z + 1) ^ 3 ∧
-      (encValue (x.depth, value nativeMk x)).length ≤ 1000 * (Z + 1) ^ 3 ∧
+    (hR₀ : ∀ w ∈ x₀.net.vertices, (VertexDesc.enc encT w.2).length ≤ 200 * (Z + 1) ^ 2) :
+    (encCall encT x).length ≤ 1000 * (Z + 1) ^ 3 ∧
+      (encValue (x.depth, value ev nativeMk x)).length ≤ 1000 * (Z + 1) ^ 3 ∧
       (active x = true → ∀ vals c,
-        (encPair encCall encFrame (x, frameAt x vals c)).length ≤ 1000 * (Z + 1) ^ 3) := by
+        (encPair (encCall encT) encFrame (x, frameAt x vals c)).length ≤ 1000 * (Z + 1) ^ 3) := by
   set m := x₀.edges with hm
   set P := x₀.prec + (m + 1) * (40 * m ^ 2) with hP
   -- The numbers of `x`.
@@ -476,7 +481,7 @@ theorem Shape.length_le (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound =
   have hports : ∀ v ∈ x.net.vertices, v.1.length ≤ Z ∧ ∀ i ∈ v.1, i ≤ Z := fun v hv =>
     ⟨(length_le_edges_of_wf h.wf hv).trans (hE.trans (by omega)),
       fun i hi => (h.wf.2.1 v hv i hi).le.trans (hE.trans (by omega))⟩
-  have hR : ∀ v ∈ x.net.vertices, (VertexDesc.enc v.2).length ≤ 200 * (Z + 1) ^ 2 := by
+  have hR : ∀ v ∈ x.net.vertices, (VertexDesc.enc encT v.2).length ≤ 200 * (Z + 1) ^ 2 := by
     intro v hv
     rcases h.desc v hv with ⟨w, hw, hvw⟩ | ⟨d, hvd, hb⟩
     · rw [hvw]; exact hR₀ w hw
@@ -492,7 +497,7 @@ theorem Shape.length_le (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound =
   have hcall := length_encCall_le (B := Z) (R := 200 * (Z + 1) ^ 2) (x := x)
     (by rw [hsc]; omega) (hd.trans (by omega)) (by omega) (hprec.trans (by omega))
     (h.fl_eq ▸ hflZ) (h.fl_eq ▸ hfl1) hrows (hE.trans (by omega)) (hV.trans (by omega)) hports hR
-  have hcall' : (encCall x).length ≤ 464 * (Z + 1) ^ 3 := by
+  have hcall' : (encCall encT x).length ≤ 464 * (Z + 1) ^ 3 := by
     have : 2 * Z * (200 * (Z + 1) ^ 2) ≤ 400 * (Z + 1) ^ 3 := by
       have : Z ≤ Z + 1 := Nat.le_succ _
       calc 2 * Z * (200 * (Z + 1) ^ 2) = 400 * (Z * (Z + 1) ^ 2) := by ring
@@ -502,7 +507,7 @@ theorem Shape.length_le (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound =
   have hZ3 : (Z + 1) ^ 2 ≤ (Z + 1) ^ 3 := Nat.pow_le_pow_right (by omega) (by norm_num)
   have hZ1' : Z + 1 ≤ (Z + 1) ^ 3 := Nat.le_self_pow (by norm_num) _
   refine ⟨hcall'.trans (by omega), ?_, fun ha vals c => ?_⟩
-  · have hv := length_encValue_le nativeMk x
+  · have hv := length_encValue_le ev nativeMk x
     rw [h.fl_eq] at hv
     have : x₀.fl.length * (2 * (x.prec + 1) + 1) ≤ Z * (2 * Z + 1) :=
       Nat.mul_le_mul hflZ (by omega)
@@ -519,7 +524,7 @@ theorem Shape.length_le (h₀s : x₀.scale = x₀.edges) (h₀b : x₀.bound =
         Nat.mul_le_mul_left _ (by omega)
       omega
     have hfZ : (frameBound x + 1) ^ 3 ≤ (Z + 1) ^ 3 := Nat.pow_le_pow_left (by omega) 3
-    have hl := length_encPair (enc₁ := encCall) (enc₂ := encFrame) (x, frameAt x vals c)
+    have hl := length_encPair (enc₁ := encCall encT) (enc₂ := encFrame) (x, frameAt x vals c)
     simp only at hl
     rw [hl]
     omega
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean
index 657277b1a..bc37a2e7a 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionStep.lean
@@ -51,6 +51,8 @@ namespace Cslib.Circuits.Frontier.FastContraction
 
 open Finset GaloisRingArith ChildCursor NativeRecovery ContractionSchedule NativeChild
 
+variable {T : Type}
+
 /-- **The native child builder**: at the cursor state `(j, i, β, g)`, the rows and the native
 child of group `g` at the `j`-th node, the `i`-th point and the exponents `β`. The rows are capped
 at the number of vertices (`FastContraction.rowCap`) and the exponents at the node's precision
@@ -58,18 +60,18 @@ at the number of vertices (`FastContraction.rowCap`) and the exponents at the no
 (`FastContraction.nativeMk_eq`); on every call and state they keep the builder polynomial-time,
 since the number of rows and the exponents are stored in binary but the child lists one word per
 row and stores the exponents in unary. -/
-@[expose] def nativeMk (x : Call) (c : State) : ℕ × DescribedNetwork VertexDesc :=
+@[expose] def nativeMk (x : Call T) (c : State) : ℕ × DescribedNetwork (VertexDesc T) :=
   (childRows (rowCap x) (level x ((nodes x).getD c.1 0)) x.net (packing x) c.2.2.2,
     nativeChild x.fl (slots x) (level x ((nodes x).getD c.1 0)) (nodePrec x c.1)
       (node (slots x) ((nodes x).getD c.1 0)) ((points x).getD c.2.1 []) (rowCap x) x.net
       (packing x) (c.2.2.1.map (min · (nodePrec x c.1))) c.2.2.2)
 
 /-- **A well-formed call**: its modulus is irreducible modulo `2` and its network is rows-first. -/
-@[expose] def WF (x : Call) : Prop :=
+@[expose] def WF (x : Call T) : Prop :=
   Irreducible ((monicOf x.fl).map (Int.castRingHom (ZMod 2))) ∧
     x.net.IsRowsFirstBipartite x.rows
 
-variable {x : Call}
+variable {x : Call T}
 
 /-- The cap of `nativeMk` leaves a tuple of weight below `p` unchanged, for positive weights. -/
 theorem map_min_of_mem_budgetTuples {ws : List ℕ} (hw : ∀ w ∈ ws, 0 < w) {p : ℕ} {β : List ℕ}
@@ -139,7 +141,8 @@ theorem pairwise_isUnit_points (hirr : Irreducible ((monicOf x.fl).map (Int.cast
 
 /-- **The step of an active call is correct**, for the native child builder and well-formed
 calls. -/
-theorem stepCorrect_nativeMk : StepCorrect nativeMk WF := by
+theorem stepCorrect_nativeMk (ev : T → List Bool → List ℕ) :
+    StepCorrect ev (nativeMk (T := T)) WF := by
   intro x hx ha vals hvals
   obtain ⟨hirr, hD⟩ := hx
   have ha' := ha
@@ -147,7 +150,7 @@ theorem stepCorrect_nativeMk : StepCorrect nativeMk WF := by
   obtain ⟨-, hu, huM, hua, -, -, -⟩ := ha'
   have hlen : (points x).length = numPoints x := by simp [points]
   have hr := DescribedNetwork.rows_le_of_isRowsFirstBipartite hD (one_le_edges_of_active ha)
-  refine NativeCall.val_recover_eq_contraction hirr hD hu huM hua (le_taperStep_mul hu)
+  refine NativeCall.val_recover_eq_contraction hirr hD ev hu huM hua (le_taperStep_mul hu)
     (taperStep_mul_le _ _ _) (pow_slots_le_edges_of_active ha) ?_ (points x)
     (pairwise_isUnit_points hirr ha)
     (by rw [hlen]; exact Nat.lt_succ_self _) _ ?_
@@ -185,7 +188,7 @@ theorem stepCorrect_nativeMk : StepCorrect nativeMk WF := by
         val P x.fl (vals (j, i, β, g)) =
           (nativeChild x.fl (slots x) v P (node (slots x) k) ((points x).getD i []) x.rows x.net
             (nativeParentPacking x.rows (slots x) x.net) β g).contraction
-            fun d bs => val P x.fl (d.entry bs) := by
+            fun d bs => val P x.fl (d.entry ev bs) := by
       rintro v P rfl rfl
       have h := hvals _ hmem
       rw [nativeMk_eq ⟨hirr, hD⟩ ha hmem] at h
@@ -209,7 +212,7 @@ theorem lt_of_mem_children {c : State} (hc : c ∈ children x) :
 
 /-- **Well-formedness passes to the native children**: they keep the modulus, and they are
 rows-first (`NativeChild.isRowsFirstBipartite_nativeChild`). -/
-theorem wfChildren_nativeMk : WFChildren nativeMk WF := by
+theorem wfChildren_nativeMk : WFChildren (nativeMk (T := T)) WF := by
   intro x hx ha c hc
   obtain ⟨hirr, hD⟩ := hx
   refine ⟨hirr, ?_⟩
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeCall.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeCall.lean
index 82af1b001..cbaf7c2e0 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeCall.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeCall.lean
@@ -66,8 +66,10 @@ theorem prod_map_range {M : Type*} [CommMonoid M] (F : ℕ → M) (n : ℕ) :
   rw [← List.map_coe_finRange_eq_range, List.map_map, ← List.ofFn_eq_map, List.prod_ofFn]
   rfl
 
-variable {fl : List ℕ} (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2))))
-  {D : DescribedNetwork VertexDesc} {r : ℕ} (hD : D.IsRowsFirstBipartite r)
+variable {T : Type} {fl : List ℕ}
+  (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2))))
+  {D : DescribedNetwork (VertexDesc T)} {r : ℕ} (hD : D.IsRowsFirstBipartite r)
+  (ev : T → List Bool → List ℕ)
 
 include hD in
 /-- **One native active call is correct when its stored values are** ([OpenAI2026ETH],
@@ -98,9 +100,9 @@ theorem val_recover_eq_contraction {a u h p Δ : ℕ} (hu : 1 ≤ u) (huM : u 
                 (nodePrecision p h a D.numEdges (padicValInt 2 (node a k))) (node a k)
                 (ζl.getD i []) r D (nativeParentPacking r a D) β g).contraction
               fun d bs => val (nodePrecision p h a D.numEdges (padicValInt 2 (node a k))) fl
-                (d.entry bs)).prod).sum) :
+                (d.entry ev bs)).prod).sum) :
     val p fl (recover p Δ fl a u h ζl W) =
-      D.contraction fun d bs => val p fl (d.entry bs) := by
+      D.contraction fun d bs => val p fl (d.entry ev bs) := by
   have hB := AdjoinRoot.algebraMap_mem_integer_padicValuation (monic_monicOf fl) hirr
   have hcard : Fintype.card (Fin D.numEdges) = D.numEdges := Fintype.card_fin _
   have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by
@@ -117,7 +119,7 @@ theorem val_recover_eq_contraction {a u h p Δ : ℕ} (hu : 1 ≤ u) (huM : u 
             Fin (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)) =>
               (Z.2.2 : ℕ) + 1)
             (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)),
-          ∏ g, ((parentSplitting hirr hD a p u h hua ht hq (ζl.getD k [])).child β
+          ∏ g, ((parentSplitting hirr hD ev a p u h hua ht hq (ζl.getD k [])).child β
             g).contraction := by
     intro t ht hq k
     obtain ⟨kk, hkk, hkt⟩ : ∃ kk, (kk < 2 ^ (a + 1) ∧ kk ≠ 2 ^ a) ∧ node a kk = t := by
@@ -138,9 +140,9 @@ theorem val_recover_eq_contraction {a u h p Δ : ℕ} (hu : 1 ≤ u) (huM : u 
     refine Fintype.prod_congr _ _ fun g => ?_
     simp only [Function.comp_apply]
     rw [DescribedNetwork.map_contraction]
-    exact contraction_nativeChild hirr hD hK hua ht hq (ζl.getD k []) β g
+    exact contraction_nativeChild hirr hD ev hK hua ht hq (ζl.getD k []) β g
   obtain ⟨b, hb, hx⟩ := TensorNetwork.exists_recoverFromValues_eq_add_of_children (RingO hirr) hB
-    (parentNetwork hirr hD) (parentSide r) (parentSide_src hD) (parentSide_tgt hD)
+    (parentNetwork hirr hD ev) (parentSide r) (parentSide_src hD) (parentSide_tgt hD)
     (parentPacking hD a) (p := p) hu (by rwa [hcard]) hua (by rwa [hcard]) (by rwa [hcard]) ζ hζ
     (by rwa [hcard]) v hv
   -- Native recovery computes the reduction of the recovered value.
@@ -161,8 +163,9 @@ theorem val_recover_eq_contraction {a u h p Δ : ℕ} (hu : 1 ≤ u) (huM : u 
     (fun t => nodePrecision p h a D.numEdges (padicValInt 2 t)) hpt ζ hζ ζl rfl
     (fun i => (reduction_liftO hirr _ _).symm) v W
     (fun k _ _ _ i => ⟨0, by simp only [v, toNat_node_add, reduction_liftO, mul_zero, add_zero]⟩)
-    (parentNetwork hirr hD).contraction hb hx
-  rw [hrec, ← DescribedNetwork.reduction_contraction_toNetwork hD hirr (fun d bs => d.entry bs) p]
+    (parentNetwork hirr hD ev).contraction hb hx
+  rw [hrec, ← DescribedNetwork.reduction_contraction_toNetwork hD hirr
+    (fun d bs => d.entry ev bs) p]
   exact RingHom.congr_fun (AdjoinRoot.castHom_comp_reduction (monic_monicOf fl) hirr
     (Nat.le_add_right p Δ)) _
 
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean
index 2d0a6a4ae..ab503a6a6 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChild.lean
@@ -112,6 +112,8 @@ namespace NativeChild
 open ChildNumbering GaloisRingArith NativePacket
 open ContractionSchedule (nodePrecision)
 
+variable {T : Type}
+
 /-! ### The native child -/
 
 /-- **The groups of the vertices** in coordinate `i`: digit `i` of the row word of a row
@@ -168,17 +170,17 @@ and the interpolation value `ζ`: the precision `p_t` and `p_t` exponents per ti
 @[expose] def betaSlice (i pt : ℕ) (β : List ℕ) (q : ℕ) : List ℕ :=
   (β.drop (q * (2 ^ (i + 1) * pt))).take (2 ^ (i + 1) * pt)
 
-/-- The default vertex: no ports and the empty table. -/
-abbrev defaultVertex : List ℕ × VertexDesc := ([], .inl [])
+/-- The default vertex: no ports and the default packet descriptor. -/
+abbrev defaultVertex : List ℕ × VertexDesc T := ([], .inr default)
 
 /-- **The native child** of group `g` at the node `t` of valuation `i`, the interpolation value
 `ζ`, the precision `p_t` and the packet-major exponents `β`, of the rows-first parent `D` with `r`
 rows and the native packing `pk` of its edges: the vertices of group `g` with their descriptors
 and renumbered ports, then one packet vertex per packet. -/
 @[expose] def nativeChild (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ : List ℕ) (r : ℕ)
-    (D : DescribedNetwork VertexDesc)
+    (D : DescribedNetwork (VertexDesc T))
     (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (β : List ℕ) (g : ℕ) :
-    DescribedNetwork VertexDesc :=
+    DescribedNetwork (VertexDesc T) :=
   let groups := groupsOf r i D.vertices.length pk.1
   let cedges := childEdgeList groups g D.edgeEnds (pk.2.2.map Prod.fst)
   ⟨cedges.length,
@@ -194,7 +196,7 @@ and renumbered ports, then one packet vertex per packet. -/
           betaSlice i pt β q))⟩
 
 /-- **The number of rows of the native child**: the number of vertices of group `g`. -/
-@[expose] def childRows (r i : ℕ) (D : DescribedNetwork VertexDesc)
+@[expose] def childRows (r i : ℕ) (D : DescribedNetwork (VertexDesc T))
     (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (g : ℕ) : ℕ :=
   (groupsOf r i D.vertices.length pk.1).count g
 
@@ -392,7 +394,8 @@ theorem map_filterMap_of_isSome {α β γ : Type*} (f : α → Option β) (y : 
 section Parent
 
 variable {fl : List ℕ} (hirr : Irreducible ((monicOf fl).map (Int.castRingHom (ZMod 2))))
-  {D : DescribedNetwork VertexDesc} {r : ℕ} (hD : D.IsRowsFirstBipartite r)
+  {D : DescribedNetwork (VertexDesc T)} {r : ℕ} (hD : D.IsRowsFirstBipartite r)
+  (ev : T → List Bool → List ℕ)
 
 /-- The valuation ring `O = ℤ_(2)[U] / (f)` of `f = monicOf fl`. -/
 noncomputable abbrev RingO : Subring (AdjoinRoot ((monicOf fl).map (Int.castRingHom ℚ))) :=
@@ -401,7 +404,7 @@ noncomputable abbrev RingO : Subring (AdjoinRoot ((monicOf fl).map (Int.castRing
 /-- **The parent over `O`**: the network of the descriptors with the lifts of their entries. -/
 @[expose] noncomputable def parentNetwork :
     TensorNetwork (RingO hirr) Bool (Fin D.vertices.length) (Fin D.numEdges) :=
-  D.toNetwork hD fun d bs => liftO hirr (d.entry bs)
+  D.toNetwork hD fun d bs => liftO hirr (d.entry ev bs)
 
 /-- The sides of the parent: the first `r` vertices are the rows. -/
 @[expose] def parentSide (r : ℕ) {k : ℕ} (v : Fin k) : Bool := decide ((v : ℕ) < r)
@@ -425,7 +428,7 @@ theorem parentSide_tgt (j : Fin D.numEdges) : parentSide r (D.tgtFin hD j) = fal
 
 /-- **The native packing of the parent**: `nativePacking` of its `(row, column)` edges, with `r`
 rows, `k - r` columns, packets of `2 ^ a` slots and `64` symbols. -/
-@[expose] def nativeParentPacking (r a : ℕ) (D : DescribedNetwork VertexDesc) :
+@[expose] def nativeParentPacking (r a : ℕ) (D : DescribedNetwork (VertexDesc T)) :
     (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ) :=
   PacketPacking.nativePacking r (D.vertices.length - r) a 64
     (D.edgeEnds.map fun e => (e.1, e.2 - r))
@@ -490,7 +493,7 @@ its packing, at the node `t`, the precision `p`, and the lift of the interpolati
 @[expose] noncomputable def parentSplitting (a p u h : ℕ) (hua : u ≤ a) {t : ℤ}
     (ht : t ∈ recoveryNodes a) (hq : 0 < taperMult u h t) (ζ : List ℕ) :=
   TensorNetwork.callSplitting (RingO hirr)
-    (AdjoinRoot.algebraMap_mem_integer_padicValuation _ hirr) (parentNetwork hirr hD)
+    (AdjoinRoot.algebraMap_mem_integer_padicValuation _ hirr) (parentNetwork hirr hD ev)
     (parentSide r) (parentSide_src hD) (parentSide_tgt hD) (parentPacking hD a) p u h hua ht hq
     (liftO hirr ζ)
 
@@ -500,21 +503,22 @@ variable {a p u h : ℕ} (hua : u ≤ a) {t : ℤ} (ht : t ∈ recoveryNodes a)
   (hq : 0 < taperMult u h t) (ζ : List ℕ)
 
 /-- The rows of the splitting are the first `r` vertices. -/
-theorem parentSplitting_side : (parentSplitting hirr hD a p u h hua ht hq ζ).side = parentSide r :=
-  TensorNetwork.callSplitting_side (RingO hirr) _ (parentNetwork hirr hD) (parentSide r) _ _
+theorem parentSplitting_side :
+    (parentSplitting hirr hD ev a p u h hua ht hq ζ).side = parentSide r :=
+  TensorNetwork.callSplitting_side (RingO hirr) _ (parentNetwork hirr hD ev) (parentSide r) _ _
     (parentPacking hD a) p u h hua ht hq (liftO hirr ζ)
 
 /-- The groups of the splitting are the groups of the packing in coordinate `v₂(t)`. -/
-theorem parentSplitting_group : (parentSplitting hirr hD a p u h hua ht hq ζ).group =
+theorem parentSplitting_group : (parentSplitting hirr hD ev a p u h hua ht hq ζ).group =
     packingGroup (parentSide r) (parentPacking hD a)
       ⟨_, padicValInt_lt_of_taperMult_pos hq hua⟩ :=
-  TensorNetwork.callSplitting_group (RingO hirr) _ (parentNetwork hirr hD) (parentSide r) _ _
+  TensorNetwork.callSplitting_group (RingO hirr) _ (parentNetwork hirr hD ev) (parentSide r) _ _
     (parentPacking hD a) p u h hua ht hq (liftO hirr ζ)
 
 /-- The packets of the splitting are the packets of the packing. -/
 theorem parentSplitting_packet :
-    (parentSplitting hirr hD a p u h hua ht hq ζ).packet = (parentPacking hD a).packet :=
-  TensorNetwork.callSplitting_packet (RingO hirr) _ (parentNetwork hirr hD) (parentSide r) _ _
+    (parentSplitting hirr hD ev a p u h hua ht hq ζ).packet = (parentPacking hD a).packet :=
+  TensorNetwork.callSplitting_packet (RingO hirr) _ (parentNetwork hirr hD ev) (parentSide r) _ _
     (parentPacking hD a) p u h hua ht hq (liftO hirr ζ)
 
 end Fields
@@ -584,7 +588,7 @@ vertex, and the child edges of a packet. -/
 /-- **The descriptors of the numbered child vertices**: the parent descriptor of a retained
 vertex, and the packet descriptor of a packet. -/
 @[expose] def numberedDesc (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ β : List ℕ) :
-    ChildVertex group g P → VertexDesc :=
+    ChildVertex group g P → VertexDesc T :=
   Sum.elim (fun v => (D.vertices[(v.1 : ℕ)]'v.1.2).2) fun q =>
     .inr (packetCtx fl a i pt t ζ g q,
       (packetPorts hD group packet g q).map fun c =>
@@ -917,7 +921,7 @@ local notation "iₜ" => padicValInt 2 t
 /-- The precision of the node. -/
 local notation "ptₜ" => nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)
 /-- The mode splitting at the node. -/
-local notation "S₀" => parentSplitting hirr hD a p u h hua ht hq ζ
+local notation "S₀" => parentSplitting hirr hD ev a p u h hua ht hq ζ
 /-- The mode tuple of `β`. -/
 local notation "β₀" => BudgetTuples.ofList
   (modeList (PacketPacking.Packing.numPackets (parentPacking hD a))
@@ -926,22 +930,22 @@ local notation "β₀" => BudgetTuples.ofList
 /-- The numbering of the child vertices. -/
 local notation "ev₀" =>
   childVertexEquiv (P := PacketPacking.Packing.numPackets (parentPacking hD a))
-  (TensorNetwork.ModeSplitting.group (parentSplitting hirr hD a p u h hua ht hq ζ)) g
+  (TensorNetwork.ModeSplitting.group (parentSplitting hirr hD ev a p u h hua ht hq ζ)) g
 /-- The numbering of the child edges. -/
 local notation "ee₀" => childEdgeEquiv (D.srcFin hD) (D.tgtFin hD)
-  (TensorNetwork.ModeSplitting.group (parentSplitting hirr hD a p u h hua ht hq ζ)) g
+  (TensorNetwork.ModeSplitting.group (parentSplitting hirr hD ev a p u h hua ht hq ζ)) g
 
 /-- **The entries of the retained vertices** of the numbered child are the tensors of the child. -/
 theorem entry_numbered_inl (v : {v // (S₀).group v = g})
     (y : ChildEdge (D.srcFin hD) (D.tgtFin hD) (S₀).group g → Bool) :
     reductionLift (monic_monicOf fl) hirr ptₜ (val ptₜ fl
         ((numberedDesc hD (S₀).group (S₀).packet (fun e => ((parentPacking hD a).slot e : ℕ)) g
-          fl a iₜ ptₜ t ζ β (.inl v)).entry
+          fl a iₜ ptₜ t ζ β (.inl v)).entry ev
           ((numberedPorts hD (S₀).group (S₀).packet g (.inl v)).map y))) =
       ((S₀).child β₀ g).tensor (.inl v) y := by
   rw [TensorNetwork.ModeSplitting.child_tensor_inl_eq_tensor (S₀) β₀ g v y,
     TensorNetwork.map_tensor,
-    ← mk_liftO, parentSplitting_side hirr hD hua ht hq ζ]
+    ← mk_liftO, parentSplitting_side hirr hD ev hua ht hq ζ]
   simp only [numberedDesc, numberedPorts, Sum.elim_inl, parentNetwork,
     DescribedNetwork.toNetwork, DescribedNetwork.wordBits]
   congr 3
@@ -959,13 +963,13 @@ theorem entry_numbered_inr (q : Fin (parentPacking hD a).numPackets)
     (y : ChildEdge (D.srcFin hD) (D.tgtFin hD) (S₀).group g → Bool) :
     reductionLift (monic_monicOf fl) hirr ptₜ (val ptₜ fl
         ((numberedDesc hD (S₀).group (S₀).packet (fun e => ((parentPacking hD a).slot e : ℕ)) g
-          fl a iₜ ptₜ t ζ β (.inr q)).entry
+          fl a iₜ ptₜ t ζ β (.inr q)).entry ev
           ((numberedPorts hD (S₀).group (S₀).packet g (.inr q)).map y))) =
       ((S₀).child β₀ g).tensor (.inr q) y := by
   have hia : iₜ < a := padicValInt_lt_of_taperMult_pos hq hua
   have hsym := PacketPacking.packetSymbols_eq (rowOfP hD) (colOfP hD) _ _ q ⟨iₜ, hia⟩
   simp only [numberedDesc, numberedPorts, Sum.elim_inr]
-  exact TensorNetwork.map_val_entry_child_inr (N := (parentNetwork hirr hD).map
+  exact TensorNetwork.map_val_entry_child_inr (N := (parentNetwork hirr hD ev).map
       (Ideal.Quotient.mk (nodeIdeal (RingO hirr) (Fintype.card (Fin D.numEdges)) a h p t)))
     (parentSide r) (parentSide_src hD) (parentSide_tgt hD)
     (packingGroup_src_tgt (parentSide r) (parentSide_src hD) (parentSide_tgt hD)
@@ -975,7 +979,7 @@ theorem entry_numbered_inr (q : Fin (parentPacking hD a).numPackets)
     (two_pow_padicValInt_dvd_and_not_dvd (Finset.ne_of_mem_erase ht)).2 β₀ g q _
     (nodup_packetPorts hD (S₀).group (S₀).packet g q)
     (fun c => (mem_packetPorts hD (S₀).group (S₀).packet g q c).trans (by
-      rw [parentSplitting_packet hirr hD hua ht hq ζ]
+      rw [parentSplitting_packet hirr hD ev hua ht hq ζ]
       exact Iff.rfl))
     (packetCtx fl a iₜ ptₜ t ζ g q) (betaSlice iₜ ptₜ β q)
     (reductionLift (monic_monicOf fl) hirr ptₜ) (mk_liftO hirr ptₜ ζ).symm rfl rfl rfl rfl rfl rfl
@@ -998,27 +1002,27 @@ theorem contraction_nativeChild :
       (fun d bs => reductionLift (monic_monicOf fl) hirr
         (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t))
         (val (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t)) fl
-          (d.entry bs))) =
-    ((parentSplitting hirr hD a p u h hua ht hq ζ).child
+          (d.entry ev bs))) =
+    ((parentSplitting hirr hD ev a p u h hua ht hq ζ).child
       (BudgetTuples.ofList (modeList (parentPacking hD a).numPackets (2 ^ (padicValInt 2 t + 1))
         (nodePrecision p h a (Fintype.card (Fin D.numEdges)) (padicValInt 2 t))) β)
       g).contraction := by
   have hia : iₜ < a := padicValInt_lt_of_taperMult_pos hq hua
   have hgroups : groupsOf r iₜ D.vertices.length (nativeParentPacking r a D).1 =
       List.ofFn fun v => ((S₀).group v : ℕ) := by
-    rw [parentSplitting_group hirr hD hua ht hq ζ]
+    rw [parentSplitting_group hirr hD ev hua ht hq ζ]
     exact groupsOf_eq hD hK hia
   have hpk1 : (nativeParentPacking r a D).2.1 = (parentPacking hD a).numPackets := by
     rw [nativeParentPacking_eq hD hK]
   have hpk2 : (nativeParentPacking r a D).2.2 =
       List.ofFn fun e => (((S₀).packet e : ℕ), ((parentPacking hD a).slot e : ℕ)) := by
-    rw [nativeParentPacking_eq hD hK, parentSplitting_packet hirr hD hua ht hq ζ]
+    rw [nativeParentPacking_eq hD hK, parentSplitting_packet hirr hD ev hua ht hq ζ]
   rw [nativeChild_eq hD (S₀).group (S₀).packet (fun e => ((parentPacking hD a).slot e : ℕ)) g
     fl a iₜ ptₜ t ζ β _ hgroups hpk1 hpk2]
   refine DescribedNetwork.contraction_eq_of_ports ((S₀).child β₀ g) _ _ _ _ _ ?_
   rintro (v | q) y
-  · exact entry_numbered_inl hirr hD hua ht hq ζ β g v y
-  · exact entry_numbered_inr hirr hD hua ht hq ζ β g q y
+  · exact entry_numbered_inl hirr hD ev hua ht hq ζ β g v y
+  · exact entry_numbered_inr hirr hD ev hua ht hq ζ β g q y
 
 end Child
 
@@ -1026,7 +1030,7 @@ end Parent
 
 /-! ### The descriptors of the native children -/
 
-variable {D : DescribedNetwork VertexDesc} {r : ℕ}
+variable {D : DescribedNetwork (VertexDesc T)} {r : ℕ}
 
 /-- **The descriptors of the native child.** A vertex of the native child of a rows-first parent
 with at least `64 ^ a` edges keeps the descriptor of a parent vertex, or is the packet `q`, with
@@ -1034,7 +1038,7 @@ the packet context of `q`, the slice of `β` at `q`, and tags whose slots are be
 distinct among its row ports. -/
 theorem desc_of_mem_nativeChild (hD : D.IsRowsFirstBipartite r) {fl : List ℕ} {a i : ℕ}
     (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64)
-    {v : List ℕ × VertexDesc}
+    {v : List ℕ × VertexDesc T}
     (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) :
     (∃ w ∈ D.vertices, v.2 = w.2) ∨
       ∃ q tags, v.2 = .inr (packetCtx fl a i pt t ζ g q, tags, betaSlice i pt β q) ∧
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildBounds.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildBounds.lean
index 57b93e560..68e073649 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildBounds.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildBounds.lean
@@ -52,7 +52,8 @@ namespace Cslib.Circuits.Frontier.NativeChild
 
 open Finset ChildNumbering
 
-variable {r a i : ℕ} {D : DescribedNetwork VertexDesc} (hD : D.IsRowsFirstBipartite r)
+variable {T : Type} {r a i : ℕ} {D : DescribedNetwork (VertexDesc T)}
+  (hD : D.IsRowsFirstBipartite r)
 
 /-- The group of a vertex of the parent in coordinate `i < a` of its packing. -/
 noncomputable abbrev parentGroup (a : ℕ) {i : ℕ} (hia : i < a) :
@@ -97,7 +98,7 @@ theorem numEdges_nativeChild_eq (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (fl :
 
 /-- A row of a rows-first network is the row of at most as many edges as it has ports. -/
 theorem card_rowOfP_le (v : Fin r) :
-    #{e | rowOfP hD e = v} ≤ (D.vertices.getD v ([], .inl [])).1.length := by
+    #{e | rowOfP hD e = v} ≤ (D.vertices.getD v defaultVertex).1.length := by
   by_cases hv : (v : ℕ) < D.vertices.length
   · rw [List.getD_eq_getElem _ _ hv]
     calc #{e | rowOfP hD e = v}
@@ -118,7 +119,7 @@ theorem card_rowOfP_le (v : Fin r) :
 
 /-- A column of a rows-first network is the column of at most as many edges as it has ports. -/
 theorem card_colOfP_le (w : Fin (D.vertices.length - r)) :
-    #{e | colOfP hD e = w} ≤ (D.vertices.getD (r + w) ([], .inl [])).1.length := by
+    #{e | colOfP hD e = w} ≤ (D.vertices.getD (r + w) defaultVertex).1.length := by
   have hv : r + (w : ℕ) < D.vertices.length := by have := w.2; omega
   rw [List.getD_eq_getElem _ _ hv]
   calc #{e | colOfP hD e = w}
@@ -142,7 +143,7 @@ theorem sixteen_mul_numEdges_nativeChild_le (hK : 64 ^ a ≤ D.numEdges) (hia :
     (fl : List ℕ) (pt : ℕ) (t : ℤ) (ζ β : List ℕ) (g : Fin 64) :
     16 * (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).numEdges ≤
       D.numEdges := by
-  have hdeg' (v : ℕ) : (D.vertices.getD v ([], .inl [])).1.length ≤ Δ := by
+  have hdeg' (v : ℕ) : (D.vertices.getD v defaultVertex).1.length ≤ Δ := by
     by_cases hv : v < D.vertices.length
     · rw [List.getD_eq_getElem _ _ hv]
       exact hdeg _ (List.getElem_mem hv)
@@ -185,7 +186,7 @@ theorem numPackets_nativeParentPacking_mul_le (hK : 64 ^ a ≤ D.numEdges) {Δ :
     (hdeg : ∀ v ∈ D.vertices, v.1.length ≤ Δ) (hM : 2 * Δ * (64 ^ (2 * a)) ^ 2 ≤ D.numEdges)
     (hL : 2 ^ a * 64 ^ (2 * a) ≤ D.numEdges) :
     (nativeParentPacking r a D).2.1 * 2 ^ a ≤ 3 * D.numEdges := by
-  have hdeg' (v : ℕ) : (D.vertices.getD v ([], .inl [])).1.length ≤ Δ := by
+  have hdeg' (v : ℕ) : (D.vertices.getD v defaultVertex).1.length ≤ Δ := by
     by_cases hv : v < D.vertices.length
     · rw [List.getD_eq_getElem _ _ hv]
       exact hdeg _ (List.getElem_mem hv)
@@ -223,7 +224,7 @@ ports, and a packet vertex has one port per end in group `g` of an edge of its p
 there are at most `2 ^ a`. -/
 theorem length_le_of_mem_vertices_nativeChild (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) {Δ : ℕ}
     (hdeg : ∀ v ∈ D.vertices, v.1.length ≤ Δ) (hL : 2 * 2 ^ a ≤ Δ) (fl : List ℕ) (pt : ℕ) (t : ℤ)
-    (ζ β : List ℕ) (g : Fin 64) {v : List ℕ × VertexDesc}
+    (ζ β : List ℕ) (g : Fin 64) {v : List ℕ × VertexDesc T}
     (hv : v ∈ (nativeChild fl a i pt t ζ r D (nativeParentPacking r a D) β g).vertices) :
     v.1.length ≤ Δ := by
   rw [nativeChild_nativeParentPacking_eq hD hK hia] at hv
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildPolyTime.lean
index a58650892..1ca5f3cfd 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildPolyTime.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/NativeChildPolyTime.lean
@@ -31,7 +31,8 @@ The native child of group `g` of an active call of the contraction recursion of
 computable in polynomial time over the encodings of the native recursion. The counts are unary,
 the node `t` is in binary sign-magnitude form, and the lists are binary, except the exponents
 `β`, which are unary as in a packet descriptor. The parent is encoded by
-`DescribedNetwork.encDescribed VertexDesc.enc` and its packing by
+`DescribedNetwork.encDescribed (VertexDesc.enc encT)`, for any encoding `encT` of the root
+descriptors, and its packing by
 `PacketPacking.encNativePacking`.
 
 The theorems are stated in composition form, for components computed from any input. Besides the
@@ -80,6 +81,8 @@ namespace Cslib.Circuits.Frontier.NativeChild
 
 open Turing.MultiTapeTM ChildNumbering NativePacket
 
+variable {T : Type} {encT : T ↪ List Bool}
+
 /-- **The rank of a port without a loop over the port**: the edges before `e` with an end in group
 `g`, the edges past the list counting as `(0, 0)`. -/
 theorem portRank_eq_countP (groups : List ℕ) (g : ℕ) (ends : List (ℕ × ℕ)) (sel : ℕ × ℕ → ℕ)
@@ -275,9 +278,9 @@ private theorem count_polyTime (hgroups : ComputableInPolyTime groups encIn (enc
   congr 2
 
 /-- **The retained vertices**: the vertices of group `g` with their renumbered ports. -/
-private theorem retained_polyTime {r : δ → ℕ} {V : δ → List (List ℕ × VertexDesc)}
+private theorem retained_polyTime {r : δ → ℕ} {V : δ → List (List ℕ × VertexDesc T)}
     (hr : ComputableInPolyTime r encIn encNat)
-    (hV : ComputableInPolyTime V encIn (encList (encPair (encList encNat) VertexDesc.enc)))
+    (hV : ComputableInPolyTime V encIn (encList (encPair (encList encNat) (VertexDesc.enc encT))))
     (hgroups : ComputableInPolyTime groups encIn (encList encNat))
     (hg : ComputableInPolyTime g encIn encNat)
     (hends : ComputableInPolyTime ends encIn (encList (encPair encNat encNat))) :
@@ -285,7 +288,7 @@ private theorem retained_polyTime {r : δ → ℕ} {V : δ → List (List ℕ ×
       ((List.range (V x).length).filter fun v => decide ((groups x).getD v 0 = g x)).map fun v =>
         (((V x).getD v defaultVertex).1.map (childEdgeOf (r x) (groups x) (g x) (ends x) v),
           ((V x).getD v defaultVertex).2))
-      encIn (encList (encPair (encList encNat) VertexDesc.enc)) := by
+      encIn (encList (encPair (encList encNat) (VertexDesc.enc encT))) := by
   let e₁ := encPair encIn encUnary
   have hx : ComputableInPolyTime (fun p : δ × ℕ => p.1) e₁ encIn := ComputableInPolyTime.fst _ _
   have hy : ComputableInPolyTime (fun p : δ × ℕ => p.2) e₁ encUnary :=
@@ -298,9 +301,9 @@ private theorem retained_polyTime {r : δ → ℕ} {V : δ → List (List ℕ ×
         ((ComputableInPolyTime.listGetD (encA := encNat) (encL := encList encNat) 0).comp
           ((hgroups.comp hx).prod hy)) (hg.comp hx))
   have hvtx : ComputableInPolyTime (fun p : δ × ℕ => (V p.1).getD p.2 defaultVertex) e₁
-      (encPair (encList encNat) VertexDesc.enc) :=
-    (ComputableInPolyTime.listGetD (encA := encPair (encList encNat) VertexDesc.enc)
-      (encL := encList (encPair (encList encNat) VertexDesc.enc)) defaultVertex).comp
+      (encPair (encList encNat) (VertexDesc.enc encT)) :=
+    (ComputableInPolyTime.listGetD (encA := encPair (encList encNat) (VertexDesc.enc encT))
+      (encL := encList (encPair (encList encNat) (VertexDesc.enc encT))) defaultVertex).comp
       ((hV.comp hx).prod hy)
   have hxx : ComputableInPolyTime (fun q : (δ × ℕ) × ℕ => q.1.1) (encPair e₁ encNat) encIn :=
     hx.comp (ComputableInPolyTime.fst _ _)
@@ -332,7 +335,7 @@ private theorem retained_polyTime {r : δ → ℕ} {V : δ → List (List ℕ ×
     hfilter (hports.prod ((ComputableInPolyTime.snd _ _).comp hvtx))
 
 variable {fl ζ β : δ → List ℕ} {a i pt r : δ → ℕ} {t : δ → ℤ}
-  {D : δ → DescribedNetwork VertexDesc}
+  {D : δ → DescribedNetwork (VertexDesc T)}
   {pk : δ → (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)}
 
 /-- **The context of a packet** is polynomial-time, with the packet in unary. -/
@@ -394,8 +397,8 @@ private theorem packetVertices_polyTime {P : δ → ℕ} {cedges : δ → List (
           (childPorts (cedges x) ((groups x).count (g x) + q)).map fun j =>
             (decide (j < (portEdges (groups x) (g x) (ends x) Prod.fst).length),
               ((place x).getD (parentEdge (groups x) (g x) (ends x) j) (0, 0)).2),
-          betaSlice (i x) (pt x) (β x) q) : VertexDesc)))
-      encIn (encList (encPair (encList encNat) VertexDesc.enc)) := by
+          betaSlice (i x) (pt x) (β x) q) : VertexDesc T)))
+      encIn (encList (encPair (encList encNat) (VertexDesc.enc encT))) := by
   let e₁ := encPair encIn encUnary
   have hx : ComputableInPolyTime (fun p : δ × ℕ => p.1) e₁ encIn := ComputableInPolyTime.fst _ _
   have hy : ComputableInPolyTime (fun p : δ × ℕ => p.2) e₁ encUnary :=
@@ -466,7 +469,7 @@ private theorem packing_parts (hpk : ComputableInPolyTime pk encIn PacketPacking
 /-- **The number of rows of the native child is polynomial-time.** -/
 theorem computableInPolyTime_childRows (hr : ComputableInPolyTime r encIn encNat)
     (hi : ComputableInPolyTime i encIn encUnary)
-    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc))
+    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT)))
     (hpk : ComputableInPolyTime pk encIn PacketPacking.encNativePacking)
     (hg : ComputableInPolyTime g encIn encNat) :
     ComputableInPolyTime (fun x => childRows (r x) (i x) (D x) (pk x) (g x)) encIn encNat :=
@@ -486,17 +489,17 @@ theorem computableInPolyTime_nativeChild (hfl : ComputableInPolyTime fl encIn (e
     (hpt : ComputableInPolyTime pt encIn encUnary) (ht : ComputableInPolyTime t encIn encIntBin)
     (hζ : ComputableInPolyTime ζ encIn (encList encNat))
     (hr : ComputableInPolyTime r encIn encNat)
-    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc))
+    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT)))
     (hpk : ComputableInPolyTime pk encIn PacketPacking.encNativePacking)
     (hP : ComputableInPolyTime (fun x => (pk x).2.1) encIn encUnary)
     (hβ : ComputableInPolyTime β encIn (encList encUnary))
     (hg : ComputableInPolyTime g encIn encNat) :
     ComputableInPolyTime (fun x =>
       nativeChild (fl x) (a x) (i x) (pt x) (t x) (ζ x) (r x) (D x) (pk x) (β x) (g x))
-      encIn (DescribedNetwork.encDescribed VertexDesc.enc) := by
+      encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT)) := by
   obtain ⟨hwords, hplace⟩ := packing_parts hpk
   have hV := DescribedNetwork.vertices_polyTime.comp hD
-  have hends := (DescribedNetwork.computableInPolyTime_edgeEnds VertexDesc.enc).comp hD
+  have hends := (DescribedNetwork.computableInPolyTime_edgeEnds (VertexDesc.enc encT)).comp hD
   have hgroups := computableInPolyTime_groupsOf hr hi
     ((ComputableInPolyTime.length_list _).comp hV) hwords
   have hpackets : ComputableInPolyTime (fun x => (pk x).2.2.map Prod.fst) encIn
@@ -510,9 +513,9 @@ theorem computableInPolyTime_nativeChild (hfl : ComputableInPolyTime fl encIn (e
   have hpair := ((ComputableInPolyTime.length_list _).comp hcedges).prod
     (ComputableInPolyTime.listAppend' (retained_polyTime hr hV hgroups hg hends)
       (packetVertices_polyTime hfl ha hL hi hT hpt ht hζ hβ hg hgroups hends hP hcedges hplace))
-  have hsymm : ComputableInPolyTime (DescribedNetwork.equivProd (T := VertexDesc)).symm
-      (encPair encUnary (encList (encPair (encList encNat) VertexDesc.enc)))
-      (DescribedNetwork.encDescribed VertexDesc.enc) :=
+  have hsymm : ComputableInPolyTime (DescribedNetwork.equivProd (T := VertexDesc T)).symm
+      (encPair encUnary (encList (encPair (encList encNat) (VertexDesc.enc encT))))
+      (DescribedNetwork.encDescribed (VertexDesc.enc encT)) :=
     ComputableInPolyTime.of_eq fun y => by
       rw [DescribedNetwork.encDescribed, encOfEquiv_apply, Equiv.apply_symm_apply]
   exact (hsymm.comp hpair).of_enc_eq fun x => by
@@ -534,7 +537,7 @@ private theorem foldl_max_le {l : List ℕ} {m n : ℕ} (hm : m ≤ n) (hl : ∀
 /-- **At most `M (2 ^ a) ^ 12` packets**: the native parent packing of a network with `M` edges
 has at most one block of `2 ^ a` slots per edge, times the `4096 ^ a` words of pairs of
 symbols. -/
-theorem numPackets_nativeParentPacking_le (r a : ℕ) (D : DescribedNetwork VertexDesc) :
+theorem numPackets_nativeParentPacking_le (r a : ℕ) (D : DescribedNetwork (VertexDesc T)) :
     (nativeParentPacking r a D).2.1 ≤ D.numEdges * (2 ^ a) ^ 12 := by
   set pairs := PacketPacking.edgeWordPairs (PacketPacking.labelWords r (D.vertices.length - r) a 64
     (D.edgeEnds.map fun e => (e.1, e.2 - r))).1 (PacketPacking.labelWords r
@@ -576,16 +579,16 @@ theorem numPackets_nativeParentPacking_le (r a : ℕ) (D : DescribedNetwork Vert
 section PolyTime
 
 variable {δ : Type} {encIn : δ ↪ List Bool} {fl ζ β : δ → List ℕ} {a i pt r g : δ → ℕ}
-  {t : δ → ℤ} {D : δ → DescribedNetwork VertexDesc}
+  {t : δ → ℤ} {D : δ → DescribedNetwork (VertexDesc T)}
 
 /-- **The native parent packing is polynomial-time**, with the number of rows and `a` in
 unary. -/
 theorem computableInPolyTime_nativeParentPacking (hr : ComputableInPolyTime r encIn encUnary)
     (ha : ComputableInPolyTime a encIn encUnary)
-    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) :
+    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT))) :
     ComputableInPolyTime (fun x => nativeParentPacking (r x) (a x) (D x)) encIn
       PacketPacking.encNativePacking := by
-  have hends := (DescribedNetwork.computableInPolyTime_edgeEnds VertexDesc.enc).comp hD
+  have hends := (DescribedNetwork.computableInPolyTime_edgeEnds (VertexDesc.enc encT)).comp hD
   have hrb := ComputableInPolyTime.unary_to_binary.comp hr
   have hshift : ComputableInPolyTime (fun x => (D x).edgeEnds.map fun e => (e.1, e.2 - r x))
       encIn (encList (encPair encNat encNat)) :=
@@ -610,7 +613,7 @@ and `2 ^ a` in unary. -/
 theorem computableInPolyTime_numPackets_nativeParentPacking
     (hr : ComputableInPolyTime r encIn encUnary) (ha : ComputableInPolyTime a encIn encUnary)
     (hL : ComputableInPolyTime (fun x => 2 ^ a x) encIn encUnary)
-    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc)) :
+    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT))) :
     ComputableInPolyTime (fun x => (nativeParentPacking (r x) (a x) (D x)).2.1) encIn
       encUnary := by
   have hpk : ComputableInPolyTime (fun x => nativeParentPacking (r x) (a x) (D x)) encIn
@@ -634,12 +637,12 @@ theorem computableInPolyTime_nativeChild_nativeParentPacking
     (hpt : ComputableInPolyTime pt encIn encUnary) (ht : ComputableInPolyTime t encIn encIntBin)
     (hζ : ComputableInPolyTime ζ encIn (encList encNat))
     (hr : ComputableInPolyTime r encIn encUnary)
-    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc))
+    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT)))
     (hβ : ComputableInPolyTime β encIn (encList encUnary))
     (hg : ComputableInPolyTime g encIn encNat) :
     ComputableInPolyTime (fun x => nativeChild (fl x) (a x) (i x) (pt x) (t x) (ζ x) (r x) (D x)
       (nativeParentPacking (r x) (a x) (D x)) (β x) (g x))
-      encIn (DescribedNetwork.encDescribed VertexDesc.enc) :=
+      encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT)) :=
   computableInPolyTime_nativeChild hfl ha hL hi hT hpt ht hζ
     (ComputableInPolyTime.unary_to_binary.comp hr) hD
     (computableInPolyTime_nativeParentPacking hr ha hD)
@@ -649,7 +652,7 @@ theorem computableInPolyTime_nativeChild_nativeParentPacking
 theorem computableInPolyTime_childRows_nativeParentPacking
     (hr : ComputableInPolyTime r encIn encUnary) (ha : ComputableInPolyTime a encIn encUnary)
     (hi : ComputableInPolyTime i encIn encUnary)
-    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed VertexDesc.enc))
+    (hD : ComputableInPolyTime D encIn (DescribedNetwork.encDescribed (VertexDesc.enc encT)))
     (hg : ComputableInPolyTime g encIn encNat) :
     ComputableInPolyTime (fun x => childRows (r x) (i x) (D x)
       (nativeParentPacking (r x) (a x) (D x)) (g x)) encIn encNat :=
@@ -662,7 +665,8 @@ end PolyTime
 
 section Shape
 
-variable (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ : List ℕ) (r : ℕ) (D : DescribedNetwork VertexDesc)
+variable (fl : List ℕ) (a i pt : ℕ) (t : ℤ) (ζ : List ℕ) (r : ℕ)
+  (D : DescribedNetwork (VertexDesc T))
   (pk : (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)) (β : List ℕ) (g : ℕ)
 
 /-- **The child has at most twice as many edges as the parent**: one per end of a parent edge in
@@ -701,7 +705,7 @@ theorem length_vertices_nativeChild :
 either a parent vertex with renumbered ports, with the same descriptor and the same number of
 ports, or the vertex of a packet `q`, whose descriptor is its context, tags of its ports with
 slots from the packing (or `0`), and its slice of `β`. -/
-theorem mem_vertices_nativeChild {v : List ℕ × VertexDesc}
+theorem mem_vertices_nativeChild {v : List ℕ × VertexDesc T}
     (hv : v ∈ (nativeChild fl a i pt t ζ r D pk β g).vertices) :
     (∃ w ∈ D.vertices, v.2 = w.2 ∧ v.1.length = w.1.length) ∨
       ∃ q < pk.2.1, ∃ tags : List (Bool × ℕ),
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/PacketTerms.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/PacketTerms.lean
index f614aa598..7280a7577 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/PacketTerms.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/PacketTerms.lean
@@ -723,6 +723,7 @@ structure PacketCtx where
   cols : List (ℕ × Bool)
   /-- The interpolation value. -/
   ζ : List ℕ
+  deriving Inhabited
 
 namespace PacketCtx
 
diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/VertexDesc.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/VertexDesc.lean
index 3fff52005..4f620b30f 100644
--- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/VertexDesc.lean
+++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/VertexDesc.lean
@@ -22,30 +22,34 @@ import Mathlib.Data.List.GetD
 # Descriptors of the vertices of the recursion's networks
 
 The networks of the contraction recursion of [OpenAI2026ETH] (§D.4.6–§D.4.7, pp. 63–64) have two
-kinds of vertices. The vertices of the input network keep their tables, and they survive into
-every child of their group with the same ports. The packet vertices created at a call are
-described by "its packet data, the tuple `β`, the interpolation value, and the creation
-precision" (p. 63), and from then on they also survive into the children of their group. A
-vertex descriptor (`VertexDesc`) is therefore a table or a packet descriptor
+kinds of vertices. The vertices of the input network keep their original descriptions, and they
+survive into every child of their group with the same ports. The packet vertices created at a call
+are described by "its packet data, the tuple `β`, the interpolation value, and the creation
+precision" (p. 63), and from then on they also survive into the children of their group. A vertex
+descriptor (`VertexDesc T`) is therefore a root descriptor of type `T` or a packet descriptor
 (`NativePacket.PacketDesc`), and a retained vertex keeps its descriptor.
 
-`VertexDesc.entry` evaluates a descriptor at the bits on its ports: the table entry, as a constant
-coefficient list, or the native packet entry at the packet's creation precision. A network of the
-recursion reads the entries at its own precision `(p, fl)` (`GaloisRingArith.val p fl`), so a
-retained packet vertex created at a lower precision is read at the higher one: its coefficients
-are those of the same element of `O = ℤ_(2)[U] / (f)`. One native machine evaluates every
-descriptor (`VertexDesc.entryCertificate`), with the packet evaluator's bounds: time
-`K (m + 2) ^ L Z ^ K` and space `K Z ^ K`, for `m` target modes and `L` row ports of a packet (none
-for a table) and `Z` polynomial in the input and the reduced coefficient lists
-(`VertexDesc.entryCertificate_le`). It is the evaluator of direct summation over networks of
-descriptors at coefficient lists (`DescribedNetwork.contractionCertificate` at `SumOps.galois`).
+`VertexDesc.entry ev` evaluates a descriptor at the bits on its ports: the root's entry procedure
+`ev`, which returns a coefficient list, or the native packet entry at the packet's creation
+precision. A network of the recursion reads the entries at its own precision `(p, fl)`
+(`GaloisRingArith.val p fl`), so a vertex is read at every precision through the canonical lift of
+its coefficient list: a retained packet vertex created at a lower precision is read at the higher
+one as the same element of `O = ℤ_(2)[U] / (f)`. Explicit tables are the root descriptors
+`T = List ℕ` with the entry procedure `tableEntry`, which returns the table entry as a constant.
+For tables, one native machine evaluates every descriptor (`VertexDesc.entryCertificate`), with
+the packet evaluator's bounds: time `K (m + 2) ^ L Z ^ K` and space `K Z ^ K`, for `m` target modes
+and `L` row ports of a packet (none for a table) and `Z` polynomial in the input and the reduced
+coefficient lists (`VertexDesc.entryCertificate_le`). It is the evaluator of direct summation over
+networks of descriptors at coefficient lists (`DescribedNetwork.contractionCertificate` at
+`SumOps.galois`).
 
 ## Main definitions
 
-* `Cslib.Circuits.Frontier.VertexDesc`: a table or a packet descriptor.
+* `Cslib.Circuits.Frontier.tableEntry`: the entry procedure of tables.
+* `Cslib.Circuits.Frontier.VertexDesc`: a root descriptor or a packet descriptor.
 * `Cslib.Circuits.Frontier.VertexDesc.entry`: its entry at the bits on its ports.
 * `Cslib.Circuits.Frontier.VertexDesc.enc`: its encoding.
-* `Cslib.Circuits.Frontier.VertexDesc.entryCertificate`: the native evaluator.
+* `Cslib.Circuits.Frontier.VertexDesc.entryCertificate`: the native evaluator, for tables.
 
 ## Main results
 
@@ -68,55 +72,62 @@ local notation "ℤ₍₂₎" => Valuation.integer (Rat.padicValuation 2)
 
 open GaloisRingArith NativePacket TensorNetwork Turing.MultiTapeTM Cslib.GenericRAM
 
-/-- **The descriptor of a vertex** of a network of the contraction recursion: the table of a
+/-- **The entry procedure of tables**: the table entry at the bits on the ports, as a constant
+coefficient list. -/
+@[expose] def tableEntry (table : List ℕ) (bs : List Bool) : List ℕ :=
+  [ExplicitTensorNetwork.entry table bs]
+
+/-- **The descriptor of a vertex** of a network of the contraction recursion: the descriptor of a
 vertex of the input network (`inl`), or the descriptor of a packet vertex (`inr`). -/
-abbrev VertexDesc : Type := List ℕ ⊕ PacketDesc
+abbrev VertexDesc (T : Type) : Type := T ⊕ PacketDesc
 
 namespace VertexDesc
 
-/-- **The entry of a vertex at the bits on its ports**: the table entry, as a constant coefficient
-list, or the native packet entry at the packet's creation precision. -/
-@[expose] def entry : VertexDesc → List Bool → List ℕ
-  | .inl table, bs => [ExplicitTensorNetwork.entry table bs]
+variable {T : Type}
+
+/-- **The entry of a vertex at the bits on its ports**: the entry procedure `ev` of the input
+network, or the native packet entry at the packet's creation precision. -/
+@[expose] def entry (ev : T → List Bool → List ℕ) : VertexDesc T → List Bool → List ℕ
+  | .inl t, bs => ev t bs
   | .inr d, bs => packetVertexEntry d bs
 
-/-- The encoding of a descriptor: a tag, then the table in binary or the packet descriptor. -/
-abbrev enc : VertexDesc ↪ List Bool := encSum (encList encNat) encPacketDesc
+/-- The encoding of a descriptor: a tag, then the root descriptor or the packet descriptor. -/
+abbrev enc (encT : T ↪ List Bool) : VertexDesc T ↪ List Bool := encSum encT encPacketDesc
 
-/-- The number of target modes of a descriptor: those of its packet, and none for a table. -/
-@[expose] def modes : VertexDesc → ℕ
+/-- The number of target modes of a descriptor: those of its packet, and none for a root. -/
+@[expose] def modes : VertexDesc T → ℕ
   | .inl _ => 0
   | .inr d => (targetModes d.1).length
 
 /-- The number of row ports of a descriptor at the bits on its ports: those of its packet, and
-none for a table. -/
-@[expose] def rowPorts : VertexDesc → List Bool → ℕ
+none for a root. -/
+@[expose] def rowPorts : VertexDesc T → List Bool → ℕ
   | .inl _, _ => 0
   | .inr d, bs => (sidePorts d.2.1 bs true).length
 
 /-- The reduced coefficient lists of the creation precision of a descriptor are at most `Rv` bits
-long; no condition for a table. -/
-@[expose] def ReducedLE (Rv : ℕ) : VertexDesc → Prop
+long; no condition for a root. -/
+@[expose] def ReducedLE (Rv : ℕ) : VertexDesc T → Prop
   | .inl _ => True
   | .inr d => ∀ y, SumOps.galois.Reduced (d.1.p, d.1.fl) y → (encList encNat y).length ≤ Rv
 
 /-! ### Values -/
 
-@[simp] theorem entry_inl (table : List ℕ) (bs : List Bool) :
-    entry (.inl table) bs = [ExplicitTensorNetwork.entry table bs] := rfl
+@[simp] theorem entry_inl (ev : T → List Bool → List ℕ) (t : T) (bs : List Bool) :
+    entry ev (.inl t) bs = ev t bs := rfl
 
-@[simp] theorem entry_inr (d : PacketDesc) (bs : List Bool) :
-    entry (.inr d) bs = packetVertexEntry d bs := rfl
+@[simp] theorem entry_inr (ev : T → List Bool → List ℕ) (d : PacketDesc) (bs : List Bool) :
+    entry ev (.inr d) bs = packetVertexEntry d bs := rfl
 
 /-- **A table entry is read as a constant** at every precision. -/
 theorem val_entry_inl (p : ℕ) (fl table : List ℕ) (bs : List Bool) :
-    val p fl (entry (.inl table) bs) =
+    val p fl (entry tableEntry (.inl table) bs) =
       ((ExplicitTensorNetwork.entry table bs : ℕ) : Ring p fl) := by
   obtain h | ⟨e, he⟩ : fl.length = 0 ∨ ∃ e, fl.length = e + 1 :=
     (Nat.eq_zero_or_pos _).imp id fun h => ⟨_, (Nat.succ_pred_eq_of_pos h).symm⟩
   · have := subsingleton_of_length_eq_zero (p := p) h
     exact Subsingleton.elim _ _
-  · rw [entry_inl, val, he, Finset.sum_range_succ',
+  · rw [entry_inl, tableEntry, val, he, Finset.sum_range_succ',
       Finset.sum_eq_zero fun i _ => by rw [List.getD_cons_succ, List.getD_nil]; simp]
     simp
 
@@ -124,12 +135,13 @@ theorem val_entry_inl (p : ℕ) (fl table : List ℕ) (bs : List Bool) :
 precision `p` of the packet, to a ring in which `2` is nilpotent, the entry of a packet descriptor
 at the bits on its ports is `packetEntry` at any ring map `κ : ℤ_(2) → S`, the image of the
 interpolation value, the dense exponents, and the row and column ports read from the bits. -/
-theorem map_val_entry_inr {S : Type*} [CommRing S] (d : PacketDesc) (bs : List Bool)
-    (ψ : Ring d.1.p d.1.fl →+* S) {n : ℕ} (hn : (2 : S) ^ n = 0) (κ : ℤ₍₂₎ →+* S)
+theorem map_val_entry_inr {S : Type*} [CommRing S] (ev : T → List Bool → List ℕ)
+    (d : PacketDesc) (bs : List Bool) (ψ : Ring d.1.p d.1.fl →+* S) {n : ℕ}
+    (hn : (2 : S) ^ n = 0) (κ : ℤ₍₂₎ →+* S)
     (hL : d.1.L = 2 ^ d.1.a) (hia : d.1.i < d.1.a) (htiles : d.1.tiles = 2 ^ (d.1.i + 1))
     (ht : d.1.t ∈ cauchyGrid (2 ^ d.1.a)) (hti : (2 : ℤ) ^ d.1.i ∣ d.1.t)
     (hti' : ¬ (2 : ℤ) ^ (d.1.i + 1) ∣ d.1.t) (hports : ∀ x ∈ d.2.1, x.2 < 2 ^ d.1.a) :
-    ψ (val d.1.p d.1.fl (entry (.inr d) bs)) =
+    ψ (val d.1.p d.1.fl (entry ev (.inr d) bs)) =
       packetEntry (p := d.1.nb) κ (ψ (val d.1.p d.1.fl d.1.ζ)) d.1.a d.1.i d.1.t d.1.e₁ d.1.e₂
         d.1.differ (fun Z => d.2.2.getD (finProdFinEquiv Z) 0) (sidePorts d.2.1 bs true)
         (sidePorts d.2.1 bs false) := by
@@ -142,33 +154,35 @@ theorem map_val_entry_inr {S : Type*} [CommRing S] (d : PacketDesc) (bs : List B
     htiles ht hti hti' (hside true) (hside false) d.2.2
 
 /-- A packet entry is a reduced coefficient list at the packet's precision. -/
-theorem reduced_entry_inr (d : PacketDesc) (bs : List Bool) :
-    SumOps.galois.Reduced (d.1.p, d.1.fl) (entry (.inr d) bs) :=
+theorem reduced_entry_inr (ev : T → List Bool → List ℕ) (d : PacketDesc) (bs : List Bool) :
+    SumOps.galois.Reduced (d.1.p, d.1.fl) (entry ev (.inr d) bs) :=
   SumOps.galois.reduced_mul (d.1.p, d.1.fl) _ _
 
-/-! ### The native evaluator -/
+/-! ### The native evaluator of tables -/
 
 /-- The right summand of a descriptor and its bits. -/
 theorem getRight_polyTime :
-    ComputableInPolyTime (fun q : VertexDesc × List Bool => q.1.getRight?) (encPair enc encBits)
-      (encOption encPacketDesc) :=
+    ComputableInPolyTime (fun q : VertexDesc (List ℕ) × List Bool => q.1.getRight?)
+      (encPair (enc (encList encNat)) encBits) (encOption encPacketDesc) :=
   (ComputableInO.getRight?_deg _ _).computableInPolyTime.comp (ComputableInPolyTime.fst _ _)
 
 /-- The table entry of a descriptor at its bits, the empty table standing for a packet, as a
 singleton list. -/
 theorem tableEntry_polyTime :
-    ComputableInPolyTime (fun q : VertexDesc × List Bool =>
-      [ExplicitTensorNetwork.entry (q.1.getLeft?.getD []) q.2]) (encPair enc encBits)
-      (encList encNat) := by
-  have hleft : ComputableInPolyTime (fun q : VertexDesc × List Bool => q.1.getLeft?)
-      (encPair enc encBits) (encOption (encList encNat)) :=
+    ComputableInPolyTime (fun q : VertexDesc (List ℕ) × List Bool =>
+      [ExplicitTensorNetwork.entry (q.1.getLeft?.getD []) q.2])
+      (encPair (enc (encList encNat)) encBits) (encList encNat) := by
+  have hleft : ComputableInPolyTime (fun q : VertexDesc (List ℕ) × List Bool => q.1.getLeft?)
+      (encPair (enc (encList encNat)) encBits) (encOption (encList encNat)) :=
     (ComputableInO.getLeft?_deg _ _).computableInPolyTime.comp (ComputableInPolyTime.fst _ _)
-  have htable : ComputableInPolyTime (fun q : VertexDesc × List Bool => q.1.getLeft?.getD [])
-      (encPair enc encBits) (encList encNat) :=
+  have htable : ComputableInPolyTime
+      (fun q : VertexDesc (List ℕ) × List Bool => q.1.getLeft?.getD [])
+      (encPair (enc (encList encNat)) encBits) (encList encNat) :=
     (ComputableInDegree.getD (enc₁ := encList encNat) (enc := encOption (encList encNat))
       []).computableInPolyTime.comp hleft
   have hindex := ComputableInPolyTime.bitsBinaryValue.comp
-    (ComputableInPolyTime.bitsReverse.comp (ComputableInPolyTime.snd enc encBits))
+    (ComputableInPolyTime.bitsReverse.comp
+      (ComputableInPolyTime.snd (enc (encList encNat)) encBits))
   have hentry := ComputableInPolyTime.listGetD_binary (encA := encNat) (encL := encList encNat) 0
     htable hindex
   exact (ComputableInPolyTime.cons' hentry (ComputableInPolyTime.const [])).of_enc_eq fun q => by
@@ -177,17 +191,18 @@ theorem tableEntry_polyTime :
 
 /-- The input of the packet evaluator from a descriptor's bits and its packet. -/
 theorem packetInput_polyTime :
-    ComputableInPolyTime (fun p : (VertexDesc × List Bool) × PacketDesc => (p.2, p.1.2))
-      (encPair (encPair enc encBits) encPacketDesc) (encPair encPacketDesc encBits) :=
+    ComputableInPolyTime (fun p : (VertexDesc (List ℕ) × List Bool) × PacketDesc => (p.2, p.1.2))
+      (encPair (encPair (enc (encList encNat)) encBits) encPacketDesc)
+      (encPair encPacketDesc encBits) :=
   (ComputableInPolyTime.snd _ _).prod
-    ((ComputableInPolyTime.snd enc encBits).comp (ComputableInPolyTime.fst _ _))
+    ((ComputableInPolyTime.snd (enc (encList encNat)) encBits).comp (ComputableInPolyTime.fst _ _))
 
-/-- **One native machine for the entries of all descriptors**: the table lookup for a table, and
-the native packet evaluator (`NativePacket.vertexCertificate`) for a packet. -/
+/-- **One native machine for the entries of all descriptors over tables**: the table lookup for a
+table, and the native packet evaluator (`NativePacket.vertexCertificate`) for a packet. -/
 noncomputable def entryCertificate :
-    NativeCertificate (fun q : VertexDesc × List Bool => entry q.1 q.2) (encPair enc encBits)
-      (encList encNat) :=
-  (NativeCertificate.option (value := fun q : VertexDesc × List Bool => q.1.getRight?)
+    NativeCertificate (fun q : VertexDesc (List ℕ) × List Bool => entry tableEntry q.1 q.2)
+      (encPair (enc (encList encNat)) encBits) (encList encNat) :=
+  (NativeCertificate.option (value := fun q : VertexDesc (List ℕ) × List Bool => q.1.getRight?)
     (fallback := fun q => [ExplicitTensorNetwork.entry (q.1.getLeft?.getD []) q.2])
     (body := fun p => packetVertexEntry p.2 p.1.2)
     (NativeCertificate.ofPolyTime getRight_polyTime)
@@ -208,11 +223,11 @@ table), if the reduced coefficient lists of a packet's precision are at most `Rv
 with `Z = n + m + Rv + 2` the time is at most `K (m + 2) ^ L Z ^ K` and the space at most
 `K Z ^ K`. -/
 theorem entryCertificate_le :
-    ∃ K : ℕ, ∀ (q : VertexDesc × List Bool) (Rv : ℕ), q.1.ReducedLE Rv →
+    ∃ K : ℕ, ∀ (q : VertexDesc (List ℕ) × List Bool) (Rv : ℕ), q.1.ReducedLE Rv →
       entryCertificate.time q ≤ K * (q.1.modes + 2) ^ q.1.rowPorts q.2 *
-          ((encPair enc encBits q).length + q.1.modes + Rv + 2) ^ K ∧
+          ((encPair (enc (encList encNat)) encBits q).length + q.1.modes + Rv + 2) ^ K ∧
         entryCertificate.space q ≤
-          K * ((encPair enc encBits q).length + q.1.modes + Rv + 2) ^ K := by
+          K * ((encPair (enc (encList encNat)) encBits q).length + q.1.modes + Rv + 2) ^ K := by
   obtain ⟨K₀, hK₀⟩ := vertexCertificate_le
   have hR := NativeCertificate.ofPolyTime_isPolynomial getRight_polyTime
   have hT := NativeCertificate.ofPolyTime_isPolynomial tableEntry_polyTime
@@ -227,7 +242,7 @@ theorem entryCertificate_le :
   obtain ⟨G, hG⟩ : ∃ G, G = K₀ + 2 * cr + 2 * cr' + ct + ct' + ci * 3 ^ di + ci' * 3 ^ di' + 1 :=
     ⟨_, rfl⟩
   refine ⟨G + D, fun q Rv hRv => ?_⟩
-  obtain ⟨n, hn⟩ : ∃ n, n = (encPair enc encBits q).length := ⟨_, rfl⟩
+  obtain ⟨n, hn⟩ : ∃ n, n = (encPair (enc (encList encNat)) encBits q).length := ⟨_, rfl⟩
   obtain ⟨Z, hZ⟩ : ∃ Z, Z = n + q.1.modes + Rv + 2 := ⟨_, rfl⟩
   obtain ⟨P, hP⟩ : ∃ P, P = (q.1.modes + 2) ^ q.1.rowPorts q.2 := ⟨_, rfl⟩
   rw [← hn, ← hZ, ← hP]
@@ -278,10 +293,12 @@ theorem entryCertificate_le :
       have h3 : (encPair encPacketDesc encBits (d, bs)).length =
           2 * (encPacketDesc d).length + 1 + (encBits bs).length := length_encPair _
       omega
-    have hlenI : (encPair (encPair enc encBits) encPacketDesc ((.inr d, bs), d)).length + 1 ≤
-        3 * Z := by
-      have h1 : (encPair (encPair enc encBits) encPacketDesc ((.inr d, bs), d)).length =
-          2 * (encPair enc encBits (.inr d, bs)).length + 1 + (encPacketDesc d).length :=
+    have hlenI : (encPair (encPair (enc (encList encNat)) encBits) encPacketDesc
+        ((.inr d, bs), d)).length + 1 ≤ 3 * Z := by
+      have h1 : (encPair (encPair (enc (encList encNat)) encBits) encPacketDesc
+          ((.inr d, bs), d)).length =
+          2 * (encPair (enc (encList encNat)) encBits (.inr d, bs)).length + 1 +
+            (encPacketDesc d).length :=
         length_encPair _
       omega
     have hpow3 {c e : ℕ} (he : e ≤ D) : c * (3 * Z) ^ e ≤ c * 3 ^ e * Z ^ D := by
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean
index e652204be..483fcbb67 100644
--- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAlgorithm.lean
@@ -298,7 +298,7 @@ section Resources
 
 open FastContraction Cslib.GenericRAM Cslib.GenericRAM.StackRecursion Turing.MultiTapeTM
 
-variable (mk : Call → ChildCursor.State → ℕ × DescribedNetwork VertexDesc)
+variable (mk : Call (List ℕ) → ChildCursor.State → ℕ × DescribedNetwork (VertexDesc (List ℕ)))
 
 /-- **The resource analysis of the fast machine**, the remaining obligation of the running time.
 For all constants `C` and `D` there are `K` and `s₀` such that on every input `(P, r, G)` with
@@ -310,13 +310,14 @@ whose leaves take time at most `TL` and space at most `SL`, with `H` open calls,
 @[expose] def FastAnalysis : Prop :=
   ∀ C D : ℕ, ∃ K s₀ : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → 1 ≤ P →
     P ≤ D * s → ExplicitAdmissible C s G → fastGuard G = true →
-    ∃ (I : Invariant Call Frame (ℕ × List ℕ)) (N H F TL SL : ℕ),
-      (scheme mk).Eval I (root (ExplicitTensorNetwork.capPrecision (P, G)))
-        (0, value mk (root (ExplicitTensorNetwork.capPrecision (P, G)))) N H ∧
+    ∃ (I : Invariant (Call (List ℕ)) Frame (ℕ × List ℕ)) (N H F TL SL : ℕ),
+      (scheme tableEntry mk).Eval I (root (ExplicitTensorNetwork.capPrecision (P, G)))
+        (0, value tableEntry mk (root (ExplicitTensorNetwork.capPrecision (P, G)))) N H ∧
       (s₀ ≤ s → 2 * N - 1 ≤ fuel (ExplicitTensorNetwork.capPrecision (P, G))) ∧
-      (∀ x, I.node x → (encCall x).length ≤ F ∧ ((scheme mk).isLeaf x = true →
+      (∀ x, I.node x → (encCall (encList encNat) x).length ≤ F ∧
+        ((scheme tableEntry mk).isLeaf x = true →
         (leafCertificate mk).time x ≤ TL ∧ (leafCertificate mk).space x ≤ SL)) ∧
-      (∀ x a, I.frame x a → (encPair encCall encFrame (x, a)).length ≤ F) ∧
+      (∀ x a, I.frame x a → (encPair (encCall (encList encNat)) encFrame (x, a)).length ≤ F) ∧
       (∀ v, I.value v → (encValue v).length ≤ F) ∧
       H + F + SL ≤ K * ((FastContraction.encInput (P, G)).length + 1) ^ K ∧
       TL ≤ K * ((FastContraction.encInput (P, G)).length + 1) ^ K *
@@ -362,7 +363,8 @@ scheme and the resource analysis, for all constants `C` and `D` there is `K` suc
 guarded input admissible at size `s ≥ 2` with constant `C` and with precision `1 ≤ P ≤ D s`, the
 fast machine takes time at most `K (n + 1) ^ K 2 ^ (K s / √⌊log₂ s⌋)` and space at most
 `K (n + 1) ^ K`. -/
-theorem fastCertificate_le (hpoly : (scheme mk).PolyTime encCall encFrame encValue)
+theorem fastCertificate_le
+    (hpoly : (scheme tableEntry mk).PolyTime (encCall (encList encNat)) encFrame encValue)
     (hana : FastAnalysis mk) (C D : ℕ) :
     ∃ K : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → 1 ≤ P → P ≤ D * s →
       ExplicitAdmissible C s G → fastGuard G = true →
@@ -496,8 +498,8 @@ theorem fastCertificate_le (hpoly : (scheme mk).PolyTime encCall encFrame encVal
           K₂ * ((encInput q).length + 1) ^ K₂ * 2 ^ (C * s₀) :=
             Nat.le_mul_of_pos_right _ Nat.one_le_two_pow
         _ = K₂ * 2 ^ (C * s₀) * B ^ K₂ := by ring)
-  have hbig : s₀ ≤ s → (scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q) =
-      some (0, value mk (root (ExplicitTensorNetwork.capPrecision q))) :=
+  have hbig : s₀ ≤ s → (scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q) =
+      some (0, value tableEntry mk (root (ExplicitTensorNetwork.capPrecision q))) :=
     fun h => Scheme.run_eq_some he (hN h)
   clear hKa hK₁ hK₂ h₁ h₂
   -- Everything against `W = B ^ E X`.
@@ -548,7 +550,7 @@ theorem fastCertificate_le (hpoly : (scheme mk).PolyTime encCall encFrame encVal
     Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega)))
   refine ⟨?_, ?_⟩
   · rw [fastCertificate_time]
-    have hrest : ((scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
+    have hrest : ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
         (ExplicitTensorNetwork.directContractionBinaryCertificate.time q) (fun v =>
           (NativeCertificate.ofPolyTime tag_polyTime).time (q, v) +
             if decide (v.1 = 0) = true then
@@ -556,7 +558,8 @@ theorem fastCertificate_le (hpoly : (scheme mk).PolyTime encCall encFrame encVal
             else (NativeCertificate.ofPolyTime
                 (ComputableInPolyTime.fst FastContraction.encInput encValue)).time (q, v) +
               ExplicitTensorNetwork.directContractionBinaryCertificate.time q) ≤ R₁ + R₂ := by
-      rcases hr : (scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q) with _ | v
+      rcases hr : (scheme tableEntry mk).run fuel root
+        (ExplicitTensorNetwork.capPrecision q) with _ | v
       · by_cases hs₀ : s₀ ≤ s
         · rw [hbig hs₀] at hr; cases hr
         · simp only [Option.elim_none]; have := hdir (by omega); omega
@@ -579,7 +582,7 @@ theorem fastCertificate_le (hpoly : (scheme mk).PolyTime encCall encFrame encVal
         rw [hWdef, ← Nat.mul_assoc]
         exact Nat.mul_le_mul (Nat.mul_le_mul hKK hBE) hXK
   · rw [fastCertificate_space]
-    have hrest : ((scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
+    have hrest : ((scheme tableEntry mk).run fuel root (ExplicitTensorNetwork.capPrecision q)).elim
         (ExplicitTensorNetwork.directContractionBinaryCertificate.space q) (fun v =>
           (NativeCertificate.ofPolyTime tag_polyTime).space (q, v) +
             if decide (v.1 = 0) = true then
@@ -587,7 +590,8 @@ theorem fastCertificate_le (hpoly : (scheme mk).PolyTime encCall encFrame encVal
             else (NativeCertificate.ofPolyTime
                 (ComputableInPolyTime.fst FastContraction.encInput encValue)).space (q, v) +
               ExplicitTensorNetwork.directContractionBinaryCertificate.space q) ≤ R₁ + R₂ := by
-      rcases hr : (scheme mk).run fuel root (ExplicitTensorNetwork.capPrecision q) with _ | v
+      rcases hr : (scheme tableEntry mk).run fuel root
+        (ExplicitTensorNetwork.capPrecision q) with _ | v
       · simp only [Option.elim_none]; omega
       · have hd := hdec v (Scheme.value_of_run_eq_some he hr)
         simp only [Option.elim_some]
@@ -609,8 +613,9 @@ call and the passage of well-formedness to the children (`FastContraction.StepCo
 (`FastAnalysis`). It branches on the guard (`ContractionAlgorithm.ofGuarded`) to the fast machine
 or to direct summation. -/
 noncomputable def contractionAlgorithmOfFast
-    (hpoly : (scheme mk).PolyTime encCall encFrame encValue) {WF : Call → Prop}
-    (hstep : StepCorrect mk WF) (hwf : WFChildren mk WF)
+    (hpoly : (scheme tableEntry mk).PolyTime (encCall (encList encNat)) encFrame encValue)
+    {WF : Call (List ℕ) → Prop}
+    (hstep : StepCorrect tableEntry mk WF) (hwf : WFChildren mk WF)
     (hroot : ∀ P G, fastGuard G = true → WF (root (ExplicitTensorNetwork.capPrecision (P, G))))
     (hana : FastAnalysis mk) :
     ContractionAlgorithm (encPair encNat ExplicitTensorNetwork.encExplicitNetwork)
@@ -645,7 +650,8 @@ children and the well-formed roots are proved (`FastContraction.stepCorrect_nati
 noncomputable def contractionAlgorithmOfNative (hana : FastAnalysis nativeMk) :
     ContractionAlgorithm (encPair encNat ExplicitTensorNetwork.encExplicitNetwork)
       (fun G => G.2.contraction) ExplicitAdmissible :=
-  contractionAlgorithmOfFast scheme_nativeMk_polyTime stepCorrect_nativeMk wfChildren_nativeMk
+  contractionAlgorithmOfFast (scheme_nativeMk_polyTime tableEntry)
+    (stepCorrect_nativeMk tableEntry) wfChildren_nativeMk
     (fun P _ hg => wf_root P hg) hana
 
 end Resources
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean
index 9e69bf87b..ff5135680 100644
--- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean
@@ -179,11 +179,12 @@ such that on every guarded input admissible at size `s ≥ 2` with constant `C`
   ∀ C D : ℕ, ∃ c d : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → 1 ≤ P →
     P ≤ D * s → ExplicitAdmissible C s G → fastGuard G = true →
     ∀ x, Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x →
-      (encCall x).length ≤ c * ((FastContraction.encInput (P, G)).length + 1) ^ d ∧
-      (∀ a, (reachInv nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G)))).frame x a →
-        (encPair encCall encFrame (x, a)).length ≤
+      (encCall (encList encNat) x).length ≤ c * ((FastContraction.encInput (P, G)).length + 1) ^ d ∧
+      (∀ a, (reachInv tableEntry nativeMk
+          (root (ExplicitTensorNetwork.capPrecision (P, G)))).frame x a →
+        (encPair (encCall (encList encNat)) encFrame (x, a)).length ≤
           c * ((FastContraction.encInput (P, G)).length + 1) ^ d) ∧
-      (encValue (x.depth, value nativeMk x)).length ≤
+      (encValue (x.depth, value tableEntry nativeMk x)).length ≤
         c * ((FastContraction.encInput (P, G)).length + 1) ^ d
 
 /-- **The leaf bounds**: for all constants `C` and `D` there is `K` such that on every guarded
@@ -223,8 +224,9 @@ theorem fastAnalysis_nativeMk_of (hS : FastSizes) (hL : FastLeaves) : FastAnalys
   have hp₀ : q.1 ≤ D * m :=
     (min_le_right _ _).trans (hPD.trans (Nat.mul_le_mul_left _ hsm))
   -- The derivation.
-  obtain ⟨N, H, he, hN, hH⟩ : ∃ N H, (scheme nativeMk).Eval (reachInv nativeMk x₀) x₀
-      (0, value nativeMk x₀) N H ∧ (max sA (D + 2) ≤ s → 2 * N - 1 ≤ fuel q) ∧ H ≤ m + 1 := by
+  obtain ⟨N, H, he, hN, hH⟩ : ∃ N H, (scheme tableEntry nativeMk).Eval
+      (reachInv tableEntry nativeMk x₀) x₀ (0, value tableEntry nativeMk x₀) N H ∧
+        (max sA (D + 2) ≤ s → 2 * N - 1 ≤ fuel q) ∧ H ≤ m + 1 := by
     by_cases hs₀ : max sA (D + 2) ≤ s
     · have hm2 : D + 2 ≤ m := by omega
       have hC1 : q.1 / m + 1 ≤ D + 1 := by
@@ -234,7 +236,7 @@ theorem fastAnalysis_nativeMk_of (hS : FastSizes) (hL : FastLeaves) : FastAnalys
       have hB := hsA m (by omega) (q.1 / m + 1) hC1
       have hpC : q.1 ≤ (q.1 / m + 1) * m :=
         (Nat.lt_div_mul_add (a := q.1) (b := m) (by omega)).le.trans (by rw [add_mul, one_mul])
-      obtain ⟨N, H, he, hN, hH⟩ := exists_eval_onSchedule hB
+      obtain ⟨N, H, he, hN, hH⟩ := exists_eval_onSchedule tableEntry hB
         (onSchedule_root_capPrecision hg (Nat.le_add_left 1 _) hpC) rfl (by omega)
       refine ⟨N, H, he, fun _ => ?_, hH.trans ((Nat.log_lt_self 2 (by omega)).le.trans
         (Nat.le_succ _))⟩
@@ -246,8 +248,9 @@ theorem fastAnalysis_nativeMk_of (hS : FastSizes) (hL : FastLeaves) : FastAnalys
   obtain hKL' := hKL s P G hs hP hPD hA hg
   set K := cS + dS + KL + 1
   have hB1 : 1 ≤ n + 1 := by omega
-  refine ⟨reachInv nativeMk x₀, N, H, cS * (n + 1) ^ dS, KL * (n + 1) ^ KL * 2 ^ (KL * s /
-    Nat.sqrt (Nat.log 2 s)), KL * (n + 1) ^ KL, he, hN, fun x hx => ⟨(hKS' x hx).1, fun hl => ?_⟩,
+  refine ⟨reachInv tableEntry nativeMk x₀, N, H, cS * (n + 1) ^ dS,
+    KL * (n + 1) ^ KL * 2 ^ (KL * s / Nat.sqrt (Nat.log 2 s)), KL * (n + 1) ^ KL, he, hN,
+    fun x hx => ⟨(hKS' x hx).1, fun hl => ?_⟩,
     fun x a ha => (hKS' x ha.1).2.1 a ha, fun v ⟨x, hx, hv⟩ => hv ▸ (hKS' x hx).2.2, ?_, ?_⟩
   · have hl' : active x = false := by simpa [scheme] using hl
     exact hKL' x hx hl'
@@ -371,7 +374,8 @@ theorem fastSizes : FastSizes := by
     have : (x₀.edges + 1) * x₀.edges ^ 2 ≤ Y * Y ^ 2 := Nat.mul_le_mul hmY hm2
     have : Y * Y ^ 2 = Y ^ 3 := by ring
     omega
-  have hR₀ : ∀ w ∈ x₀.net.vertices, (VertexDesc.enc w.2).length ≤ 200 * (Z + 1) ^ 2 := by
+  have hR₀ : ∀ w ∈ x₀.net.vertices,
+      (VertexDesc.enc (encList encNat) w.2).length ≤ 200 * (Z + 1) ^ 2 := by
     intro w hw
     change w ∈ List.map _ G.2.vertices at hw
     obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hw
@@ -380,7 +384,7 @@ theorem fastSizes : FastSizes := by
     have := hdesc v hv
     have : Z ≤ (Z + 1) ^ 2 := (Nat.le_succ Z).trans (Nat.le_self_pow (by norm_num) _)
     omega
-  obtain ⟨hc, hv, hf⟩ := hsh.length_le rfl rfl rfl hZ1 hZ2
+  obtain ⟨hc, hv, hf⟩ := hsh.length_le tableEntry rfl rfl rfl hZ1 hZ2
     (fun z hz => le_one_of_mem_modulus hz) hR₀
   -- `1000 (Z + 1) ^ 3 ≤ 2 ^ 55 (n + 1) ^ 24`.
   have hfin : 1000 * (Z + 1) ^ 3 ≤ 2 ^ 55 * Y ^ 24 := by
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean
index 805a16171..447d80216 100644
--- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastLeaves.lean
@@ -51,7 +51,7 @@ namespace Cslib.Circuits.Frontier.FastContraction
 
 /-- **The reached calls are well-formed and have the packet shape**, from a well-formed root with
 the packet shape. -/
-theorem Reach.wf_packetShape {x₀ x : Call} (h : Reach nativeMk x₀ x) (hw : WF x₀)
+theorem Reach.wf_packetShape {x₀ x : Call (List ℕ)} (h : Reach nativeMk x₀ x) (hw : WF x₀)
     (hs : PacketShape x₀) : WF x ∧ PacketShape x := by
   induction h with
   | root => exact ⟨hw, hs⟩
@@ -61,7 +61,7 @@ theorem Reach.wf_packetShape {x₀ x : Call} (h : Reach nativeMk x₀ x) (hw : W
 /-- **Reached calls have at most twice the scale in edges**, from a root at scale its number of
 edges with bound plus depth one more, for every input: a child has at most twice its parent's
 edges (`NativeChild.numEdges_nativeChild_le`), and an active parent has at most the root's. -/
-theorem Reach.edges_le_two_mul_scale {x₀ x : Call} (h₀s : x₀.scale = x₀.edges)
+theorem Reach.edges_le_two_mul_scale {x₀ x : Call (List ℕ)} (h₀s : x₀.scale = x₀.edges)
     (h₀b : x₀.bound + x₀.depth = x₀.edges + 1) (h : Reach nativeMk x₀ x) :
     x.edges ≤ 2 * x.scale := by
   have key : x.edges ≤ 2 * x₀.edges := by
@@ -84,13 +84,14 @@ namespace Cslib.Complexity.CountingSimulation
 
 open Cslib.Circuits.Frontier Cslib.Circuits.Frontier.ContractionSchedule
   Cslib.Circuits.Frontier.FastContraction
+open Turing.MultiTapeTM (encList encNat)
 
 /-- **The leaf bounds of the native recursion**, from the sizes of the reached calls and three
 facts about them on admissible guarded inputs: every reached call has at most twice its scale in
 edges, and for each `C` and `D`, from some size on, every reached leaf has at most the leaf size in
 edges and precision at most the fourth power of its scale. -/
 theorem fastLeaves_of (hS : FastSizes)
-    (hE : ∀ (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) (x : Call),
+    (hE : ∀ (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) (x : Call (List ℕ)),
       Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x →
         x.edges ≤ 2 * x.scale)
     (hbig : ∀ C D : ℕ, ∃ s₀ : ℕ, ∀ (s P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ), 2 ≤ s → 1 ≤ P →
@@ -113,15 +114,16 @@ theorem fastLeaves_of (hS : FastSizes)
     fun h => hs₀ s P G hs hP hPD hA hg h x hx hl
   have hlen' := (hKS s P G hs hP hPD hA hg x hx).1
   rw [← hn] at hlen'
-  have hlen : (encCall x).length ≤ KS * (n + 1) ^ KS :=
+  have hlen : (encCall (encList encNat) x).length ≤ KS * (n + 1) ^ KS :=
     hlen'.trans (Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega)))
   -- `n_x + 1 ≤ (KS + 1) (n + 1) ^ KS`.
   have hB1 : 1 ≤ (n + 1) ^ KS := Nat.one_le_pow _ _ (by omega)
-  have hx1 : (encCall x).length + 1 ≤ (KS + 1) * (n + 1) ^ KS := by
+  have hx1 : (encCall (encList encNat) x).length + 1 ≤ (KS + 1) * (n + 1) ^ KS := by
     rw [add_mul, one_mul]; omega
   set K := KB * (KS + 1) ^ KB + KS * KB + KB
-  have hpoly : KB * ((encCall x).length + 1) ^ KB ≤ K * (n + 1) ^ K :=
-    calc KB * ((encCall x).length + 1) ^ KB ≤ KB * ((KS + 1) * (n + 1) ^ KS) ^ KB :=
+  have hpoly : KB * ((encCall (encList encNat) x).length + 1) ^ KB ≤ K * (n + 1) ^ K :=
+    calc KB * ((encCall (encList encNat) x).length + 1) ^ KB
+        ≤ KB * ((KS + 1) * (n + 1) ^ KS) ^ KB :=
           Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hx1 _)
       _ = KB * (KS + 1) ^ KB * (n + 1) ^ (KS * KB) := by rw [mul_pow, ← pow_mul]; ring
       _ ≤ K * (n + 1) ^ K :=
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChild.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChild.lean
index 1431e819e..deb70c052 100644
--- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChild.lean
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChild.lean
@@ -20,10 +20,10 @@ The row `0` joins the columns `1` and `2` by the edges `0` and `1`, and the vert
 The network is rows-first at `1`, and the ends of its edges are computed from the ports. -/
 
 /-- The tables of the vertices. -/
-def table (n : ℕ) : VertexDesc := .inl (List.replicate n 1)
+def table (n : ℕ) : VertexDesc (List ℕ) := .inl (List.replicate n 1)
 
 /-- The row `0` with ports `1, 0` (not in edge order), the columns `1` and `2`. -/
-def path : DescribedNetwork VertexDesc :=
+def path : DescribedNetwork (VertexDesc (List ℕ)) :=
   ⟨2, [([1, 0], table 4), ([0], table 2), ([1], table 2)]⟩
 
 example : path.IsRowsFirstBipartite 1 := by decide
@@ -34,7 +34,7 @@ example : path.edgeEnds = [(0, 1), (0, 2)] := by decide
 
 /-- The native child of group `0` for a packing that puts the row and the column `1` in group `0`,
 the column `2` in group `1`, and both edges in packet `0` with slots `0` and `1`. -/
-def child : DescribedNetwork VertexDesc :=
+def child : DescribedNetwork (VertexDesc (List ℕ)) :=
   nativeChild [1] 1 0 3 (-1) [0] 1 path (([[0]], [[0], [1]]), 1, [(0, 0), (0, 1)]) [] 0
 
 /-- The child keeps the row and the column `1`, and adds the packet: three child edges, the two
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChildPolyTime.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChildPolyTime.lean
index 5a4e66be6..3c9ba93ca 100644
--- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChildPolyTime.lean
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkNativeChildPolyTime.lean
@@ -33,10 +33,10 @@ The path of `TensorNetworkNativeChild` with one row joined to two columns. The c
 keeps the row and the column `1` and adds one packet. -/
 
 /-- The tables of the vertices. -/
-def table (n : ℕ) : VertexDesc := .inl (List.replicate n 1)
+def table (n : ℕ) : VertexDesc (List ℕ) := .inl (List.replicate n 1)
 
 /-- The row `0` with ports `1, 0`, the columns `1` and `2`. -/
-def path : DescribedNetwork VertexDesc :=
+def path : DescribedNetwork (VertexDesc (List ℕ)) :=
   ⟨2, [([1, 0], table 4), ([0], table 2), ([1], table 2)]⟩
 
 /-- The packing: the row and the column `1` in group `0`, the column `2` in group `1`, both edges
@@ -58,17 +58,17 @@ and its number of packets in unary, with the other parameters fixed. -/
 
 /-- A parent, the packing words, the number of packets and the placements. -/
 abbrev Input : Type :=
-  DescribedNetwork VertexDesc × (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)
+  DescribedNetwork (VertexDesc (List ℕ)) × (List (List ℕ) × List (List ℕ)) × ℕ × List (ℕ × ℕ)
 
 /-- The encoding of `Input`, with the number of packets in unary. -/
 abbrev encInput : Input ↪ List Bool :=
-  encPair (DescribedNetwork.encDescribed VertexDesc.enc)
+  encPair (DescribedNetwork.encDescribed (VertexDesc.enc (encList encNat)))
     (encPair (encPair (encList (encList encNat)) (encList (encList encNat)))
       (encPair encUnary (encList (encPair encNat encNat))))
 
 example : ComputableInPolyTime (fun x : Input =>
     nativeChild [1] 1 0 3 (-1) [0] 1 x.1 x.2 [] 0) encInput
-    (DescribedNetwork.encDescribed VertexDesc.enc) := by
+    (DescribedNetwork.encDescribed (VertexDesc.enc (encList encNat))) := by
   have hpk : ComputableInPolyTime (fun x : Input => x.2) encInput
       PacketPacking.encNativePacking :=
     ((ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _)).prod
@@ -85,10 +85,10 @@ example : ComputableInPolyTime (fun x : Input =>
     (ComputableInPolyTime.const _) (ComputableInPolyTime.const _)
 
 /-- With the native parent packing, the number of rows and `a` are the only further inputs. -/
-example : ComputableInPolyTime (fun D : DescribedNetwork VertexDesc =>
+example : ComputableInPolyTime (fun D : DescribedNetwork (VertexDesc (List ℕ)) =>
     nativeChild [1] 1 0 3 (-1) [0] 1 D (nativeParentPacking 1 1 D) [] 0)
-    (DescribedNetwork.encDescribed VertexDesc.enc)
-    (DescribedNetwork.encDescribed VertexDesc.enc) :=
+    (DescribedNetwork.encDescribed (VertexDesc.enc (encList encNat)))
+    (DescribedNetwork.encDescribed (VertexDesc.enc (encList encNat))) :=
   computableInPolyTime_nativeChild_nativeParentPacking (ComputableInPolyTime.const _)
     (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) (ComputableInPolyTime.const _)
     (ComputableInPolyTime.const _) (ComputableInPolyTime.const _) (ComputableInPolyTime.const _)
diff --git a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkVertexDesc.lean b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkVertexDesc.lean
index e3be36554..e84885bb7 100644
--- a/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkVertexDesc.lean
+++ b/ComplexityTests/Computability/Circuit/Frontier/TensorNetworkVertexDesc.lean
@@ -27,13 +27,14 @@ list come out in order. Reducing an element of `O` to `A_n` and mapping back alo
 namespace ComplexityTests.TensorNetworkVertexDesc
 
 open Cslib Cslib.Circuits.Frontier Cslib.Circuits.Frontier.NativePacket
+open Turing.MultiTapeTM (encList encNat)
 
 /-! ### Tables -/
 
 -- The bits `[true, false]` index the table at `1`.
-example : VertexDesc.entry (.inl [3, 5, 7, 9]) [true, false] = [5] := by decide
+example : VertexDesc.entry tableEntry (.inl [3, 5, 7, 9]) [true, false] = [5] := by decide
 
-example : VertexDesc.entry (.inl [3, 5, 7, 9]) [false, true] = [7] := by decide
+example : VertexDesc.entry tableEntry (.inl [3, 5, 7, 9]) [false, true] = [7] := by decide
 
 -- A table has no modes and no row ports.
 example : VertexDesc.modes (.inl [3, 5]) = 0 := rfl
@@ -41,7 +42,7 @@ example : VertexDesc.modes (.inl [3, 5]) = 0 := rfl
 example : VertexDesc.rowPorts (.inl [3, 5]) [true] = 0 := rfl
 
 -- A table entry is a constant in `A_p`.
-example : GaloisRingArith.val 3 [1, 1] (VertexDesc.entry (.inl [3, 5]) [true]) =
+example : GaloisRingArith.val 3 [1, 1] (VertexDesc.entry tableEntry (.inl [3, 5]) [true]) =
     ((5 : ℕ) : GaloisRingArith.Ring 3 [1, 1]) :=
   VertexDesc.val_entry_inl 3 [1, 1] [3, 5] [true]
 
@@ -52,13 +53,23 @@ def ctx : PacketCtx :=
   ⟨3, [1, 1], 1, 2, 0, 2, 1, 2, true, false, true, [], [0, 1]⟩
 
 /-- The descriptor: a row port in slot `0` and a column port in slot `1`, zero exponents. -/
-def desc : VertexDesc := .inr (ctx, [(true, 0), (false, 1)], [0, 0, 0, 0])
+def desc : VertexDesc (List ℕ) := .inr (ctx, [(true, 0), (false, 1)], [0, 0, 0, 0])
 
 -- The column ports are read from the tags and the bits: the entry is `W_1(T) = 5 + 2 U`.
-example : VertexDesc.entry desc [true, true] = [5, 2] := by decide
+example : VertexDesc.entry tableEntry desc [true, true] = [5, 2] := by decide
 
 example : VertexDesc.rowPorts desc [true, true] = 1 := by decide
 
+/-! ### Other root descriptors -/
+
+-- A root descriptor of any type is read by its entry procedure, here a number read as the
+-- coefficient list `[n, 1]`.
+example : VertexDesc.entry (fun (n : ℕ) _ => [n, 1]) (.inl 7) [true] = [7, 1] := rfl
+
+-- A packet descriptor reads the same entry whatever the type of the root descriptors.
+example : VertexDesc.entry (fun (n : ℕ) _ => [n])
+    (.inr (ctx, [(true, 0), (false, 1)], [0, 0, 0, 0])) [true, true] = [5, 2] := by decide
+
 /-! ### Tagged ports -/
 
 example : sidePorts [(true, 3), (false, 1), (true, 2)] [true, false, false] true =
@@ -75,12 +86,14 @@ example : sidePorts ([4, 1, 2].map fun c => (decide (c % 2 = 0), c)) ([4, 1, 2].
 
 /-! ### Resources -/
 
-example : ∃ K : ℕ, ∀ (q : VertexDesc × List Bool) (Rv : ℕ), q.1.ReducedLE Rv →
+example : ∃ K : ℕ, ∀ (q : VertexDesc (List ℕ) × List Bool) (Rv : ℕ), q.1.ReducedLE Rv →
     VertexDesc.entryCertificate.time q ≤ K * (q.1.modes + 2) ^ q.1.rowPorts q.2 *
-        ((Turing.MultiTapeTM.encPair VertexDesc.enc Turing.MultiTapeTM.encBits q).length +
+        ((Turing.MultiTapeTM.encPair (VertexDesc.enc (encList encNat)) Turing.MultiTapeTM.encBits
+          q).length +
           q.1.modes + Rv + 2) ^ K ∧
       VertexDesc.entryCertificate.space q ≤
-        K * ((Turing.MultiTapeTM.encPair VertexDesc.enc Turing.MultiTapeTM.encBits q).length +
+        K * ((Turing.MultiTapeTM.encPair (VertexDesc.enc (encList encNat))
+          Turing.MultiTapeTM.encBits q).length +
           q.1.modes + Rv + 2) ^ K :=
   VertexDesc.entryCertificate_le
 
diff --git a/ComplexityTests/FastContractionAnalysis.lean b/ComplexityTests/FastContractionAnalysis.lean
index 29eb99127..10ad24c52 100644
--- a/ComplexityTests/FastContractionAnalysis.lean
+++ b/ComplexityTests/FastContractionAnalysis.lean
@@ -22,11 +22,11 @@ def tiny : ℕ × ExplicitTensorNetwork ℕ := (1, ⟨1, [([0], [1, 2]), ([0], [
 example : fastGuard tiny = true := by decide
 
 /-- The root of `tiny` at precision `3`. -/
-abbrev tinyRoot : Call := root (ExplicitTensorNetwork.capPrecision (3, tiny))
+abbrev tinyRoot : Call (List ℕ) := root (ExplicitTensorNetwork.capPrecision (3, tiny))
 
 -- The root is reached, and it is the only reached call at depth `0`.
 example : Reach nativeMk tinyRoot tinyRoot := .root
-example (x : Call) (hx : Reach nativeMk tinyRoot x) (h0 : x.depth = 0) : x = tinyRoot :=
+example (x : Call (List ℕ)) (hx : Reach nativeMk tinyRoot x) (h0 : x.depth = 0) : x = tinyRoot :=
   hx.eq_root_of_depth_le (by rw [h0]; rfl)
 
 -- The root is a leaf, so its derivation has one node and no open call.
@@ -41,8 +41,8 @@ example : OnSchedule 3 tiny.2.numEdges tinyRoot :=
   onSchedule_root_capPrecision (by decide) (by norm_num) (by decide)
 
 -- Values are reduced at their precision: at most `e` coordinates below `2 ^ p`.
-example : ReducedAt tinyRoot.prec tinyRoot.fl (value nativeMk tinyRoot) :=
-  reducedAt_value nativeMk tinyRoot
+example : ReducedAt tinyRoot.prec tinyRoot.fl (value tableEntry nativeMk tinyRoot) :=
+  reducedAt_value tableEntry nativeMk tinyRoot
 
 -- The modulus at `m = 1` has `2 ⬝ 3 ^ 1 = 6` coefficients, within `32 (m + 1) ^ 2`.
 example : (modulus 1).length = 6 := by decide
@@ -55,7 +55,7 @@ example (N : ℕ) (hN : N ≤ 2 ^ ((245760 * (50 / 100 + 1) + 37) * 100 / Nat.sq
   two_mul_sub_one_le_fuel (D := 1) (by norm_num) (by norm_num) hN
 
 -- A child of a parent with `M` edges under (D.6) has at most `M / 16` edges.
-example {r a i Δ : ℕ} {D : DescribedNetwork VertexDesc} (hD : D.IsRowsFirstBipartite r)
+example {r a i Δ : ℕ} {D : DescribedNetwork (VertexDesc (List ℕ))} (hD : D.IsRowsFirstBipartite r)
     (hK : 64 ^ a ≤ D.numEdges) (hia : i < a) (hdeg : ∀ v ∈ D.vertices, v.1.length ≤ Δ)
     (hM : 2 * Δ * (64 ^ (2 * a)) ^ 2 ≤ D.numEdges) (fl : List ℕ) (pt : ℕ) (t : ℤ)
     (ζ β : List ℕ) (g : Fin 64) :
diff --git a/ComplexityTests/FastContractionLeaf.lean b/ComplexityTests/FastContractionLeaf.lean
index 5a2370278..dea272a33 100644
--- a/ComplexityTests/FastContractionLeaf.lean
+++ b/ComplexityTests/FastContractionLeaf.lean
@@ -53,10 +53,11 @@ def ctx : PacketCtx where
   ζ := [0]
 
 /-- A packet vertex with a row port in slot `0` and a column port in slot `1`. -/
-def packetVertex : List ℕ × VertexDesc := ([0, 1], .inr (ctx, [(true, 0), (false, 1)], [0, 0]))
+def packetVertex : List ℕ × VertexDesc (List ℕ) :=
+  ([0, 1], .inr (ctx, [(true, 0), (false, 1)], [0, 0]))
 
 /-- A call at scale `4` and precision `1` whose network is the packet vertex alone. -/
-def packetCall : Call := ((4, 1, 3, 1, [1], 0), ⟨2, [packetVertex]⟩)
+def packetCall : Call (List ℕ) := ((4, 1, 3, 1, [1], 0), ⟨2, [packetVertex]⟩)
 
 -- The packet vertex has one row port, and at most `2 ⬝ 1` target modes.
 example : packetVertex.2.rowPorts [true, false] = 1 := by decide
diff --git a/ComplexityTests/FastContractionPolyTime.lean b/ComplexityTests/FastContractionPolyTime.lean
index 2b8c3ca97..b266ee102 100644
--- a/ComplexityTests/FastContractionPolyTime.lean
+++ b/ComplexityTests/FastContractionPolyTime.lean
@@ -32,15 +32,18 @@ example : (packing (root (3, 1, tiny))).2.1 ≤
   NativeChild.numPackets_nativeParentPacking_le _ _ _
 
 -- On every call, `2 ^ a ≤ s + 1`, and the levels are at most `a + 1`.
-example (x : Call) : 2 ^ slots x ≤ x.scale + 1 := two_pow_slots_le x
-example (x : Call) (k : ℕ) : level x k ≤ slots x + 1 := level_le x k
+example {T : Type} (x : Call T) : 2 ^ slots x ≤ x.scale + 1 := two_pow_slots_le x
+example {T : Type} (x : Call T) (k : ℕ) : level x k ≤ slots x + 1 := level_le x k
 
 -- The cap on the exponents leaves the tuples of weight below the budget unchanged.
 example : ([1, 0, 1] : List ℕ).map (min · 3) = [1, 0, 1] :=
   map_min_of_mem_budgetTuples (ws := [1, 1, 1]) (by decide) (by decide)
 
--- The components of the scheme of the native child builder are polynomial-time.
-example : (scheme nativeMk).PolyTime encCall encFrame encValue := scheme_nativeMk_polyTime
+-- The components of the scheme of the native child builder are polynomial-time, for every type
+-- of root descriptors and every entry procedure.
+example {T : Type} (encT : T ↪ List Bool) (ev : T → List Bool → List ℕ) :
+    (scheme ev (nativeMk (T := T))).PolyTime (encCall encT) encFrame encValue :=
+  scheme_nativeMk_polyTime ev
 
 -- The contraction interface for admissible explicit networks, from the resource analysis alone.
 noncomputable example (hana : FastAnalysis nativeMk) :
diff --git a/ComplexityTests/FastLeaves.lean b/ComplexityTests/FastLeaves.lean
index 2e205e997..e241e2c01 100644
--- a/ComplexityTests/FastLeaves.lean
+++ b/ComplexityTests/FastLeaves.lean
@@ -28,7 +28,7 @@ example : WF (root (ExplicitTensorNetwork.capPrecision (1, pair))) ∧
   (Reach.root (mk := nativeMk)).wf_packetShape (wf_root 1 (by decide)) (packetShape_root _)
 
 -- Reached calls have at most twice the scale in edges, on every input.
-example (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) (x : Call)
+example (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) (x : Call (List ℕ))
     (hx : Reach nativeMk (root (ExplicitTensorNetwork.capPrecision (P, G))) x) :
     x.edges ≤ 2 * x.scale :=
   hx.edges_le_two_mul_scale rfl rfl