From bec86df635d23f6115092f6361dcf310ac27c1d3 Mon Sep 17 00:00:00 2001
From: chris-ai1 <chris-ai1@catch.exinto.de>
Date: Sun, 1 Nov 2026 23:11:59 +0000
Subject: [PATCH] refactor(Encodings): generate structure encodings with
 enc_structure

Bring `enc_structure` and its tests over from #2184, and migrate hand-written
structure encodings to it, removing the rules it generates.

The command also generates polynomial-time rules, accepts parameters and
binders, supports `noncomputable` and `global`, and no longer marks `_apply`
as `simp`, because the migrated clients need these.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Complexity.lean                               |   1 +
 .../Classes/Space/TQBF/Membership.lean        | 105 +--------
 .../GenericRAM/Simulation/Turing.lean         |  22 +-
 .../Computability/Kolmogorov/MINKT.lean       |  12 +-
 .../LogSpace/InductiveCounting/Machine.lean   |  13 +-
 .../Complexity/Space/Reachability.lean        |  36 +--
 .../Turing/MultiTape/Encodings/Structure.lean | 206 ++++++++++++++++++
 .../ExplicitBlockNetwork/TablePolyTime.lean   |   2 +-
 .../Probabilistic/IntervalCount/PolyTime.lean | 168 ++++----------
 .../Approximation/LabelCover/Incidence.lean   |  14 +-
 .../PCP/Approximation/MaxThreeSAT.lean        |   2 +-
 .../Computability/PCP/Encoded/AddTrivial.lean |   8 +-
 .../Computability/PCP/Encoded/Basic.lean      |  89 +-------
 .../Computability/PCP/Encoded/Cloud.lean      |   4 +-
 .../PCP/Encoded/GenericComposition.lean       |  10 +-
 .../Computability/PCP/Encoded/Power.lean      |   4 +-
 .../Computability/PCP/Encoded/ThreeSAT.lean   |   2 +-
 .../PCP/Encoded/Verifier/Repetition.lean      |   2 +-
 .../Computational/Hybrid/SavedPrediction.lean |  27 +--
 .../Pseudoentropy/Boosting/Program.lean       | 144 +-----------
 ComplexityTests/HPVIntervalCount.lean         |   2 +-
 ComplexityTests/StructureEncoding.lean        | 120 ++++++++++
 22 files changed, 462 insertions(+), 531 deletions(-)
 create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Encodings/Structure.lean
 create mode 100644 ComplexityTests/StructureEncoding.lean

diff --git a/Complexity.lean b/Complexity.lean
index 1062ce1794..84c833ae4a 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2029,6 +2029,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pi
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StepMachine
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StepMachineComp
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StreamFold
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Sum
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Tape
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary
diff --git a/Complexity/Computability/Complexity/Classes/Space/TQBF/Membership.lean b/Complexity/Computability/Complexity/Classes/Space/TQBF/Membership.lean
index 04ce31f636..261868ebd6 100644
--- a/Complexity/Computability/Complexity/Classes/Space/TQBF/Membership.lean
+++ b/Complexity/Computability/Complexity/Classes/Space/TQBF/Membership.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.Space
 public import Complexity.Computability.Complexity.Classes.Space.TQBF.Evaluation
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration
 import Complexity.Computability.Machines.Turing.MultiTape.Combinators.IterateWhile
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
@@ -66,35 +67,13 @@ open Cslib.Logic.PL Turing.MultiTapeTM
 
 /-! ### Encodings -/
 
-/-- The fields of a frame. -/
-def Frame.fields (f : Frame) : (QBF.Kind × ℕ) × Option Bool × List (QBF.Kind × ℕ) :=
-  (f.token, f.first, f.rest)
-
-/-- The encoding of the fields of a frame. -/
-abbrev encFrameFields : (QBF.Kind × ℕ) × Option Bool × List (QBF.Kind × ℕ) ↪ List Bool :=
-  encPair encToken (encPair (encOption encBool) (encList encToken))
-
 /-- Frames encoded by their fields. -/
-def encFrame : Frame ↪ List Bool :=
-  ⟨fun f => encFrameFields f.fields, fun f g h => by
-    obtain ⟨⟩ := f
-    obtain ⟨⟩ := g
-    simpa [Frame.fields] using encFrameFields.injective h⟩
-
-/-- The fields of a state. -/
-def State.fields (s : State) : List (QBF.Kind × ℕ) × List Frame × Option Bool × Bool :=
-  (s.input, s.stack, s.value, s.ok)
-
-/-- The encoding of the fields of a state. -/
-abbrev encStateFields : List (QBF.Kind × ℕ) × List Frame × Option Bool × Bool ↪ List Bool :=
-  encPair (encList encToken) (encPair (encList encFrame) (encPair (encOption encBool) encBool))
+enc_structure encFrame : Frame where
+  token : encToken, first : (encOption encBool), rest : (encList encToken)
 
 /-- States encoded by their fields. -/
-def encState : State ↪ List Bool :=
-  ⟨fun s => encStateFields s.fields, fun s t h => by
-    obtain ⟨⟩ := s
-    obtain ⟨⟩ := t
-    simpa [State.fields] using encStateFields.injective h⟩
+enc_structure encState : State where
+  input : (encList encToken), stack : (encList encFrame), value : (encOption encBool), ok : encBool
 
 /-! ### The step in polynomial time -/
 
@@ -102,67 +81,6 @@ section Step
 
 open ComputableInPolyTime
 
-/-- The fields of a state, the identity on encoded values. -/
-@[local fun_prop] private lemma fields_pt :
-    ComputableInPolyTime State.fields encState encStateFields :=
-  of_eq fun _ => rfl
-
-/-- A state from its fields, the identity on encoded values. -/
-@[local fun_prop] private lemma stateMk_pt :
-    ComputableInPolyTime
-      (fun p : List (QBF.Kind × ℕ) × List Frame × Option Bool × Bool =>
-        State.mk p.1 p.2.1 p.2.2.1 p.2.2.2) encStateFields encState :=
-  of_eq fun _ => rfl
-
-/-- The fields of a frame, the identity on encoded values. -/
-@[local fun_prop] private lemma frameFields_pt :
-    ComputableInPolyTime Frame.fields encFrame encFrameFields :=
-  of_eq fun _ => rfl
-
-/-- A frame from its fields, the identity on encoded values. -/
-@[local fun_prop] private lemma frameMk_pt :
-    ComputableInPolyTime
-      (fun p : (QBF.Kind × ℕ) × Option Bool × List (QBF.Kind × ℕ) => Frame.mk p.1 p.2.1 p.2.2)
-      encFrameFields encFrame :=
-  of_eq fun _ => rfl
-
-@[local fun_prop] private lemma stateMk_comp_pt {α : Type} {encIn : α ↪ List Bool}
-    {f₁ : α → List (QBF.Kind × ℕ)} {f₂ : α → List Frame}
-    {f₃ : α → Option Bool} {f₄ : α → Bool}
-    (h₁ : ComputableInPolyTime f₁ encIn (encList encToken))
-    (h₂ : ComputableInPolyTime f₂ encIn (encList encFrame))
-    (h₃ : ComputableInPolyTime f₃ encIn (encOption encBool))
-    (h₄ : ComputableInPolyTime f₄ encIn encBool) :
-    ComputableInPolyTime (fun a => State.mk (f₁ a) (f₂ a) (f₃ a) (f₄ a)) encIn encState :=
-  stateMk_pt.comp (h₁.prod (h₂.prod (h₃.prod h₄)))
-
-@[local fun_prop] private lemma input_pt :
-    ComputableInPolyTime State.input encState (encList encToken) :=
-  (fst _ _).comp fields_pt
-
-@[local fun_prop] private lemma stack_pt :
-    ComputableInPolyTime State.stack encState (encList encFrame) :=
-  ((fst _ _).comp (snd _ _)).comp fields_pt
-
-@[local fun_prop] private lemma value_pt :
-    ComputableInPolyTime State.value encState (encOption encBool) :=
-  ((fst _ _).comp ((snd _ _).comp (snd _ _))).comp fields_pt
-
-@[local fun_prop] private lemma ok_pt : ComputableInPolyTime State.ok encState encBool :=
-  ((snd _ _).comp ((snd _ _).comp (snd _ _))).comp fields_pt
-
-@[local fun_prop] private lemma token_pt :
-    ComputableInPolyTime Frame.token encFrame encToken :=
-  (fst _ _).comp frameFields_pt
-
-@[local fun_prop] private lemma first_pt :
-    ComputableInPolyTime Frame.first encFrame (encOption encBool) :=
-  ((fst _ _).comp (snd _ _)).comp frameFields_pt
-
-@[local fun_prop] private lemma rest_pt :
-    ComputableInPolyTime Frame.rest encFrame (encList encToken) :=
-  ((snd _ _).comp (snd _ _)).comp frameFields_pt
-
 /-- The next token, or `(top, 0)` when the input is empty. -/
 private def State.head (s : State) : QBF.Kind × ℕ := s.input.headD (.top, 0)
 
@@ -251,7 +169,7 @@ private theorem assignment_eq (stack : List Frame) (v : ℕ) :
   have h : ComputableInPolyTime (fun p : State × Frame => Frame.binds p.1.head.2 p.2)
       (encPair encState encFrame) encBool :=
     binds_pt.comp (g := fun p : State × Frame => (p.1.head.2, p.2)) (by fun_prop)
-  exact optionIsSome (findWithInput stack_pt h)
+  exact optionIsSome (findWithInput (encState_stack_polyTime id') h)
 
 /-- The value of the next variable, by a search of the stack. -/
 @[local fun_prop] private lemma assignment_pt :
@@ -260,7 +178,8 @@ private theorem assignment_eq (stack : List Frame) (v : ℕ) :
   have h : ComputableInPolyTime (fun p : State × Frame => Frame.binds p.1.head.2 p.2)
       (encPair encState encFrame) encBool :=
     binds_pt.comp (g := fun p : State × Frame => (p.1.head.2, p.2)) (by fun_prop)
-  exact optionElimWithInput (findWithInput stack_pt h) (const false) (by fun_prop)
+  exact optionElimWithInput (findWithInput (encState_stack_polyTime id') h) (const false)
+    (by fun_prop)
 
 /-- A step reading a token is polynomial-time. -/
 private lemma readStep_pt (k : QBF.Kind) :
@@ -275,7 +194,7 @@ private lemma retStep_pt (k : QBF.Kind) (second : Bool) :
 /-- **A step of the evaluator is polynomial-time** in the encoded state. -/
 theorem computableInPolyTime_step : ComputableInPolyTime step encState encState := by
   rw [show step = _ from funext step_eq]
-  refine ite (optionIsSome value_pt) (ite (by fun_prop) id' ?_)
+  refine ite (optionIsSome (encState_value_polyTime id')) (ite (by fun_prop) id' ?_)
     (ite (by fun_prop) (by fun_prop) ?_)
   · exact finite_cases (tagEncoding := encPair encKind encBool)
       (tag := fun s => (s.top.token.1, s.top.first.isSome))
@@ -311,9 +230,8 @@ private theorem length_encFrame_le {φ : QBF ℕ} {f : Frame} (h : f.token :: f.
     (encFrame f).length ≤ (encQBF φ).length + 5 := by
   have hs := length_encList_le_of_suffix h
   have hfirst : (encOption encBool f.first).length ≤ 2 := by cases f.first <;> simp [encOption]
-  change (encFrameFields f.fields).length ≤ _
   rw [encQBF_apply]
-  simp only [Frame.fields, length_encPair, encList_cons, List.length_append, length_frame] at hs ⊢
+  simp only [encFrame_apply, length_encPair, encList_cons, List.length_append, length_frame] at hs ⊢
   omega
 
 /-- **The states of a run are of quadratic size**: a state satisfying the invariant on `φ` has an
@@ -329,8 +247,7 @@ theorem length_encState_le {φ : QBF ℕ} {s : State} (h : Good φ s) :
     h.length_stack_le.trans (by have := three_mul_length_tokens_le φ; omega)
   have hval : (encOption encBool s.value).length ≤ 2 := by cases s.value <;> simp [encOption]
   have hmul := Nat.mul_le_mul_right (2 * ((encQBF φ).length + 5) + 1) hdepth
-  change (encStateFields s.fields).length ≤ _
-  simp only [State.fields, length_encPair, encBool_apply, List.length_singleton]
+  simp only [encState_apply, length_encPair, encBool_apply, List.length_singleton]
   nlinarith
 
 /-! ### The evaluator in polynomial space -/
diff --git a/Complexity/Computability/GenericRAM/Simulation/Turing.lean b/Complexity/Computability/GenericRAM/Simulation/Turing.lean
index d780cd835d..c1dbc96a46 100644
--- a/Complexity/Computability/GenericRAM/Simulation/Turing.lean
+++ b/Complexity/Computability/GenericRAM/Simulation/Turing.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Equali
 public import Complexity.Computability.GenericRAM.Simulation.Finite
 public import Complexity.Computability.GenericRAM.SparseMemory.Turing
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Pi
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 
 /-!
 # Native implementation of fixed-program finite RAM steps
@@ -68,22 +69,11 @@ open NativeCertificate
 variable {M : Model.{0, 0, 0, 0}} {r : ℕ}
 
 /-- Encode all finite state components, including the default and distinct stored bindings. -/
-def encoding (enc : M.Encoding) : FiniteState M r ↪ List Bool :=
-  ⟨fun s => encPair encNat (encPair (encPi enc.value)
-      (encPair enc.value (SparseMemory.encoding enc.address enc.value)))
-      (s.pc, s.regs, s.default, s.memory), by
-    intro s t h
-    have hp := (encPair encNat (encPair (encPi enc.value)
-      (encPair enc.value (SparseMemory.encoding enc.address enc.value)))).injective h
-    cases s
-    cases t
-    cases hp
-    rfl⟩
-
-@[simp] theorem encoding_apply (enc : M.Encoding) (s : FiniteState M r) :
-    encoding enc s = encPair encNat (encPair (encPi enc.value)
-      (encPair enc.value (SparseMemory.encoding enc.address enc.value)))
-      (s.pc, s.regs, s.default, s.memory) := rfl
+enc_structure encoding (enc : M.Encoding) : FiniteState M r where
+  pc : encNat, regs : (encPi (Index := Fin r) enc.value), default : enc.value,
+  memory : (SparseMemory.encoding enc.address enc.value)
+
+attribute [simp] encoding_apply
 
 /-- Configuration is a runtime input, alongside the complete finite state. -/
 abbrev inputEncoding (enc : M.Encoding) :
diff --git a/Complexity/Computability/Kolmogorov/MINKT.lean b/Complexity/Computability/Kolmogorov/MINKT.lean
index 184119e7bd..fffc36c410 100644
--- a/Complexity/Computability/Kolmogorov/MINKT.lean
+++ b/Complexity/Computability/Kolmogorov/MINKT.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.NP.Witness
 public import Complexity.Computability.Complexity.Classes.Promise.Basic
 public import Complexity.Computability.Kolmogorov.TimeBounded
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
@@ -111,16 +112,9 @@ namespace MINKT
 
 /-- Standard encoding of `MINKT.Instance`: the string `x`, followed by `1^time` and `1^size` in
 unary ([Ko][Ko1991]; [Hirahara, Definition 9][Hirahara2018]). -/
-def enc : Instance ↪ List Bool :=
-  (⟨fun i => (i.string, (i.time, i.size)), fun i j h => by
-    cases i; cases j; simpa using h⟩ : Instance ↪ List Bool × (ℕ × ℕ)).trans
-    (encPair encBits (encPair encUnary encUnary))
+enc_structure enc : Instance where string : encBits, time : encUnary, size : encUnary
 
-/-- Applying `MINKT.enc` encodes `(i.string, (i.time, i.size))` via `encPair`. -/
-@[simp]
-theorem enc_apply (i : Instance) :
-    enc i = encPair encBits (encPair encUnary encUnary) (i.string, (i.time, i.size)) :=
-  rfl
+attribute [simp] enc_apply
 
 /-- The unary size parameter `i.size` is at most the encoded instance length `(enc i).length`. -/
 theorem size_le_length_enc (i : Instance) : i.size ≤ (enc i).length := by
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Machine.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Machine.lean
index 8ae0d6cd23..ca865b18e3 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Machine.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Machine.lean
@@ -11,6 +11,7 @@ public import Complexity.Algorithms.Reachability.InductiveCounting.Bounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.InductiveCounting.Encoding
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.InductiveCounting.Graph
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.NondeterministicQueryMachine
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 
 /-!
 # The input-scanning query machine for inductive counting
@@ -70,16 +71,8 @@ structure Runtime where
   counting : Option Cslib.InductiveCounting.State
 
 /-- The state encoding omits the input and every proof-level choice history. -/
-def encRuntime : Runtime ↪ List Bool :=
-  ⟨fun s => encPair encNat (encPair encNat (encPair encBool (encOption encState)))
-      (s.length, s.radix, s.checked, s.counting), by
-    intro s t h
-    have h' := (encPair encNat (encPair encNat (encPair encBool (encOption encState)))).injective h
-    cases s
-    cases t
-    simp only [Prod.mk.injEq] at h'
-    obtain ⟨rfl, rfl, rfl, rfl⟩ := h'
-    rfl⟩
+enc_structure encRuntime : Runtime where
+  length : encNat, radix : encNat, checked : encBool, counting : (encOption encState)
 
 variable {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State)
 
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean
index 446b9db5f2..278470731c 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean
@@ -7,6 +7,7 @@ Authors: Bolton Bailey, Samuel Schlesinger
 module
 -- upstream: candidate
 
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 public import Complexity.Algorithms.Reachability.Savitch
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
@@ -94,20 +95,9 @@ namespace Savitch
 
 /-! ### Encodings -/
 
-/-- The fields of a frame. -/
-def Frame.fields (f : Frame) : ℕ × List Bool × List Bool × List Bool × Bool :=
-  (f.level, f.src, f.dst, f.mid, f.phase)
-
-/-- The encoding of the fields of a frame: the level in unary, the words as themselves. -/
-abbrev encFrameFields : ℕ × List Bool × List Bool × List Bool × Bool ↪ List Bool :=
-  encPair encUnary (encPair encBits (encPair encBits (encPair encBits encBool)))
-
-/-- Frames encoded by their fields. -/
-def encFrame : Frame ↪ List Bool :=
-  ⟨fun f => encFrameFields f.fields, fun f g h => by
-    obtain ⟨⟩ := f
-    obtain ⟨⟩ := g
-    simpa [Frame.fields] using encFrameFields.injective h⟩
+/-- Frames encoded by their fields: the level in unary, the words as themselves. -/
+enc_structure encFrame : Frame where
+  level : encUnary, src : encBits, dst : encBits, mid : encBits, phase : encBool
 
 /-- The register as a pending call, if any, and the returned value, `false` during a call. -/
 def Reg.toPair : Reg → Option (ℕ × List Bool × List Bool) × Bool
@@ -124,11 +114,7 @@ def encReg : Reg ↪ List Bool :=
     cases r <;> cases r' <;> simp_all [Reg.toPair]⟩
 
 /-- States encoded as the list of their frames followed by their register. -/
-def encState : State ↪ List Bool :=
-  ⟨fun s => encPair (encList encFrame) encReg (s.stack, s.reg), fun s s' h => by
-    obtain ⟨⟩ := s
-    obtain ⟨⟩ := s'
-    simpa using (encPair (encList encFrame) encReg).injective h⟩
+enc_structure encState : State where stack : (encList encFrame), reg : encReg
 
 /-! ### The step in linear time, apart from the edge test -/
 
@@ -220,11 +206,11 @@ attribute [local fun_prop] ComputableTidilyInDegree.increment
 /-- The stack of a state. -/
 @[local fun_prop] private lemma stack_deg :
     ComputableTidilyInDegree State.stack encState (encList encFrame) 1 1 :=
-  of_linear (.of_unframe fun s => by simp [encState])
+  of_linear (.of_unframe fun s => by simp [encState_apply])
 
 /-- The register of a state. -/
 @[local fun_prop] private lemma reg_deg : ComputableTidilyInDegree State.reg encState encReg 1 1 :=
-  of_linear (.of_dropFrame fun s => by simp [encState])
+  of_linear (.of_dropFrame fun s => by simp [encState_apply])
 
 /-- The register as a pair, the identity on encoded values. -/
 @[local fun_prop] private lemma toPair_deg :
@@ -232,7 +218,8 @@ attribute [local fun_prop] ComputableTidilyInDegree.increment
   of_eq fun _ => rfl
 
 /-- The fields of a frame, the identity on encoded values. -/
-private lemma fields_deg : ComputableTidilyInDegree Frame.fields encFrame encFrameFields 1 1 :=
+private lemma fields_deg : ComputableTidilyInDegree
+    (fun f : Frame => (f.level, f.src, f.dst, f.mid, f.phase)) encFrame encFrameFields 1 1 :=
   of_eq fun _ => rfl
 
 /-- The level of a frame. -/
@@ -355,8 +342,7 @@ private theorem step_eq (edge : List Bool → List Bool → Bool) (w : ℕ) (s :
 theorem length_encFrame (f : Frame) :
     (encFrame f).length =
       2 * f.level + 2 * f.src.length + 2 * f.dst.length + 2 * f.mid.length + 5 := by
-  change (encFrameFields f.fields).length = _
-  simp only [Frame.fields, length_encPair, encUnary_apply, encBits_apply, encBool_apply,
+  simp only [encFrame_apply, length_encPair, encUnary_apply, encBits_apply, encBool_apply,
     List.length_replicate, List.length_singleton]
   omega
 
@@ -374,7 +360,7 @@ theorem length_encReg_ret (b : Bool) : (encReg (.ret b)).length = 2 := rfl
 /-- The length of an encoded state. -/
 theorem length_encState (s : State) :
     (encState s).length = 2 * (encList encFrame s.stack).length + 1 + (encReg s.reg).length := by
-  simp [encState]
+  simp [encState_apply]
 
 /-! ### A step carrying the parameter of the edge test -/
 
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Structure.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Structure.lean
new file mode 100644
index 0000000000..e3949594d8
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Structure.lean
@@ -0,0 +1,206 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.FunProp
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimePrimitives
+public meta import Lean.Elab.Command
+
+/-!
+# Encodings of structures as the tuple of their fields
+
+`enc_structure eS binders : S where f₁ : e₁, …` declares the encoding of a structure as the framed
+tuple of its fields, with everything a certificate needs to work with it:
+
+* `eSFields`, the encoding of the tuple, and `eS`, the encoding of the structure;
+* `eS_apply`, unfolding `eS` to `eSFields` of the tuple, which is not a `simp` lemma, so that
+  lemmas stated about `eS` keep firing;
+* `eS_fields_deg`, the linear map from a structure to the tuple of its fields;
+* for each field `f`, the linear rules `eS_f_deg` and `eS_f_inO`, and `eS_f_polyTime`, which reads
+  the field of a computed structure;
+* the constructor rules `eS_mk_deg`, on tuples, `eS_mk_inO`, which adds up the bounds of its
+  arguments, and `eS_mk_polyTime`.
+
+The rules are `scoped` `fun_prop` rules, so that a program using the structure is assembled by
+`fun_prop` inside the namespace of the declaration, or after `open scoped` of that namespace.
+`global enc_structure` makes them ordinary `fun_prop` rules, for a structure in a public API.
+
+The structure may have parameters, written as a term such as `Edge C`, and `eS` may take binders,
+such as an encoding of a parameter. Explicit binders stay explicit arguments of `eS` and
+`eSFields`, and are implicit in the rules that take hypotheses. An encoding built from
+noncomputable parts is declared with `noncomputable enc_structure`.
+-/
+
+public meta section
+
+namespace Turing.MultiTapeTM
+
+open Lean Elab Command
+open Lean.Parser.Term (attrInstance)
+
+/-- `enc_structure eS binders : S where f₁ : e₁, f₂ : e₂` declares the encoding `eS` of the
+structure `S` as the tuple of its fields encoded by `e₁`, `e₂`, with its rules. -/
+syntax (name := encStructure) (docComment)? ("noncomputable ")? ("global ")? "enc_structure " ident
+  (ppSpace bracketedBinder)* " : " term " where " (ident " : " term:max),+ : command
+
+private def app (base : Name) (suffix : String) : Ident :=
+  mkIdent (base.appendAfter suffix)
+
+/-- The tuple `(t₁, (t₂, …))`. -/
+private def tuple (ts : Array Term) : MacroM Term := do
+  let mut r := ts.back!
+  for t in ts.pop.reverse do
+    r ← `(($t, $r))
+  return r
+
+/-- `h.snd'…snd'.fst'`: component `i` of the `n`-tuple `h`, for `ns` the calculus namespace. -/
+private def component (ns : Name) (h : Term) (i n : Nat) : MacroM Term := do
+  let snd := mkIdent (ns ++ `snd')
+  let fst := mkIdent (ns ++ `fst')
+  let mut r := h
+  for _ in [0:i] do
+    r ← `($snd $r)
+  if i + 1 < n then r ← `($fst $r)
+  return r
+
+/-- The names bound by the explicit binders among `bs`, as arguments. -/
+private def explicitArgs (bs : TSyntaxArray ``Lean.Parser.Term.bracketedBinder) : Array Term :=
+  bs.flatMap fun b =>
+    if b.raw.isOfKind ``Lean.Parser.Term.explicitBinder then
+      b.raw[1].getArgs.map fun n => ⟨n⟩
+    else #[]
+
+/-- The binders `bs`, with explicit ones made implicit: a rule finds them by unification. -/
+private def implicitBinders (bs : TSyntaxArray ``Lean.Parser.Term.bracketedBinder) :
+    TSyntaxArray ``Lean.Parser.Term.bracketedBinder :=
+  bs.map fun b =>
+    if b.raw.isOfKind ``Lean.Parser.Term.explicitBinder then
+      ⟨mkNode ``Lean.Parser.Term.implicitBinder #[mkAtom "{", b.raw[1], b.raw[2], mkAtom "}"]⟩
+    else b
+
+/-- The structure named at the head of the type `S`. -/
+private def headName (S : Term) : CommandElabM Name :=
+  match S with
+  | `($f:ident $_*) | `($f:ident) => return f.getId
+  | _ => throwErrorAt S "enc_structure: expected a structure, optionally applied to parameters"
+
+/-- Elaborate `enc_structure`: the encoding, its unfolding lemma and its rules. -/
+@[command_elab encStructure] def elabEncStructure : CommandElab := fun stx => do
+  let `($[$doc:docComment]? $[noncomputable%$nc]? $[global%$gl]? enc_structure $eS:ident
+      $bs:bracketedBinder* : $S:term where $[$fs:ident : $es:term],*) :=
+    stx | throwUnsupportedSyntax
+  let name := eS.getId
+  let rule ← if gl.isSome then `(attrInstance| fun_prop) else `(attrInstance| scoped fun_prop)
+  let struct ← headName S
+  let args := explicitArgs bs
+  let ibs := implicitBinders bs
+  let a := mkIdent `a
+  let n := fs.size
+  let last := n - 1
+  let (tup, enc) ← liftMacroM do
+    let tup ← tuple (fs.map fun f => ⟨mkIdent (a.getId ++ f.getId)⟩)
+    let mut enc : Term := es.back!
+    for e in es.pop.reverse do
+      enc ← `(encPair $e $enc)
+    return (tup, enc)
+  let fieldsName := app name "Fields"
+  let fields : Term := Syntax.mkApp fieldsName args
+  let encS : Term := Syntax.mkApp eS args
+  let lin : Term ← `(fun a => List.length ($encS a))
+  if nc.isSome then
+    elabCommand (← `(public noncomputable abbrev $fieldsName:ident $bs* := $enc))
+    elabCommand (← `($[$doc:docComment]? @[expose] public noncomputable def $eS:ident $bs* :
+      $S ↪ List Bool :=
+      (⟨fun $a => $tup, fun x y h => by cases x; cases y; simp_all⟩ : $S ↪ _).trans $fields))
+  else
+    elabCommand (← `(public abbrev $fieldsName:ident $bs* := $enc))
+    elabCommand (← `($[$doc:docComment]? @[expose] public def $eS:ident $bs* : $S ↪ List Bool :=
+      (⟨fun $a => $tup, fun x y h => by cases x; cases y; simp_all⟩ : $S ↪ _).trans $fields))
+  addDocStringCore ((← getCurrNamespace) ++ fieldsName.getId)
+    s!"The tuple of the fields of `{name}`."
+  elabCommand (← `(public theorem $(app name "_apply") $bs* ($a : $S) :
+    $encS $a = $fields $tup := rfl))
+  let fieldsDeg := app name "_fields_deg"
+  let fieldsDegT : Term := Syntax.mkApp fieldsDeg args
+  elabCommand (← `(public theorem $fieldsDeg:ident $bs* :
+    ComputableInDegree (fun $a : $S => $tup) $encS $fields 1 1 :=
+      ComputableInDegree.of_eq fun _ => rfl))
+  let fieldsPoly : Term ← `((ComputableInPolyTime.of_eq fun _ => rfl :
+    ComputableInPolyTime (fun $a : $S => $tup) $encS $fields))
+  let γ := mkIdent `γ
+  let encIn := mkIdent `encIn
+  let g := mkIdent `g
+  let x := mkIdent `x
+  for f in fs, e in es, i in Array.range n do
+    let proj := mkIdent (struct ++ f.getId)
+    let deg := app name s!"_{f.getId}_deg"
+    let body ← liftMacroM <| component `Turing.MultiTapeTM.ComputableInDegree fieldsDegT i n
+    elabCommand (← `(@[$rule:attrInstance] public theorem $deg:ident $bs* :
+      ComputableInDegree ($proj : $S → _) $encS $e 1 1 := $body))
+    let degT : Term := Syntax.mkApp deg args
+    elabCommand (← `(@[$rule:attrInstance] public theorem
+      $(app name s!"_{f.getId}_inO"):ident $bs* :
+      ComputableInO ($proj : $S → _) $encS $e $lin $lin :=
+        ComputableInDegree.inO_one $degT))
+    let poly ← liftMacroM <| component `Turing.MultiTapeTM.ComputableInPolyTime fieldsPoly i n
+    elabCommand (← `(@[$rule:attrInstance] public theorem
+      $(app name s!"_{f.getId}_polyTime"):ident $ibs* {$γ : Type} {$encIn : $γ ↪ List Bool}
+      {$g : $γ → $S}
+      (h : ComputableInPolyTime $g $encIn $encS) :
+      ComputableInPolyTime (fun $x => $proj ($g $x)) $encIn $e :=
+        ComputableInPolyTime.comp $poly h))
+  let p := mkIdent `p
+  let comps ← (List.range n).toArray.mapM fun i => do
+    let mut t : Term ← `($p)
+    for _ in [0:i] do
+      t ← `(($t).2)
+    if i + 1 < n then t ← `(($t).1)
+    return t
+  let mk := mkIdent (struct ++ `mk)
+  let mkApp : Term := Syntax.mkApp mk comps
+  elabCommand (← `(@[$rule:attrInstance] public theorem $(app name "_mk_deg"):ident $bs* :
+    ComputableInDegree (fun $p => ($mkApp : $S)) $fields $encS 1 1 :=
+      ComputableInDegree.of_eq fun _ => rfl))
+  -- the constructor, adding up the bounds of its arguments
+  let xN (i : Nat) := mkIdent (Name.mkSimple s!"x{i}")
+  let hN (i : Nat) := mkIdent (Name.mkSimple s!"h{i}")
+  let TN (i : Nat) := mkIdent (Name.mkSimple s!"T{i}")
+  let SN (i : Nat) := mkIdent (Name.mkSimple s!"S{i}")
+  let mut sumT : Term ← `($(TN last) $x:ident)
+  let mut sumS : Term ← `($(SN last) $x:ident)
+  let mut prod : Term := hN last
+  let mut prodPoly : Term := hN last
+  for i in (List.range last).reverse do
+    sumT ← `($(TN i) $x:ident + $sumT)
+    sumS ← `($(SN i) $x:ident + $sumS)
+    prod ← `(ComputableInO.prod $(hN i) $prod)
+    prodPoly ← `(ComputableInPolyTime.prod $(hN i) $prodPoly)
+  let appl : Term := Syntax.mkApp mk ((Array.range n).map fun i =>
+    ⟨Syntax.mkApp (xN i) #[x]⟩)
+  let mut fns : TSyntaxArray ``Lean.Parser.Term.bracketedBinder := #[]
+  let mut bounds : TSyntaxArray ``Lean.Parser.Term.bracketedBinder := #[]
+  let mut hsO : TSyntaxArray ``Lean.Parser.Term.bracketedBinder := #[]
+  let mut hsPoly : TSyntaxArray ``Lean.Parser.Term.bracketedBinder := #[]
+  for e in es, i in Array.range n do
+    fns := fns.push (← `(bracketedBinder| {$(xN i) : $γ → _}))
+    bounds := bounds.push (← `(bracketedBinder| {$(TN i) $(SN i) : $γ → ℕ}))
+    hsO := hsO.push (← `(bracketedBinder|
+      ($(hN i) : ComputableInO $(xN i) $encIn $e $(TN i) $(SN i))))
+    hsPoly := hsPoly.push (← `(bracketedBinder|
+      ($(hN i) : ComputableInPolyTime $(xN i) $encIn $e)))
+  elabCommand (← `(@[$rule:attrInstance] public theorem $(app name "_mk_inO"):ident $ibs*
+    {$γ : Type} {$encIn : $γ ↪ List Bool} $fns* $bounds* $hsO* :
+    ComputableInO (fun $x => ($appl : $S)) $encIn $encS (fun $x => $sumT) fun $x => $sumS :=
+      ComputableInO.of_enc_eq $prod fun _ => rfl))
+  elabCommand (← `(@[$rule:attrInstance] public theorem $(app name "_mk_polyTime"):ident $ibs*
+    {$γ : Type} {$encIn : $γ ↪ List Bool} $fns* $hsPoly* :
+    ComputableInPolyTime (fun $x => ($appl : $S)) $encIn $encS :=
+      ComputableInPolyTime.of_enc_eq $prodPoly fun _ => rfl))
+
+end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/TablePolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/TablePolyTime.lean
index cb04f090b9..1c84a20159 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/TablePolyTime.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/TablePolyTime.lean
@@ -300,7 +300,7 @@ theorem computableInPolyTime_intervalEntryNum {i : α → ℕ}
     refine bool_and' (binary_lt' (hLat hi) hC) (allConst _ fun h _ => allConst _ fun δ _ => ?_)
     exact bool_not.comp (binary_lt' (hLat (unary_add' hq (unary_add' (const _)
       (unary_mul' (const _) hi)))) hC)
-  · have hd := IntervalData.computableInPolyTime_mk hx hb
+  · have hd := encIntervalData_mk_polyTime hx hb
       (computableInPolyTime_blockIndexNum hσ hi) (computableInPolyTime_blockMoveNum hσ hi) hcIn
       (pi fun h : Fin k => computableInPolyTime_inCellsNum (k := k) (s := s) h.val hb hq hσ hL hi)
       (computableInPolyTime_decodeControlData e hb hb0 (hLat hi))
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean
index b2581b0aa0..63b1ecb77f 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalCount/PolyTime.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Finit
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.IntBinary
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pi
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Tape
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Words
 public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
@@ -60,7 +61,7 @@ their stored cells (`Turing.MultiTapeTM.encBiTape`), and the head positions in b
 ## Main results
 
 * `Turing.MultiTapePTM.computableInPolyTime_localRun`: replays are polynomial-time.
-* `Turing.MultiTapePTM.IntervalData.computableInPolyTime_mk`,
+* `Turing.MultiTapePTM.encIntervalData_mk_polyTime`,
   `Turing.MultiTapePTM.ControlData.computableInPolyTime_mk`: assembling the arguments.
 * `Turing.MultiTapePTM.computableInPolyTime_localIntervalCount`: interval counts are
   polynomial-time when the `2 ^ b` coin strings are polynomially many in the input.
@@ -76,22 +77,15 @@ variable {k : ℕ} {State : Type}
 
 /-! ### Encoding finite storage -/
 
-/-- Finite storage as the tuple of its fields. -/
-@[expose] def LocalCfg.equivProd :
-    LocalCfg k State ≃ Option State × ℕ × (Fin k → BiTape Bool) × (Fin k → ℤ) × OutputTrack where
-  toFun l := (l.state, l.inputPos, l.workTapes, l.workTapePos, l.track)
-  invFun p := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2.1, p.2.2.2.2⟩
-  left_inv _ := rfl
-  right_inv _ := rfl
-
 variable [Finite State]
 
 /-- **The encoding of finite storage**: the control and the output track by their ranks, the input
 position in unary, the work tapes with all their stored cells, and the head positions in
 binary. -/
-noncomputable def encLocalCfg : LocalCfg k State ↪ List Bool :=
-  encOfEquiv LocalCfg.equivProd (encPair (encFinite (Option State)) (encPair encUnary
-    (encPair (encPi (encBiTape encBool)) (encPair (encPi encIntBin) (encFinite OutputTrack)))))
+noncomputable enc_structure encLocalCfg : LocalCfg k State where
+  state : (encFinite (Option State)), inputPos : encUnary,
+  workTapes : (encPi (Index := Fin k) (encBiTape encBool)),
+  workTapePos : (encPi (Index := Fin k) encIntBin), track : (encFinite OutputTrack)
 
 /-! ### Rules for finite storage -/
 
@@ -99,47 +93,6 @@ section Rules
 
 variable {α : Type} {input : α ↪ List Bool}
 
-/-- Assemble finite storage from its certified fields. -/
-private theorem localCfg_mk {state : α → Option State} {pos : α → ℕ}
-    {tapes : α → Fin k → BiTape Bool} {coords : α → Fin k → ℤ} {track : α → OutputTrack}
-    (hstate : ComputableInPolyTime state input (encFinite (Option State)))
-    (hpos : ComputableInPolyTime pos input encUnary)
-    (htapes : ComputableInPolyTime tapes input (encPi (encBiTape encBool)))
-    (hcoords : ComputableInPolyTime coords input (encPi encIntBin))
-    (htrack : ComputableInPolyTime track input (encFinite OutputTrack)) :
-    ComputableInPolyTime (fun a => (⟨state a, pos a, tapes a, coords a, track a⟩ :
-      LocalCfg k State)) input encLocalCfg :=
-  (hstate.prod (hpos.prod (htapes.prod (hcoords.prod htrack)))).of_enc_eq fun _ => rfl
-
-private theorem localCfg_parts : ComputableInPolyTime (LocalCfg.equivProd (k := k) (State := State))
-    encLocalCfg (encPair (encFinite (Option State)) (encPair encUnary
-      (encPair (encPi (encBiTape encBool)) (encPair (encPi encIntBin) (encFinite OutputTrack))))) :=
-  of_eq fun _ => rfl
-
-private theorem localCfg_state :
-    ComputableInPolyTime (LocalCfg.state (k := k) (State := State)) encLocalCfg
-      (encFinite (Option State)) :=
-  localCfg_parts.fst'
-
-private theorem localCfg_inputPos :
-    ComputableInPolyTime (LocalCfg.inputPos (k := k) (State := State)) encLocalCfg encUnary :=
-  localCfg_parts.snd'.fst'
-
-private theorem localCfg_workTapes :
-    ComputableInPolyTime (LocalCfg.workTapes (k := k) (State := State)) encLocalCfg
-      (encPi (encBiTape encBool)) :=
-  localCfg_parts.snd'.snd'.fst'
-
-private theorem localCfg_workTapePos :
-    ComputableInPolyTime (LocalCfg.workTapePos (k := k) (State := State)) encLocalCfg
-      (encPi encIntBin) :=
-  localCfg_parts.snd'.snd'.snd'.fst'
-
-private theorem localCfg_track :
-    ComputableInPolyTime (LocalCfg.track (k := k) (State := State)) encLocalCfg
-      (encFinite OutputTrack) :=
-  localCfg_parts.snd'.snd'.snd'.snd'
-
 /-- Adding a binary integer, by two subtractions. -/
 private theorem intBin_add' {left right : α → ℤ}
     (hleft : ComputableInPolyTime left input encIntBin)
@@ -197,23 +150,24 @@ private theorem computableInPolyTime_applyAction (a : Action k Bool State) :
   have h1 : ComputableInPolyTime (fun p : (List Bool × LocalCfg k State) × Bool => p.1.1.length)
       (encPair (encPair encBits encLocalCfg) encBool) encUnary := length_bits.comp hword
   have h2 : ComputableInPolyTime (fun p : (List Bool × LocalCfg k State) × Bool => p.1.2.inputPos)
-      (encPair (encPair encBits encLocalCfg) encBool) encUnary := localCfg_inputPos.comp hcfg
+      (encPair (encPair encBits encLocalCfg) encBool) encUnary := encLocalCfg_inputPos_polyTime hcfg
   have h3 := (MultiTapeTM.ComputableInPolyTime.moveInputPosNat a.inputTape).comp (h1.prod h2)
   have h4 : ComputableInPolyTime
       (fun p : (List Bool × LocalCfg k State) × Bool => fun h => (p.1.2.workTapes h).step
         (a.workTapes h)) (encPair (encPair encBits encLocalCfg) encBool)
         (encPi (encBiTape encBool)) :=
-    pi fun h => biTape_step (a.workTapes h) ((pi_apply _ h).comp (localCfg_workTapes.comp hcfg))
+    pi fun h => biTape_step (a.workTapes h)
+      ((pi_apply _ h).comp (encLocalCfg_workTapes_polyTime hcfg))
   have h5 : ComputableInPolyTime
       (fun p : (List Bool × LocalCfg k State) × Bool => fun h => p.1.2.workTapePos h +
         ((a.workTapes h).2 : ℤ)) (encPair (encPair encBits encLocalCfg) encBool)
         (encPi encIntBin) :=
-    pi fun h => intBin_add' ((pi_apply _ h).comp (localCfg_workTapePos.comp hcfg)) (const _)
+    pi fun h => intBin_add' ((pi_apply _ h).comp (encLocalCfg_workTapePos_polyTime hcfg)) (const _)
   have h6 : ComputableInPolyTime
       (fun p : (List Bool × LocalCfg k State) × Bool => p.1.2.track.emit a.output)
       (encPair (encPair encBits encLocalCfg) encBool) (encFinite OutputTrack) :=
-    (of_finite fun t : OutputTrack => t.emit a.output).comp (localCfg_track.comp hcfg)
-  exact localCfg_mk (const a.state) h3 h4 h5 h6
+    (of_finite fun t : OutputTrack => t.emit a.output).comp (encLocalCfg_track_polyTime hcfg)
+  exact encLocalCfg_mk_polyTime (const a.state) h3 h4 h5 h6
 
 /-- The key of a coin step is polynomial-time. -/
 private theorem computableInPolyTime_stepKey :
@@ -225,13 +179,14 @@ private theorem computableInPolyTime_stepKey :
   have hheads : ComputableInPolyTime
       (fun p : (List Bool × LocalCfg k State) × Bool => fun h => (p.1.2.workTapes h).head)
       (encPair (encPair encBits encLocalCfg) encBool) (encPi (encOption encBool)) :=
-    pi fun h => (biTape_head encBool).comp ((pi_apply _ h).comp (localCfg_workTapes.comp hcfg))
+    pi fun h => (biTape_head encBool).comp
+      ((pi_apply _ h).comp (encLocalCfg_workTapes_polyTime hcfg))
   have hheads' : ComputableInPolyTime
       (fun p : (List Bool × LocalCfg k State) × Bool => fun h => (p.1.2.workTapes h).head)
       (encPair (encPair encBits encLocalCfg) encBool) (encFinite (Fin k → Option Bool)) :=
     (of_finite id).comp hheads
-  have hsym := inputAt' hword (localCfg_inputPos.comp hcfg)
-  have hall := (localCfg_state.comp hcfg).prod (hsym.prod (hheads'.prod hbit))
+  have hsym := inputAt' hword (encLocalCfg_inputPos_polyTime hcfg)
+  have hall := (encLocalCfg_state_polyTime hcfg).prod (hsym.prod (hheads'.prod hbit))
   exact (of_finite id).comp hall
 
 /-- **One coin step is polynomial-time.** -/
@@ -357,8 +312,8 @@ private theorem length_encLocalCfg_localCoinStep_le (input : List Bool) (l : Loc
     (machine.localCoinStep input l bit).workTapePos 2
     fun h => length_encIntBin_add_sign_le (l.workTapePos h) (a.workTapes h).2
   simp only [Fintype.card_fin] at htapes hcoords
-  simp only [encLocalCfg, encOfEquiv_apply, LocalCfg.equivProd, Equiv.coe_fn_mk, length_encPair,
-    encUnary_apply, List.length_replicate, stepGrowth] at hstate htrack ⊢
+  simp only [encLocalCfg_apply, length_encPair, encUnary_apply, List.length_replicate,
+    stepGrowth] at hstate htrack ⊢
   omega
 
 end Growth
@@ -492,8 +447,9 @@ private theorem localCfg_headCoord {l : α → LocalCfg k State}
   cases head with
   | none =>
     exact intBin_sub.comp
-      ((intBin_natCast.comp (unary_to_binary.comp (localCfg_inputPos.comp hl))).prod (const 1))
-  | some h => exact (pi_apply _ h).comp (localCfg_workTapePos.comp hl)
+      ((intBin_natCast.comp (unary_to_binary.comp (encLocalCfg_inputPos_polyTime hl))).prod
+        (const 1))
+  | some h => exact (pi_apply _ h).comp (encLocalCfg_workTapePos_polyTime hl)
 
 /-- The window cells of computed storage. -/
 private theorem localCfg_windowCellsAt {b : α → ℕ} {j : α → ℤ} {l : α → LocalCfg k State}
@@ -510,9 +466,10 @@ private theorem localCfg_windowCellsAt {b : α → ℕ} {j : α → ℤ} {l : α
       (fun p : α × ℕ => (b p.1 : ℤ) * (j p.1 - 1) + (p.2 : ℤ) - (l p.1).workTapePos h)
       (encPair input encUnary) encIntBin :=
     intBin_sub.comp ((intBin_add' (intBin_mul' hbZ (intBin_sub.comp ((hj.comp hfst).prod
-      (const 1)))) hcZ).prod ((pi_apply _ h).comp (localCfg_workTapePos.comp (hl.comp hfst))))
+      (const 1)))) hcZ).prod
+        ((pi_apply _ h).comp (encLocalCfg_workTapePos_polyTime (hl.comp hfst))))
   exact mapWithInput (unary_range' (unary_mul' (const 3) hb))
-    (biTape_read ((pi_apply _ h).comp (localCfg_workTapes.comp (hl.comp hfst))) hoff)
+    (biTape_read ((pi_apply _ h).comp (encLocalCfg_workTapes_polyTime (hl.comp hfst))) hoff)
 
 /-- The stored input position of a coordinate. -/
 private theorem val_inputPosOfCoord (x : List Bool) (p : ℤ) :
@@ -576,16 +533,6 @@ structure IntervalData (k : ℕ) (State : Type) where
   /-- The leaving window cells. -/
   wOut : Fin k → List (Option Bool)
 
-/-- The arguments of an interval count as a tuple. -/
-@[expose] def IntervalData.equivProd : IntervalData k State ≃
-    List Bool × ℕ × (Option (Fin k) → ℤ) × (Option (Fin k) → SignType) × ControlData k State ×
-      (Fin k → List (Option Bool)) × ControlData k State × (Fin k → List (Option Bool)) where
-  toFun d := (d.input, d.b, d.J, d.δ, d.cIn, d.wIn, d.cOut, d.wOut)
-  invFun p := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2.1, p.2.2.2.2.1, p.2.2.2.2.2.1, p.2.2.2.2.2.2.1,
-    p.2.2.2.2.2.2.2⟩
-  left_inv _ := rfl
-  right_inv _ := rfl
-
 /-- The encoding of a control record on plain data: the state and the track by their ranks, and
 the offsets in unary. -/
 noncomputable def encControlData : ControlData k State ↪ List Bool :=
@@ -593,11 +540,12 @@ noncomputable def encControlData : ControlData k State ↪ List Bool :=
 
 /-- **The encoding of the arguments of an interval count**: the input, the block length in unary,
 the block indices in binary, the movements by their ranks, and the records and window cells. -/
-noncomputable def encIntervalData : IntervalData k State ↪ List Bool :=
-  encOfEquiv IntervalData.equivProd (encPair encBits (encPair encUnary (encPair (encPi encIntBin)
-    (encPair (encFinite (Option (Fin k) → SignType)) (encPair encControlData
-      (encPair (encPi (encList (encOption encBool))) (encPair encControlData
-        (encPi (encList (encOption encBool))))))))))
+noncomputable enc_structure encIntervalData : IntervalData k State where
+  input : encBits, b : encUnary, J : (encPi (Index := Option (Fin k)) encIntBin),
+  δ : (encFinite (Option (Fin k) → SignType)), cIn : (encControlData (k := k) (State := State)),
+  wIn : (encPi (Index := Fin k) (encList (encOption encBool))),
+  cOut : (encControlData (k := k) (State := State)),
+  wOut : (encPi (Index := Fin k) (encList (encOption encBool)))
 
 /-- The interval count of its arguments. -/
 @[expose] def IntervalData.count [DecidableEq State] (machine : MultiTapePTM k Bool State)
@@ -616,30 +564,6 @@ theorem ControlData.computableInPolyTime_mk {state : α → Option State}
       encControlData :=
   (hstate.prod (hoff.prod htrack)).of_enc_eq fun _ => rfl
 
-/-- Assemble the arguments of an interval count from their certified components. -/
-theorem IntervalData.computableInPolyTime_mk {word : α → List Bool} {b : α → ℕ}
-    {J : α → Option (Fin k) → ℤ} {δ : α → Option (Fin k) → SignType}
-    {cIn cOut : α → ControlData k State} {wIn wOut : α → Fin k → List (Option Bool)}
-    (hword : ComputableInPolyTime word input encBits) (hb : ComputableInPolyTime b input encUnary)
-    (hJ : ComputableInPolyTime J input (encPi encIntBin))
-    (hδ : ComputableInPolyTime δ input (encFinite _))
-    (hcIn : ComputableInPolyTime cIn input encControlData)
-    (hwIn : ComputableInPolyTime wIn input (encPi (encList (encOption encBool))))
-    (hcOut : ComputableInPolyTime cOut input encControlData)
-    (hwOut : ComputableInPolyTime wOut input (encPi (encList (encOption encBool)))) :
-    ComputableInPolyTime (fun a => (⟨word a, b a, J a, δ a, cIn a, wIn a, cOut a, wOut a⟩ :
-      IntervalData k State)) input encIntervalData :=
-  (hword.prod (hb.prod (hJ.prod (hδ.prod (hcIn.prod (hwIn.prod (hcOut.prod hwOut))))))).of_enc_eq
-    fun _ => rfl
-
-private theorem intervalData_parts : ComputableInPolyTime
-    (IntervalData.equivProd (k := k) (State := State)) encIntervalData
-    (encPair encBits (encPair encUnary (encPair (encPi encIntBin)
-      (encPair (encFinite (Option (Fin k) → SignType)) (encPair encControlData
-        (encPair (encPi (encList (encOption encBool))) (encPair encControlData
-          (encPi (encList (encOption encBool)))))))))) :=
-  of_eq fun _ => rfl
-
 private theorem controlData_parts : ComputableInPolyTime (fun c : ControlData k State => c)
     encControlData (encPair (encFinite (Option State)) (encPair (encPi encUnary)
       (encFinite OutputTrack))) :=
@@ -650,14 +574,13 @@ private theorem localStartData' {d : α → IntervalData k State}
     (hd : ComputableInPolyTime d input encIntervalData) :
     ComputableInPolyTime (fun a => localStartData (d a).b (d a).input (d a).J (d a).cIn (d a).wIn)
       input encLocalCfg := by
-  have hp := intervalData_parts.comp hd
-  have hword : ComputableInPolyTime (fun a => (d a).input) input encBits := hp.fst'
-  have hb : ComputableInPolyTime (fun a => (d a).b) input encUnary := hp.snd'.fst'
-  have hJ : ComputableInPolyTime (fun a => (d a).J) input (encPi encIntBin) := hp.snd'.snd'.fst'
-  have hc := controlData_parts.comp (hp.snd'.snd'.snd'.snd'.fst' :
+  have hword := encIntervalData_input_polyTime hd
+  have hb := encIntervalData_b_polyTime hd
+  have hJ := encIntervalData_J_polyTime hd
+  have hc := controlData_parts.comp (encIntervalData_cIn_polyTime hd :
     ComputableInPolyTime (fun a => (d a).cIn) input encControlData)
   have hw : ComputableInPolyTime (fun a => (d a).wIn) input
-      (encPi (encList (encOption encBool))) := hp.snd'.snd'.snd'.snd'.snd'.fst'
+      (encPi (encList (encOption encBool))) := encIntervalData_wIn_polyTime hd
   have hbZ : ComputableInPolyTime (fun a => ((d a).b : ℤ)) input encIntBin :=
     intBin_natCast.comp (unary_to_binary.comp hb)
   have hoff (head : Option (Fin k)) : ComputableInPolyTime (fun a => (d a).cIn.2.1 head) input
@@ -666,7 +589,7 @@ private theorem localStartData' {d : α → IntervalData k State}
       (fun a => ((d a).b : ℤ) * (d a).J head + ((d a).cIn.2.1 head : ℤ)) input encIntBin :=
     intBin_add' (intBin_mul' hbZ ((pi_apply _ head).comp hJ))
       (intBin_natCast.comp (unary_to_binary.comp (hoff head)))
-  exact localCfg_mk hc.fst' (inputPosOfCoord' hword (hcoord none))
+  exact encLocalCfg_mk_polyTime hc.fst' (inputPosOfCoord' hword (hcoord none))
     (pi fun h => biTape_ofCells ((pi_apply _ h).comp hw) (unary_add' hb (hoff (some h))))
     (pi fun h => hcoord (some h)) hc.snd'.snd'
 
@@ -705,25 +628,24 @@ private theorem computableInPolyTime_stepTest [DecidableEq State] :
       (encPair encIntervalData encLocalCfg) encBool := by
   have hd := fst (encIntervalData (k := k) (State := State)) (encLocalCfg (k := k) (State := State))
   have hl := snd (encIntervalData (k := k) (State := State)) (encLocalCfg (k := k) (State := State))
-  have hp := intervalData_parts.comp hd
   have hb : ComputableInPolyTime (fun p : IntervalData k State × LocalCfg k State => p.1.b)
-      (encPair encIntervalData encLocalCfg) encUnary := hp.snd'.fst'
+      (encPair encIntervalData encLocalCfg) encUnary := encIntervalData_b_polyTime hd
   have hJ : ComputableInPolyTime (fun p : IntervalData k State × LocalCfg k State => p.1.J)
-      (encPair encIntervalData encLocalCfg) (encPi encIntBin) := hp.snd'.snd'.fst'
+      (encPair encIntervalData encLocalCfg) (encPi encIntBin) := encIntervalData_J_polyTime hd
   have hδ : ComputableInPolyTime (fun p : IntervalData k State × LocalCfg k State => p.1.δ)
-      (encPair encIntervalData encLocalCfg) (encFinite _) := hp.snd'.snd'.snd'.fst'
-  have hc := controlData_parts.comp (hp.snd'.snd'.snd'.snd'.snd'.snd'.fst' :
+      (encPair encIntervalData encLocalCfg) (encFinite _) := encIntervalData_δ_polyTime hd
+  have hc := controlData_parts.comp (encIntervalData_cOut_polyTime hd :
     ComputableInPolyTime (fun p : IntervalData k State × LocalCfg k State => p.1.cOut)
       (encPair encIntervalData encLocalCfg) encControlData)
   have hw : ComputableInPolyTime (fun p : IntervalData k State × LocalCfg k State => p.1.wOut)
       (encPair encIntervalData encLocalCfg) (encPi (encList (encOption encBool))) :=
-    hp.snd'.snd'.snd'.snd'.snd'.snd'.snd'
+    encIntervalData_wOut_polyTime hd
   have hbZ : ComputableInPolyTime
       (fun p : IntervalData k State × LocalCfg k State => (p.1.b : ℤ))
       (encPair encIntervalData encLocalCfg) encIntBin :=
     intBin_natCast.comp (unary_to_binary.comp hb)
-  refine bool_and' (bool_and' (bool_and' (decide_eq' (localCfg_state.comp hl) hc.fst')
-    (decide_eq' (localCfg_track.comp hl) hc.snd'.snd')) ?_) ?_
+  refine bool_and' (bool_and' (bool_and' (decide_eq' (encLocalCfg_state_polyTime hl) hc.fst')
+    (decide_eq' (encLocalCfg_track_polyTime hl) hc.snd'.snd')) ?_) ?_
   · refine allConst _ fun head _ => bool_and' (unary_lt' ((pi_apply _ head).comp hc.snd'.fst') hb)
       (decide_eq' (localCfg_headCoord hl head) ?_)
     have hδZ : ComputableInPolyTime
@@ -745,13 +667,13 @@ theorem computableInPolyTime_localIntervalCount [DecidableEq State]
     (hbudget : ∀ a, 2 ^ (d a).b * (2 * (d a).b + 1) ≤ size (input a).length) :
     ComputableInPolyTime (fun a => (d a).count machine) input encUnary := by
   have hb : ComputableInPolyTime (fun a => (d a).b) input encUnary :=
-    (intervalData_parts.comp hd).snd'.fst'
+    encIntervalData_b_polyTime hd
   have hlist := bitsEnumList hb hsize hbudget
   have hfst := fst input encBits
   have hrun : ComputableInPolyTime (fun p : α × List Bool => machine.localRun (d p.1).input p.2
       (localStartData (d p.1).b (d p.1).input (d p.1).J (d p.1).cIn (d p.1).wIn))
       (encPair input encBits) encLocalCfg :=
-    computableInPolyTime_localRun machine ((intervalData_parts.comp (hd.comp hfst)).fst')
+    computableInPolyTime_localRun machine (encIntervalData_input_polyTime (hd.comp hfst))
       (snd _ _) (localStartData' (hd.comp hfst))
   have htest : ComputableInPolyTime (fun p : α × List Bool =>
       decide (machine.LocalIntervalStepData (d p.1).b (d p.1).input (d p.1).J (d p.1).δ
diff --git a/Complexity/Computability/PCP/Approximation/LabelCover/Incidence.lean b/Complexity/Computability/PCP/Approximation/LabelCover/Incidence.lean
index d05f20c67a..d6ab723ca5 100644
--- a/Complexity/Computability/PCP/Approximation/LabelCover/Incidence.lean
+++ b/Complexity/Computability/PCP/Approximation/LabelCover/Incidence.lean
@@ -273,10 +273,10 @@ private theorem isPolyTime_block (pairs : List (α × α)) (fallback : α × α)
       (encPair (Edge.encoding (encPi (encPi encBool))) encUnary)
       (encList (Edge.encoding (encPi encA))) := by
     unfold block
-    exact (Edge.isPolyTime_mk hidx (Edge.isPolyTime_src hleft)
-      (hproj₁.comp (Edge.isPolyTime_constraint hleft))).cons'
-        ((Edge.isPolyTime_mk hidx (Edge.isPolyTime_dst hleft)
-          (hproj₂.comp (Edge.isPolyTime_constraint hleft))).cons' (.const []))
+    exact (Edge.encoding_mk_polyTime hidx (Edge.encoding_src_polyTime hleft)
+      (hproj₁.comp (Edge.encoding_constraint_polyTime hleft))).cons'
+        ((Edge.encoding_mk_polyTime hidx (Edge.encoding_dst_polyTime hleft)
+          (hproj₂.comp (Edge.encoding_constraint_polyTime hleft))).cons' (.const []))
   exact hb
 
 omit [DecidableEq α] [Fintype α] in
@@ -305,7 +305,7 @@ private theorem isPolyTime_incidence (pairs : List (α × α)) (fallback : α ×
       (fun g : Graph (α → α → Bool) => g.edges.length)
       (Graph.encoding (encPi (encPi encBool))) encUnary :=
     (ComputableInPolyTime.length_list (Edge.encoding (encPi (encPi encBool)))).comp
-      (Graph.isPolyTime_edges ComputableInPolyTime.id')
+      (Graph.encoding_edges_polyTime ComputableInPolyTime.id')
   have hrange := ComputableInPolyTime.range.comp hlen
   have hindex : ComputableInPolyTime
       (fun p : Graph (α → α → Bool) × ℕ => p.2)
@@ -324,11 +324,11 @@ private theorem isPolyTime_incidence (pairs : List (α × α)) (fallback : α ×
       (fun g : Graph (α → α → Bool) => g.vertices + g.edges.length)
       (Graph.encoding (encPi (encPi encBool))) encUnary :=
     ComputableInPolyTime.unary_add'
-      (Graph.isPolyTime_vertices (ComputableInPolyTime.id'
+      (Graph.encoding_vertices_polyTime (ComputableInPolyTime.id'
         (encIn := Graph.encoding (encPi (encPi encBool))))) hlen
   unfold incidence
   simp_rw [zipIdx_edges_eq, List.flatMap_map]
-  exact Graph.isPolyTime_mk hvertices hedges
+  exact Graph.encoding_mk_polyTime hvertices hedges
 
 omit [DecidableEq α] in
 /-- The incidence reduction is polynomial-time for every fixed finite alphabet and fixed pair
diff --git a/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean b/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean
index b236c9cd0d..ddfc05dfcd 100644
--- a/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean
+++ b/Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean
@@ -251,7 +251,7 @@ theorem isPolyTime_toCNF :
     | cons p l ih =>
       simp only [List.filter_cons, List.map_cons, apply_ite]
       exact (htest p).ite ((hclause p).cons' ih) ih
-  exact flatMapWithInput (isPolyTime_edges id') ((hmapFilter pairs).comp (snd _ _))
+  exact flatMapWithInput (encoding_edges_polyTime id') ((hmapFilter pairs).comp (snd _ _))
 
 end Cslib.PCP.Encoded.Graph
 
diff --git a/Complexity/Computability/PCP/Encoded/AddTrivial.lean b/Complexity/Computability/PCP/Encoded/AddTrivial.lean
index b579bb08d6..ac4a690fa4 100644
--- a/Complexity/Computability/PCP/Encoded/AddTrivial.lean
+++ b/Complexity/Computability/PCP/Encoded/AddTrivial.lean
@@ -68,11 +68,11 @@ theorem isPolyTime_addTrivial (enc : C ↪ List Bool) (truth : C) :
       (encList (encPair encUnary encUnary)) := ComputableInPolyTime.snd _ _
   have hedge : ComputableInPolyTime (fun p : ℕ × ℕ => Edge.mk p.1 p.2 truth)
       (encPair encUnary encUnary) (Edge.encoding enc) :=
-    Edge.isPolyTime_mk (ComputableInPolyTime.fst _ _) (ComputableInPolyTime.snd _ _)
+    Edge.encoding_mk_polyTime (ComputableInPolyTime.fst _ _) (ComputableInPolyTime.snd _ _)
       (ComputableInPolyTime.const truth)
   unfold addTrivial
-  exact isPolyTime_mk (isPolyTime_vertices hgraph)
-    (ComputableInPolyTime.listAppend' (isPolyTime_edges hgraph)
+  exact encoding_mk_polyTime (encoding_vertices_polyTime hgraph)
+    (ComputableInPolyTime.listAppend' (encoding_edges_polyTime hgraph)
       ((ComputableInPolyTime.map hedge).comp hextra))
 
 /-- Constructing all self-loops, including enumerating their endpoints, is polynomial-time. -/
@@ -84,7 +84,7 @@ theorem isPolyTime_addLoops (enc : C ↪ List Bool) (truth : C) :
     (ComputableInPolyTime.id'.prod
       ((ComputableInPolyTime.map
         (ComputableInPolyTime.id'.prod ComputableInPolyTime.id')).comp
-        (ComputableInPolyTime.range.comp (isPolyTime_vertices ComputableInPolyTime.id'))))
+        (ComputableInPolyTime.range.comp (encoding_vertices_polyTime ComputableInPolyTime.id'))))
 
 /-- An appended edge list has the declared number of old and new edges. -/
 @[simp]
diff --git a/Complexity/Computability/PCP/Encoded/Basic.lean b/Complexity/Computability/PCP/Encoded/Basic.lean
index 1d691f98eb..a4338f0358 100644
--- a/Complexity/Computability/PCP/Encoded/Basic.lean
+++ b/Complexity/Computability/PCP/Encoded/Basic.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.PCP.ConstraintGraph
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 public import Complexity.Foundations.Data.List.Equiv
 import Mathlib.Data.List.GetD
 
@@ -67,49 +68,8 @@ namespace Edge
 variable {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool}
 
 /-- An edge is encoded by its unary endpoints and its constraint descriptor. -/
-def encoding (enc : C ↪ List Bool) : Edge C ↪ List Bool :=
-  ⟨fun e => encPair encUnary (encPair encUnary enc) (e.src, e.dst, e.constraint),
-    fun e f h => by
-      have h := (encPair encUnary (encPair encUnary enc)).injective h
-      exact Edge.ext (congrArg Prod.fst h) (congrArg (fun p => p.2.1) h)
-        (congrArg (fun p => p.2.2) h)⟩
-
-private theorem isPolyTime_toPair (enc : C ↪ List Bool) :
-    ComputableInPolyTime (fun e : Edge C => (e.src, e.dst, e.constraint))
-      (encoding enc) (encPair encUnary (encPair encUnary enc)) :=
-  .of_eq fun _ => rfl
-
-/-- Reading an edge's first endpoint is polynomial-time. -/
-@[fun_prop]
-theorem isPolyTime_src {edge : Input → Edge C}
-    (hedge : ComputableInPolyTime edge input (encoding enc)) :
-    ComputableInPolyTime (fun x => (edge x).src) input encUnary :=
-  (isPolyTime_toPair enc).fst'.comp hedge
-
-/-- Reading an edge's second endpoint is polynomial-time. -/
-@[fun_prop]
-theorem isPolyTime_dst {edge : Input → Edge C}
-    (hedge : ComputableInPolyTime edge input (encoding enc)) :
-    ComputableInPolyTime (fun x => (edge x).dst) input encUnary :=
-  (isPolyTime_toPair enc).snd'.fst'.comp hedge
-
-/-- Reading an edge's constraint descriptor is polynomial-time. -/
-@[fun_prop]
-theorem isPolyTime_constraint {edge : Input → Edge C}
-    (hedge : ComputableInPolyTime edge input (encoding enc)) :
-    ComputableInPolyTime (fun x => (edge x).constraint) input enc :=
-  (isPolyTime_toPair enc).snd'.snd'.comp hedge
-
-/-- Assemble computed endpoints and a computed constraint into an edge. -/
-@[fun_prop]
-theorem isPolyTime_mk {Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool}
-    {src dst : Input → ℕ} {constraint : Input → C}
-    (hsrc : ComputableInPolyTime src input encUnary)
-    (hdst : ComputableInPolyTime dst input encUnary)
-    (hconstraint : ComputableInPolyTime constraint input enc) :
-    ComputableInPolyTime (fun x => Edge.mk (src x) (dst x) (constraint x))
-      input (encoding enc) :=
-  (hsrc.prod (hdst.prod hconstraint)).of_enc_eq fun _ => rfl
+global enc_structure encoding (enc : C ↪ List Bool) : Edge C where
+  src : encUnary, dst : encUnary, constraint : enc
 
 end Edge
 
@@ -128,39 +88,8 @@ namespace Graph
 variable {C α Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool}
 
 /-- The vertex count is unary and the edges use the standard framed list encoding. -/
-def encoding (enc : C ↪ List Bool) : Graph C ↪ List Bool :=
-  ⟨fun g => encPair encUnary (encList (Edge.encoding enc)) (g.vertices, g.edges),
-    fun g h heq => by
-      have heq := (encPair encUnary (encList (Edge.encoding enc))).injective heq
-      exact Graph.ext (congrArg Prod.fst heq) (congrArg Prod.snd heq)⟩
-
-private theorem isPolyTime_toPair (enc : C ↪ List Bool) :
-    ComputableInPolyTime (fun g : Graph C => (g.vertices, g.edges))
-      (encoding enc) (encPair encUnary (encList (Edge.encoding enc))) :=
-  .of_eq fun _ => rfl
-
-/-- Reading the declared vertex count is polynomial-time. -/
-@[fun_prop]
-theorem isPolyTime_vertices {graph : Input → Graph C}
-    (hgraph : ComputableInPolyTime graph input (encoding enc)) :
-    ComputableInPolyTime (fun x => (graph x).vertices) input encUnary :=
-  (isPolyTime_toPair enc).fst'.comp hgraph
-
-/-- Reading the edge list is polynomial-time. -/
-@[fun_prop]
-theorem isPolyTime_edges {graph : Input → Graph C}
-    (hgraph : ComputableInPolyTime graph input (encoding enc)) :
-    ComputableInPolyTime (fun x => (graph x).edges) input (encList (Edge.encoding enc)) :=
-  (isPolyTime_toPair enc).snd'.comp hgraph
-
-/-- Assemble a computed vertex count and edge list into a graph. -/
-@[fun_prop]
-theorem isPolyTime_mk {Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool}
-    {vertices : Input → ℕ} {edges : Input → List (Edge C)}
-    (hvertices : ComputableInPolyTime vertices input encUnary)
-    (hedges : ComputableInPolyTime edges input (encList (Edge.encoding enc))) :
-    ComputableInPolyTime (fun x => Graph.mk (vertices x) (edges x)) input (encoding enc) :=
-  (hvertices.prod hedges).of_enc_eq fun _ => rfl
+global enc_structure encoding (enc : C ↪ List Bool) : Graph C where
+  vertices : encUnary, edges : (encList (Edge.encoding enc))
 
 /-- All listed endpoints are among the declared vertices. -/
 def WellFormed (g : Graph C) : Prop :=
@@ -194,7 +123,7 @@ theorem isPolyTime_edgeAt {graph : Input → Graph C} {index : Input → ℕ}
     ComputableInPolyTime (fun x => (graph x).edgeAt fallback (index x))
       input (Edge.encoding enc) :=
   (ComputableInPolyTime.listGetD (encA := Edge.encoding enc)
-    (Edge.mk 0 0 fallback)).comp ((isPolyTime_edges hgraph).prod hindex)
+    (Edge.mk 0 0 fallback)).comp ((encoding_edges_polyTime hgraph).prod hindex)
 
 /-- Check a numbered edge against a list of labels. Both lookups are total, with explicit
 fallbacks; the correctness theorem applies to valid edge indices. -/
@@ -216,9 +145,9 @@ theorem isPolyTime_checkEdge {alphabet : α ↪ List Bool}
     ComputableInPolyTime
       (fun x => checkEdge eval fallback label (graph x) (labels x) (index x)) input encBool := by
   have hedge := isPolyTime_edgeAt hgraph hindex fallback
-  have hsrc := Edge.isPolyTime_src hedge
-  have hdst := Edge.isPolyTime_dst hedge
-  have hconstraint := Edge.isPolyTime_constraint hedge
+  have hsrc := Edge.encoding_src_polyTime hedge
+  have hdst := Edge.encoding_dst_polyTime hedge
+  have hconstraint := Edge.encoding_constraint_polyTime hedge
   exact heval.comp (hconstraint.prod
     (((ComputableInPolyTime.listGetD (encA := alphabet) label).comp (hlabels.prod hsrc)).prod
       ((ComputableInPolyTime.listGetD (encA := alphabet) label).comp (hlabels.prod hdst))))
diff --git a/Complexity/Computability/PCP/Encoded/Cloud.lean b/Complexity/Computability/PCP/Encoded/Cloud.lean
index 59f7a38f18..e6c05b9e6d 100644
--- a/Complexity/Computability/PCP/Encoded/Cloud.lean
+++ b/Complexity/Computability/PCP/Encoded/Cloud.lean
@@ -73,7 +73,7 @@ theorem isPolyTime_halfEdges {graph : Input → Graph C}
   have hrange : ComputableInPolyTime (fun x => List.range (graph x).edges.length)
       input (encList encUnary) :=
     ComputableInPolyTime.range.comp
-      ((ComputableInPolyTime.length_list (Edge.encoding enc)).comp (isPolyTime_edges hgraph))
+      ((ComputableInPolyTime.length_list (Edge.encoding enc)).comp (encoding_edges_polyTime hgraph))
   unfold halfEdges List.product
   exact ComputableInPolyTime.flatMapWithInput hrange
     (ComputableInPolyTime.mapWithInput
@@ -92,7 +92,7 @@ theorem isPolyTime_endpoint {graph : Input → Graph C} {halfEdge : Input → 
       input encUnary := by
   have hedge := isPolyTime_edgeAt hgraph hhalfEdge.fst' fallback
   unfold endpoint
-  exact hhalfEdge.snd'.ite (Edge.isPolyTime_dst hedge) (Edge.isPolyTime_src hedge)
+  exact hhalfEdge.snd'.ite (Edge.encoding_dst_polyTime hedge) (Edge.encoding_src_polyTime hedge)
 
 /-- Cloud enumeration charges each endpoint lookup and the entire filtered output. -/
 @[fun_prop]
diff --git a/Complexity/Computability/PCP/Encoded/GenericComposition.lean b/Complexity/Computability/PCP/Encoded/GenericComposition.lean
index 5e67d2b7a0..a4de7da1a7 100644
--- a/Complexity/Computability/PCP/Encoded/GenericComposition.lean
+++ b/Complexity/Computability/PCP/Encoded/GenericComposition.lean
@@ -155,14 +155,14 @@ theorem isPolyTime_composeEdge [Fintype α] [Finite I] [Finite P] [Finite R] [Fi
       (encPair (encPi (encPi encBool)) (encPair coinsEncoding queryEncoding))
       (encFinite ((Fin 2 × I) ⊕ P)) := .of_finite _
   have hposition' := hposition.comp
-    ((Edge.isPolyTime_constraint hedge).prod (hcoins.prod hquery))
-  have hdst' := isPolyTime_composePosition number hindex (Edge.isPolyTime_src hedge)
-    (Edge.isPolyTime_dst hedge) hposition'
-  exact Edge.isPolyTime_mk
+    ((Edge.encoding_constraint_polyTime hedge).prod (hcoins.prod hquery))
+  have hdst' := isPolyTime_composePosition number hindex (Edge.encoding_src_polyTime hedge)
+    (Edge.encoding_dst_polyTime hedge) hposition'
+  exact Edge.encoding_mk_polyTime
     (ComputableInPolyTime.unary_add.comp
       ((ComputableInPolyTime.unary_mul.comp (hindex.prod (.const width))).prod
         (hnumber.comp hcoins))) hdst'
-    ((Edge.isPolyTime_constraint hedge).prod (hcoins.prod hquery))
+    ((Edge.encoding_constraint_polyTime hedge).prod (hcoins.prod hquery))
 
 /-- The verifier's edge predicate charges all supplied finite tables and query answers. -/
 @[fun_prop]
diff --git a/Complexity/Computability/PCP/Encoded/Power.lean b/Complexity/Computability/PCP/Encoded/Power.lean
index ca8e1c9acd..cff0a6fbb0 100644
--- a/Complexity/Computability/PCP/Encoded/Power.lean
+++ b/Complexity/Computability/PCP/Encoded/Power.lean
@@ -230,7 +230,7 @@ private theorem polytime_powerPreprocessEdge (eval : C → α → α → Bool) (
   have hrel := RegularConstraintGraph.isPolyTime_powerRelationWithInput
     hr he T q (encFinEnum (Fin q))
   unfold powerPreprocessEdge
-  refine Edge.isPolyTime_mk ?_ ?_ ?_
+  refine Edge.encoding_mk_polyTime ?_ ?_ ?_
   · fun_prop
   · exact isPolyTime_halfEdgeNumber.comp hwalk.fst'
   · apply pi
@@ -259,7 +259,7 @@ private theorem polytime_powerPreprocess (eval : C → α → α → Bool) (fall
     unfold List.product
     fun_prop
   unfold powerPreprocess
-  refine isPolyTime_mk ?_ ?_
+  refine encoding_mk_polyTime ?_ ?_
   · fun_prop
   · exact mapWithInput hdarts hedge
 
diff --git a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean
index 192df8ef41..6f0d919625 100644
--- a/Complexity/Computability/PCP/Encoded/ThreeSAT.lean
+++ b/Complexity/Computability/PCP/Encoded/ThreeSAT.lean
@@ -109,7 +109,7 @@ theorem isPolyTime_cnfEdge :
   have hliteral := ComputableInPolyTime.getElem? (encA := encPair encUnary encBool)
     hclause (hindex.comp ((snd _ _).snd'))
   unfold cnfEdge
-  refine Edge.isPolyTime_mk (by fun_prop) (by fun_prop) ?_
+  refine Edge.encoding_mk_polyTime (by fun_prop) (by fun_prop) ?_
   refine pi fun a => pi fun b => ?_
   have ha : ComputableInPolyTime a (encFinEnum (Fin 3)) encBool := .of_finite _
   fun_prop
diff --git a/Complexity/Computability/PCP/Encoded/Verifier/Repetition.lean b/Complexity/Computability/PCP/Encoded/Verifier/Repetition.lean
index 75b1c29e18..df952ee040 100644
--- a/Complexity/Computability/PCP/Encoded/Verifier/Repetition.lean
+++ b/Complexity/Computability/PCP/Encoded/Verifier/Repetition.lean
@@ -142,7 +142,7 @@ theorem polyTime_repeatedEdgeVerifier (width repeats : ℕ) (decode : (Fin width
   have hclog : ComputableInPolyTime (fun g : Graph C => (edgeVerifier width decode eval).coins g)
       (encoding enc) encUnary :=
     (ComputableInPolyTime.unary_clog_const 2).comp
-      ((ComputableInPolyTime.length_list (Edge.encoding enc)).comp (isPolyTime_edges .id'))
+      ((ComputableInPolyTime.length_list (Edge.encoding enc)).comp (encoding_edges_polyTime .id'))
   refine ⟨?_, ?_, ?_⟩
   · exact ComputableInPolyTime.unary_to_binary.comp
       (ComputableInPolyTime.unary_mul.comp ((ComputableInPolyTime.const repeats).prod hclog))
diff --git a/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean b/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean
index fa922b66ab..3b5b0b1ef3 100644
--- a/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean
+++ b/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Hybrid.Sequence
 public import Complexity.Crypto.Computational.Prediction
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 import Complexity.Computability.Probabilistic.CoinTape
 import Complexity.Tactic.PPT
 
@@ -70,16 +71,8 @@ structure Description where
 namespace Description
 
 /-- Encode a description using the shared pair representation. -/
-def encoding : Description ↪ List Bool :=
-  ⟨fun desc => encPair encBool
-    (encPair encBool (encPair encBits (encPair encBits encBits)))
-      (desc.active, desc.trial, desc.front, desc.back, desc.coins), by
-    intro left right h
-    have hfields := (encPair encBool
-      (encPair encBool (encPair encBits (encPair encBits encBits)))).injective h
-    cases left
-    cases right
-    simpa using hfields⟩
+enc_structure encoding : Description where
+  active : encBool, trial : encBool, front : encBits, back : encBits, coins : encBits
 
 /-- Decode any word. Missing or malformed fields use the total pair projections. -/
 def decode (code : List Bool) : Description where
@@ -91,15 +84,14 @@ def decode (code : List Bool) : Description where
 
 @[simp] theorem decode_encoding (desc : Description) : decode (encoding desc) = desc := by
   cases desc
-  simp only [decode, encoding, Function.Embedding.coeFn_mk, encPair_apply,
-    unframe_frame_append, dropFrame_frame_append, encBool_apply, List.headD_cons,
-    encBits, Function.Embedding.refl_apply]
+  simp only [decode, encoding_apply, encPair_apply, unframe_frame_append, dropFrame_frame_append,
+    encBool_apply, List.headD_cons, encBits, Function.Embedding.refl_apply]
 
 @[simp] theorem length_encoding (desc : Description) :
     (encoding desc).length =
       2 * (desc.front.length + desc.back.length) + desc.coins.length + 8 := by
-  simp only [encoding, Function.Embedding.coeFn_mk, length_encPair, encBool_apply,
-    List.length_singleton, encBits, Function.Embedding.refl_apply]
+  simp only [encoding_apply, length_encPair, encBool_apply, List.length_singleton, encBits,
+    Function.Embedding.refl_apply]
   lia
 
 /-- Insert a labeled example directly into the saved encoded input. -/
@@ -150,7 +142,7 @@ theorem isPPTOn_save {Param : Type} {input : Param ↪ List Bool}
     (hwidth : ComputableInPolyTime width input encUnary)
     (htrial : ComputableInPolyTime trial input encBool) :
     IsPPTOn input encBits (fun a => save c d (width a) (trial a) (front a) (back a)) := by
-  simp only [save, coinBudget, Description.encoding, Function.Embedding.coeFn_mk]
+  simp only [save, coinBudget, Description.encoding_apply]
   ppt
 
 attribute [program_certificate] isPPTOn_save
@@ -428,7 +420,8 @@ theorem isPPTOn_sample {Param : Type} {input : Param ↪ List Bool} {output : α
   have hbase := hbase.tidy
   have hcount := hcount.tidy
   have hwidth := hwidth.tidy
-  unfold sample Description.encoding
+  unfold sample
+  simp only [Description.encoding_apply]
   ppt
 
 attribute [program_certificate hreplacement] isPPTOn_sample
diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Program.lean b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Program.lean
index 5942dc9871..8c5c732756 100644
--- a/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Program.lean
+++ b/Complexity/Crypto/Computational/Pseudoentropy/Boosting/Program.lean
@@ -13,6 +13,7 @@ import Complexity.Computability.Probabilistic.Adaptive
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Tactic.PPT
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 
 /-!
 # A clocked hard-core boosting program
@@ -63,15 +64,10 @@ structure State where
 namespace State
 
 /-- Reuse the standard Boolean, unary, and list encodings. -/
-def encoding : State ↪ List Bool :=
-  ⟨fun state => encPair encBool (encPair encUnary (encList encBits))
-    (state.stopped, state.threshold, state.predictors), by
-    intro left right h
-    have hfields := (encPair encBool
-      (encPair encUnary (encList encBits))).injective h
-    cases left
-    cases right
-    simpa using hfields⟩
+global enc_structure encoding : State where
+  stopped : encBool, threshold : encUnary, predictors : (encList encBits)
+
+attribute [program_certificate] encoding_mk_polyTime
 
 /-- Start before any learned predictors or threshold shifts. -/
 def initial : State := ⟨false, 0, []⟩
@@ -104,8 +100,8 @@ def add (state : State) (bound : ℕ) (code : List Bool) : State :=
 @[simp] theorem length_encoding (state : State) :
     (encoding state).length = 2 * state.threshold +
       (encList encBits state.predictors).length + 4 := by
-  simp only [encoding, Function.Embedding.coeFn_mk, length_encPair, encBool_apply,
-    List.length_singleton, encUnary_apply, List.length_replicate]
+  simp only [encoding_apply, length_encPair, encBool_apply, List.length_singleton, encUnary_apply,
+    List.length_replicate]
   lia
 
 /-- After `rounds` rounds there are at most that many shifts and bounded descriptions. -/
@@ -154,47 +150,6 @@ section Efficiency
 
 variable {α : Type} {input : α ↪ List Bool} {state : α → State}
 
-private theorem isPolyTime_fields
-    (hstate : ComputableTidilyInPolyTime state input encoding) :
-    ComputableTidilyInPolyTime
-      (fun a => ((state a).stopped, (state a).threshold, (state a).predictors))
-      input (encPair encBool (encPair encUnary (encList encBits))) :=
-  hstate.of_enc_eq (fun _ => rfl)
-
-/-- Efficient field values construct an efficient state. -/
-@[program_certificate]
-theorem isPolyTime_mk {stopped : α → Bool} {threshold : α → ℕ}
-    {predictors : α → List (List Bool)}
-    (hstopped : ComputableInPolyTime stopped input encBool)
-    (hthreshold : ComputableInPolyTime threshold input encUnary)
-    (hpredictors : ComputableInPolyTime predictors input (encList encBits)) :
-    ComputableInPolyTime (fun a => ⟨stopped a, threshold a, predictors a⟩) input encoding := by
-  have hstopped := hstopped.tidy
-  have hthreshold := hthreshold.tidy
-  have hpredictors := hpredictors.tidy
-  exact .of_tidy ((hstopped.prod (hthreshold.prod hpredictors)).of_enc_eq (fun _ => rfl))
-
-/-- Project the stopping flag through the shared pair implementation. -/
-@[fun_prop]
-theorem isPolyTime_stopped (hstate : ComputableInPolyTime state input encoding) :
-    ComputableInPolyTime (fun a => (state a).stopped) input encBool := by
-  have hstate := hstate.tidy
-  exact .of_tidy ((isPolyTime_fields hstate).fst')
-
-/-- Project the threshold through the shared pair implementation. -/
-@[fun_prop]
-theorem isPolyTime_threshold (hstate : ComputableInPolyTime state input encoding) :
-    ComputableInPolyTime (fun a => (state a).threshold) input encUnary := by
-  have hstate := hstate.tidy
-  exact .of_tidy ((isPolyTime_fields hstate).snd'.fst')
-
-/-- Project the predictor collection through the shared pair implementation. -/
-@[fun_prop]
-theorem isPolyTime_predictors (hstate : ComputableInPolyTime state input encoding) :
-    ComputableInPolyTime (fun a => (state a).predictors) input (encList encBits) := by
-  have hstate := hstate.tidy
-  exact .of_tidy ((isPolyTime_fields hstate).snd'.snd')
-
 attribute [local fun_prop] ComputableInPolyTime.tidy in
 /-- Evaluating a list of descriptions is an ordinary captured map. -/
 @[program_certificate]
@@ -252,86 +207,11 @@ structure Parameters where
 namespace Parameters
 
 /-- Store all five resource parameters in unary using the shared product encoding. -/
-def encoding : Parameters ↪ List Bool :=
-  ⟨fun params => encPair encUnary (encPair encUnary
-      (encPair encUnary (encPair encUnary encUnary)))
-    (params.confidence, params.densityNumerator, params.densityBound,
-      params.rateBound, params.codeBound), by
-    intro left right h
-    have hfields := (encPair encUnary (encPair encUnary
-      (encPair encUnary (encPair encUnary encUnary)))).injective h
-    cases left
-    cases right
-    simpa using hfields⟩
-
-section Efficiency
-
-variable {α : Type} {input : α ↪ List Bool} {params : α → Parameters}
-
-private theorem isPolyTime_fields
-    (hparams : ComputableTidilyInPolyTime params input encoding) :
-    ComputableTidilyInPolyTime (fun a =>
-      ((params a).confidence, (params a).densityNumerator, (params a).densityBound,
-        (params a).rateBound, (params a).codeBound))
-      input (encPair encUnary
-        (encPair encUnary (encPair encUnary (encPair encUnary encUnary)))) :=
-  hparams.of_enc_eq (fun _ => rfl)
+global enc_structure encoding : Parameters where
+  confidence : encUnary, densityNumerator : encUnary, densityBound : encUnary,
+  rateBound : encUnary, codeBound : encUnary
 
-/-- Computing the five fields suffices to construct the encoded parameter record. -/
-@[program_certificate]
-theorem isPolyTime_mk {confidence densityNumerator densityBound rateBound codeBound : α → ℕ}
-    (hconfidence : ComputableInPolyTime confidence input encUnary)
-    (hdensityNumerator : ComputableInPolyTime densityNumerator input encUnary)
-    (hdensityBound : ComputableInPolyTime densityBound input encUnary)
-    (hrateBound : ComputableInPolyTime rateBound input encUnary)
-    (hcodeBound : ComputableInPolyTime codeBound input encUnary) :
-    ComputableInPolyTime (fun a =>
-      ⟨confidence a, densityNumerator a, densityBound a, rateBound a, codeBound a⟩)
-      input encoding := by
-  have hconfidence := hconfidence.tidy
-  have hdensityNumerator := hdensityNumerator.tidy
-  have hdensityBound := hdensityBound.tidy
-  have hrateBound := hrateBound.tidy
-  have hcodeBound := hcodeBound.tidy
-  exact .of_tidy ((hconfidence.prod (hdensityNumerator.prod
-    (hdensityBound.prod (hrateBound.prod hcodeBound)))).of_enc_eq (fun _ => rfl))
-
-/-- Project the confidence through the shared product implementation. -/
-@[fun_prop]
-theorem isPolyTime_confidence (hparams : ComputableInPolyTime params input encoding) :
-    ComputableInPolyTime (fun a => (params a).confidence) input encUnary := by
-  have hparams := hparams.tidy
-  exact .of_tidy ((isPolyTime_fields hparams).fst')
-
-/-- Project the density numerator through the shared product implementation. -/
-@[fun_prop]
-theorem isPolyTime_densityNumerator (hparams : ComputableInPolyTime params input encoding) :
-    ComputableInPolyTime (fun a => (params a).densityNumerator) input encUnary := by
-  have hparams := hparams.tidy
-  exact .of_tidy ((isPolyTime_fields hparams).snd'.fst')
-
-/-- Project the density parameter through the shared product implementation. -/
-@[fun_prop]
-theorem isPolyTime_densityBound (hparams : ComputableInPolyTime params input encoding) :
-    ComputableInPolyTime (fun a => (params a).densityBound) input encUnary := by
-  have hparams := hparams.tidy
-  exact .of_tidy ((isPolyTime_fields hparams).snd'.snd'.fst')
-
-/-- Project the rate parameter through the shared product implementation. -/
-@[fun_prop]
-theorem isPolyTime_rateBound (hparams : ComputableInPolyTime params input encoding) :
-    ComputableInPolyTime (fun a => (params a).rateBound) input encUnary := by
-  have hparams := hparams.tidy
-  exact .of_tidy ((isPolyTime_fields hparams).snd'.snd'.snd'.fst')
-
-/-- Project the description bound through the shared product implementation. -/
-@[fun_prop]
-theorem isPolyTime_codeBound (hparams : ComputableInPolyTime params input encoding) :
-    ComputableInPolyTime (fun a => (params a).codeBound) input encUnary := by
-  have hparams := hparams.tidy
-  exact .of_tidy ((isPolyTime_fields hparams).snd'.snd'.snd'.snd')
-
-end Efficiency
+attribute [program_certificate] encoding_mk_polyTime
 
 /-- The density denominator is a positive power of two. -/
 def denominator (params : Parameters) : ℕ := dyadicSize params.densityBound
@@ -471,7 +351,7 @@ theorem isPPTOn_run {α : Type} {input : α ↪ List Bool} {evaluate : List Bool
   have hclock : ComputableTidilyInPolyTime (fun a => (params a).clock) input encUnary := by
     unfold Parameters.clock Parameters.inverseRate Parameters.denominator
     polytime
-  have hcode := (Parameters.isPolyTime_codeBound (.of_tidy hparams)).tidy
+  have hcode := (Parameters.encoding_codeBound_polyTime (.of_tidy hparams)).tidy
   refine (IsPPTOn.iterateWith_spec (stateEncoding := State.encoding)
     (initial := fun _ => State.initial)
     (step := fun a => round evaluate (source a) (learn a) (params a))
diff --git a/ComplexityTests/HPVIntervalCount.lean b/ComplexityTests/HPVIntervalCount.lean
index 941665f2d2..9c8cb83700 100644
--- a/ComplexityTests/HPVIntervalCount.lean
+++ b/ComplexityTests/HPVIntervalCount.lean
@@ -75,7 +75,7 @@ example : MultiTapeTM.ComputableInPolyTime (fun x : List Bool =>
       fun h => windowCells 2 (w₁ h)⟩ : IntervalData 1 Bool).count walk)
     MultiTapeTM.encBits MultiTapeTM.encUnary :=
   computableInPolyTime_localIntervalCount walk
-    (IntervalData.computableInPolyTime_mk MultiTapeTM.ComputableInPolyTime.id'
+    (encIntervalData_mk_polyTime MultiTapeTM.ComputableInPolyTime.id'
       (.const _) (.const _) (.const _) (.const _) (.const _) (.const _) (.const _))
     (size := fun _ => 20) (Cslib.PolynomiallyBounded.const 20) fun _ => by norm_num
 
diff --git a/ComplexityTests/StructureEncoding.lean b/ComplexityTests/StructureEncoding.lean
new file mode 100644
index 0000000000..77d2ba5d5f
--- /dev/null
+++ b/ComplexityTests/StructureEncoding.lean
@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Finite
+
+/-! Tests of `enc_structure`. -/
+
+namespace ComplexityTests.StructureEncoding
+
+open Turing.MultiTapeTM
+
+/-- A structure with fields of different encodings. -/
+structure Point where
+  /-- A binary number. -/
+  x : ℕ
+  /-- A bit string. -/
+  y : List Bool
+  /-- A list of unary numbers. -/
+  z : List ℕ
+
+/-- Points, as their fields. -/
+enc_structure ePoint : Point where x : encNat, y : encBits, z : (encList encUnary)
+
+/-! The encoding unfolds to the tuple, and the encoding is injective by construction. -/
+
+example (p : Point) : ePoint p = ePointFields (p.x, p.y, p.z) := ePoint_apply p
+example {p q : Point} (h : ePoint p = ePoint q) : p = q := ePoint.injective h
+
+/-! The rules assemble programs over the fields, at each level of the calculus. -/
+
+example : ComputableInDegree (fun p : Point => Point.mk p.x p.y p.z) ePoint ePoint 1 1 := by
+  fun_prop (disch := lia)
+
+-- Reading fields and rebuilding the structure, with the bounds checked once.
+example : ComputableInO (fun p : Point => Point.mk p.x p.y p.z) ePoint ePoint
+    (fun p => 8 * ((ePoint p).length + 1)) fun p => 8 * ((ePoint p).length + 1) := by
+  refine .mono (by fun_prop) 16 (fun p => ?_) fun p => ?_ <;>
+  · simp only [ePoint_apply, length_encPair]
+    omega
+
+example {α : Type} {input : α ↪ List Bool} {p : α → Point}
+    (hp : ComputableInPolyTime p input ePoint) :
+    ComputableInPolyTime (fun a => Point.mk (p a).x (p a).y (p a).z) input ePoint := by
+  fun_prop
+
+/-- A parametric structure. -/
+structure Tagged (C : Type) where
+  /-- A unary tag. -/
+  tag : ℕ
+  /-- The payload. -/
+  payload : C
+
+namespace Tagged
+
+/-! An explicit binder stays an explicit argument of the encoding. -/
+
+/-- Tagged values, with the encoding of the payload as a parameter. -/
+enc_structure encoding {C : Type} (enc : C ↪ List Bool) : Tagged C where
+  tag : encUnary, payload : enc
+
+end Tagged
+
+example {C : Type} (enc : C ↪ List Bool) (t : Tagged C) :
+    Tagged.encoding enc t = Tagged.encodingFields enc (t.tag, t.payload) := rfl
+
+section
+
+open scoped Tagged
+
+-- The rules are available outside the namespace after `open scoped`.
+example {α C : Type} {input : α ↪ List Bool} {enc : C ↪ List Bool} {t : α → Tagged C}
+    (ht : ComputableInPolyTime t input (Tagged.encoding enc)) :
+    ComputableInPolyTime (fun a => (t a).payload) input enc := by
+  fun_prop
+
+end
+
+/-- A structure in a public API. -/
+structure Labelled where
+  /-- A unary label. -/
+  label : ℕ
+
+/-- Labelled values, with rules available everywhere. -/
+global enc_structure encLabelled : Labelled where label : encUnary
+
+end ComplexityTests.StructureEncoding
+
+namespace ComplexityTests
+
+-- Outside the namespace, without `open scoped`.
+example {α : Type} {input : α ↪ List Bool} {l : α → StructureEncoding.Labelled}
+    (hl : Turing.MultiTapeTM.ComputableInPolyTime l input StructureEncoding.encLabelled) :
+    Turing.MultiTapeTM.ComputableInPolyTime (fun a => StructureEncoding.Labelled.mk (l a).label)
+      input StructureEncoding.encLabelled := by
+  fun_prop
+
+end ComplexityTests
+
+namespace ComplexityTests.StructureEncoding
+
+open Turing.MultiTapeTM
+
+/-! An encoding built from noncomputable parts is declared as such. -/
+
+/-- A pair of a finite value and a number. -/
+structure FinitePart (α : Type) where
+  /-- The finite value. -/
+  value : α
+  /-- The number. -/
+  count : ℕ
+
+/-- Finite parts, with the value by its rank. -/
+noncomputable enc_structure encFinitePart {α : Type} [Finite α] : FinitePart α where
+  value : (encFinite α), count : encUnary
+
+end ComplexityTests.StructureEncoding