diff --git a/Complexity/Algorithms/Reachability/ReingoldEval.lean b/Complexity/Algorithms/Reachability/ReingoldEval.lean
index 3fc8581fa..ccdaa0ca3 100644
--- a/Complexity/Algorithms/Reachability/ReingoldEval.lean
+++ b/Complexity/Algorithms/Reachability/ReingoldEval.lean
@@ -128,7 +128,7 @@ theorem reingoldStep_rot {V : Type*} (G : RotationMap V B) (y : V) (c a : B) :
       ((r₂.1, s₄.1), reingoldFinish e s₄.2) := by
   simp only [reingoldStep, rot_relabel, reingoldHStep, reingoldFinish, Equiv.apply_symm_apply]
   change Prod.map id e.symm (powRot (G.zigzag H).rot 2 ((y, c), e.symm.symm a)) = _
-  simp only [powRot, Equiv.symm_symm, zigzag, zigzagRot, Fin.tail, Prod.map_apply, id_eq]
+  simp only [powRot, Equiv.symm_symm, zigzagRot, Fin.tail, Prod.map_apply, id_eq]
   refine Prod.ext rfl (congrArg e.symm (funext fun i ↦ ?_))
   fin_cases i <;> simp [Matrix.cons_val_zero, Matrix.cons_val_one, Fin.snoc]
 
diff --git a/Complexity/Computability/Complexity/CookLevin/Parameters.lean b/Complexity/Computability/Complexity/CookLevin/Parameters.lean
index 0bf9c3539..8b71f391b 100644
--- a/Complexity/Computability/Complexity/CookLevin/Parameters.lean
+++ b/Complexity/Computability/Complexity/CookLevin/Parameters.lean
@@ -45,7 +45,8 @@ open Turing.MultiTapeTM
 
 /-- The input prefix, certificate length and verifier time bound used by the Cook–Levin
 reduction are jointly computable in polynomial time, with the bounds in unary. -/
-@[fun_prop]
+-- The reducible tuple is handled by compositional rules. Registering this certificate would
+-- index its specialized formula under `Prod.mk` and interfere with unrelated tuple clients.
 theorem computableInPolyTime_parameters {α : Type} (p : Polynomial ℕ) (c d : ℕ)
     (enc : α ↪ List Bool) :
     ComputableInPolyTime (parameters p c d enc)
diff --git a/Complexity/Computability/Complexity/CookLevin/Reduction.lean b/Complexity/Computability/Complexity/CookLevin/Reduction.lean
index 77a3af708..2c5271405 100644
--- a/Complexity/Computability/Complexity/CookLevin/Reduction.lean
+++ b/Complexity/Computability/Complexity/CookLevin/Reduction.lean
@@ -111,7 +111,9 @@ theorem Var.index_injective : Function.Injective (Var.index (k := k) (State := S
 variable [DecidableEq State] {α : Type}
 
 /-- The framed input prefix, certificate length and verifier time bound supplied to the tableau.
-The verifier is allowed `c * (n + 1) ^ d` steps on an input of encoded length `n`. -/
+The verifier is allowed `c * (n + 1) ^ d` steps on an input of encoded length `n`.
+The tuple wrapper is reducible so projection clients can compute its components directly. -/
+@[reducible]
 def parameters (p : Polynomial ℕ) (c d : ℕ) (enc : α ↪ List Bool) (a : α) :
     List Bool × ℕ × ℕ :=
   (frame (enc a), p.eval (enc a).length,
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean
index 247f87ef4..587bf13be 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean
@@ -21,6 +21,13 @@ Tensor and zig-zag rotations are straight-line programs calling their constituen
 Their certificates charge the complete vertex and edge-label encodings, including copying and
 intermediate pairs. The affine-plane rotation similarly composes multiplication and subtraction.
 
+The structure wrappers `RotationMap.tensor`, `RotationMap.zigzag`, `RotationMap.affinePlane`,
+`RotationMap.contract` and `RotationMap.reindex` are reducible. Thus `fun_prop` sees the distinct
+certified rotation programs beneath their `.rot` projections, including in larger compositions.
+Default `simp` also exposes the corresponding `tensorRot`, `zigzagRot`, `affinePlaneRot`,
+`contractRot` and `reindexRot` forms; the `rot_*` equations remain available for `rw` and
+applicable explicit `simp only` proofs.
+
 These rules certify a rotation call. They do not enumerate a graph or certify an unbounded
 recursive tower. In particular, a certificate for a fixed finite base is not a uniform efficiency
 theorem for a varying field size or tower depth.
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean
index 9303742e8..d6f3999da 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean
@@ -188,7 +188,7 @@ theorem lookup_iterate_numbered {B : Type*} (H : RotationMap B D)
     rw [Function.iterate_zero_apply]
     change (initial (H.reindex numbering)).lookup (numbering vertex).val label = _
     rw [lookup_initial]
-    simp only [rot_reindex, Equiv.symm_apply_apply]
+    simp only [reindexRot, Equiv.symm_apply_apply]
     rfl
   | succ level ih =>
     rcases vertex with ⟨vertex, cloud⟩
@@ -213,10 +213,10 @@ theorem lookup_iterate_numbered {B : Type*} (H : RotationMap B D)
           (ZigzagTowerVertex.equivFin numbering level vertex).val := by
       rw [Nat.mul_comm (ZigzagTowerVertex.equivFin numbering level vertex).val,
         Nat.mul_add_div hb, Nat.div_eq_of_lt (numbering cloud).isLt, Nat.add_zero]
-    simp only [nextRow, hmod, hdiv, rot_reindex, Equiv.trans_apply, Fin.eta,
+    simp only [nextRow, hmod, hdiv, reindexRot, Equiv.trans_apply, Fin.eta,
       Equiv.symm_apply_apply, Equiv.symm_trans_apply, Equiv.apply_symm_apply]
     rw [ih, ih]
-    simp only [rot_zigzagTower_succ, rot_zigzag, square_relabel_rotation, hstep]
+    simp only [rot_zigzagTower_succ, zigzagRot, square_relabel_rotation, hstep]
 
 /-- The selected complete table has the exact cardinality used by the tower family. -/
 theorem length_build (H : RotationMap (Fin b) D) (e : Fin b ≃ (Fin 2 → D × D))
@@ -232,7 +232,7 @@ theorem lookup_build {B : Type*} (H : RotationMap B D) (e : B ≃ (Fin 2 → D 
       let target := ((zigzagTower H e (Nat.clog b size - 1)).reindex
         (ZigzagTowerVertex.equivFin numbering (Nat.clog b size - 1))).rot (vertex, label)
       (target.1.val, target.2) := by
-  simpa only [build, Equiv.apply_symm_apply, rot_reindex] using
+  simpa only [build, Equiv.apply_symm_apply, reindexRot] using
     lookup_iterate_numbered H e numbering hb (Nat.clog b size - 1)
       ((ZigzagTowerVertex.equivFin numbering (Nat.clog b size - 1)).symm vertex) label
 
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
index e96823c50..9dd5afd22 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
@@ -79,7 +79,7 @@ theorem contract_eq {m n : ℕ} (G : RotationMap (Fin m) (D × D))
       if hindex : vertex.val + n * label.1.val < m then
         some (⟨vertex.val + n * label.1.val, hindex⟩ : Fin m) else none := rfl
   unfold contract contractFin
-  simp only [rot_contract, hdecode, hlength]
+  simp only [contractRot, hdecode, hlength]
   split <;> rename_i hindex
   · simp only [hlookup ⟨vertex.val + n * label.1.val, hindex⟩ label.2]
     simp only [contractDart, finSlotEncode]
diff --git a/Complexity/Computability/PCP/Encoded/Preprocess.lean b/Complexity/Computability/PCP/Encoded/Preprocess.lean
index ccaa13855..0a292f54d 100644
--- a/Complexity/Computability/PCP/Encoded/Preprocess.lean
+++ b/Complexity/Computability/PCP/Encoded/Preprocess.lean
@@ -249,7 +249,7 @@ private theorem rotationEdges_represents {V : Type} (vertices : ℕ)
     change (rotate (vertices, (eV.symm p.1).val, p.2)).1 = _
     rw [hrotate]
     simp [RegularConstraintGraph.toConstraintGraph, RegularConstraintGraph.unconstrained,
-      RotationMap.neighbor_def, hnumber]
+      RotationMap.neighbor_def, RotationMap.reindexRot, hnumber]
   · intro p a b
     simp [edge, htruth, RegularConstraintGraph.toConstraintGraph,
       RegularConstraintGraph.unconstrained]
@@ -318,7 +318,7 @@ theorem toGraph_preprocess [DecidableEq α] (htruth : ∀ a b, eval truth a b =
     (RotationMap.loops (Fin n) Unit) (fun _ _ => rfl) eV number hnumber
   have hreindex : (RotationMap.loops (Fin n) Unit).reindex eV =
       RotationMap.loops (Fin g.edges.length × Bool) Unit := by
-    ext p <;> simp
+    ext p <;> simp [RotationMap.reindexRot]
   have hloopedges : rotationEdges (fun p : ℕ × ℕ × Unit => p.2) [()] n =
       (List.range n).map (fun v => (v, v)) := by
     simp only [rotationEdges, List.map_cons, List.map_nil]
diff --git a/Complexity/Foundations/Combinatorics/Expander/AffinePlane.lean b/Complexity/Foundations/Combinatorics/Expander/AffinePlane.lean
index a68656263..cf2ab604f 100644
--- a/Complexity/Foundations/Combinatorics/Expander/AffinePlane.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/AffinePlane.lean
@@ -56,6 +56,7 @@ def affinePlaneRot (p : (K × K) × K) : (K × K) × K :=
 
 /-- The affine-plane graph: `(a, b)` is adjacent to `(c, d)` when `a * c = b + d`.
 The edge to first coordinate `c` has label `c`, and its reverse has label `a`. -/
+@[reducible]
 def affinePlane : RotationMap (K × K) K where
   rot := affinePlaneRot K
   rot_involutive p := by
diff --git a/Complexity/Foundations/Combinatorics/Expander/Contraction.lean b/Complexity/Foundations/Combinatorics/Expander/Contraction.lean
index 04fdca819..20bcc8e92 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Contraction.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Contraction.lean
@@ -75,6 +75,7 @@ theorem contractRot_contractDart (rotate : V × D → V × D) (p : V × D) :
   simp [contractRot, contractDart, h.eq]
 
 /-- Contract the occupied slots over each vertex, completing the degree with self-loops. -/
+@[reducible]
 def contract (G : RotationMap V D) : RotationMap W (I × D) where
   rot := contractRot encode decode G.rot
   rot_involutive := by
diff --git a/Complexity/Foundations/Combinatorics/Expander/Reindex.lean b/Complexity/Foundations/Combinatorics/Expander/Reindex.lean
index 582b1adef..f6fbea7b9 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Reindex.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Reindex.lean
@@ -48,6 +48,7 @@ def reindexRot (forward : V → W) (backward : W → V) (rotate : V × D → V 
   (forward next.1, next.2)
 
 /-- Rename the vertices of a graph, retaining every outgoing and return edge label. -/
+@[reducible]
 def reindex (G : RotationMap V D) (e : V ≃ W) : RotationMap W D where
   rot := reindexRot e e.symm G.rot
   rot_involutive p := by simp [reindexRot]
diff --git a/Complexity/Foundations/Combinatorics/Expander/Tensor.lean b/Complexity/Foundations/Combinatorics/Expander/Tensor.lean
index bf21386ce..626bc1d7b 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Tensor.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Tensor.lean
@@ -69,6 +69,7 @@ def tensorRot (rotate : V × D → V × D) (other : V' × D' → V' × D')
 [Reingold, Vadhan and Wigderson, Section 2.3][ReingoldVadhanWigderson2002]: the multigraph on
 `V × V'` with labels `D × D'` whose edge `(i, i')` at `(v, v')` takes the edge `i` of `G` at `v` and
 the edge `i'` of `H` at `v'` at the same time. -/
+@[reducible]
 def tensor : RotationMap (V × V') (D × D') where
   rot := tensorRot G.rot H.rot
   rot_involutive p := by simp [tensorRot]
diff --git a/Complexity/Foundations/Combinatorics/Expander/Zigzag.lean b/Complexity/Foundations/Combinatorics/Expander/Zigzag.lean
index 791537b11..ca4f68367 100644
--- a/Complexity/Foundations/Combinatorics/Expander/Zigzag.lean
+++ b/Complexity/Foundations/Combinatorics/Expander/Zigzag.lean
@@ -138,6 +138,7 @@ at `v`, grouped into the cloud `{v} × D` of `v`, and its labels are pairs of la
 `(i, j)` at `(v, k)` takes the edge `i` of `H` from `k` to `k'` inside the cloud ("zig"), crosses
 the `k'`-th edge of `G` from `v` to `(w, ℓ')`, where it is the `ℓ'`-th edge at `w`, and takes the
 edge `j` of `H` from `ℓ'` to `ℓ` inside the cloud of `w` ("zag"), ending at `(w, ℓ)`. -/
+@[reducible]
 def zigzag : RotationMap (V × D) (E × E) where
   rot := zigzagRot G.rot H.rot
   rot_involutive p := by simp [zigzagRot]
diff --git a/ComplexityTests/CookLevinPolyTime.lean b/ComplexityTests/CookLevinPolyTime.lean
index bb276330c..a7bd622fa 100644
--- a/ComplexityTests/CookLevinPolyTime.lean
+++ b/ComplexityTests/CookLevinPolyTime.lean
@@ -46,6 +46,12 @@ example {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] :
       (encPair (encPair (encPair encBits encUnary) encUnary) encUnary) encCNF := by
   fun_prop
 
+-- The full reducible tuple composes without a specialized `Prod.mk` search rule.
+example {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (c d : ℕ) :
+    ComputableInPolyTime (parameters p c d enc)
+      enc (encPair encBits (encPair encUnary encUnary)) := by
+  fun_prop
+
 -- The input encoding, polynomial and machine are fixed parameters of the reduction.
 example {k : ℕ} {State α : Type} [Fintype State]
     (tm : Turing.MultiTapeTM k Bool State) (enc : α ↪ List Bool)
diff --git a/ComplexityTests/ExpanderContraction.lean b/ComplexityTests/ExpanderContraction.lean
index 1bd9d7150..ac59474d9 100644
--- a/ComplexityTests/ExpanderContraction.lean
+++ b/ComplexityTests/ExpanderContraction.lean
@@ -68,7 +68,7 @@ example : ComputableInPolyTime threeVertices.rot
   have hg : ComputableInPolyTime completeFive.rot
       (encPair (encFinEnum (Fin 5)) (encFinEnum (Fin 5)))
       (encPair (encFinEnum (Fin 5)) (encFinEnum (Fin 5))) := .of_finite _
-  exact ComputableInPolyTime.rotationMap_contract he hd hg
+  fun_prop [threeVertices, RotationMap.contractFin]
 
 example {V W I D : Type} (G : RotationMap V D) (encode : V → W × I)
     (decode : W × I → Option V) (hinv : Function.IsPartialInv encode decode)
@@ -80,7 +80,6 @@ example {V W I D : Type} (G : RotationMap V D) (encode : V → W × I)
       (fun p : (W × (I × D)) × Bool => ((RotationMap.contract encode decode hinv G).rot p.1, !p.2))
       (encPair (encPair ew (encPair ei ed)) encBool)
       (encPair (encPair ew (encPair ei ed)) encBool) := by
-  dsimp only [RotationMap.contract, RotationMap.contractRot, RotationMap.contractDart]
   fail_if_success (clear he; fun_prop)
   fail_if_success (clear hd; fun_prop)
   fail_if_success (clear hg; fun_prop)
diff --git a/ComplexityTests/ExpanderFamily.lean b/ComplexityTests/ExpanderFamily.lean
index 51163712e..e8dcc9636 100644
--- a/ComplexityTests/ExpanderFamily.lean
+++ b/ComplexityTests/ExpanderFamily.lean
@@ -96,7 +96,6 @@ example {V W D : Type} (G : RotationMap V D) (e : V ≃ W)
         let next := (G.reindex e).rot p.1
         (next, !p.2))
       (encPair (encPair ew ed) encBool) (encPair (encPair ew ed) encBool) := by
-  dsimp only [RotationMap.reindex, RotationMap.reindexRot]
   fail_if_success (clear hf; fun_prop)
   fail_if_success (clear hb; fun_prop)
   fail_if_success (clear hg; fun_prop)
@@ -110,7 +109,7 @@ example (G : RotationMap (Bool × List Bool) Bool)
     ComputableInPolyTime (G.reindex (Equiv.prodComm Bool (List Bool))).rot
       (encPair (encPair encBits encBool) encBool)
       (encPair (encPair encBits encBool) encBool) := by
-  simp only [RotationMap.reindex, Equiv.prodComm, Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk]
+  simp only [Equiv.prodComm, Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk]
   fun_prop [Prod.swap]
 
 end ComplexityTests.ExpanderFamily
diff --git a/ComplexityTests/ExplicitExpanders.lean b/ComplexityTests/ExplicitExpanders.lean
index c8d706921..c9d29bf21 100644
--- a/ComplexityTests/ExplicitExpanders.lean
+++ b/ComplexityTests/ExplicitExpanders.lean
@@ -64,8 +64,7 @@ example {K : Type} [Field K] (encode : K ↪ List Bool)
     ComputableInPolyTime (RotationMap.affinePlaneTowerBase K).rot
       (encPair (baseEncoding encode) (planeEncoding encode))
       (encPair (baseEncoding encode) (planeEncoding encode)) := by
-  have hplane := ComputableInPolyTime.rotationMap_affinePlane hmul hsub
-  exact ((hplane.rotationMap_tensor hplane).rotationMap_zigzag hplane).rotationMap_zigzag hplane
+  fun_prop [RotationMap.affinePlaneTowerBase]
 
 -- Only the fixed field operations use the finite-domain theorem; graph products compose them.
 example (encode : ZMod 257 ↪ List Bool) :
@@ -76,8 +75,7 @@ example (encode : ZMod 257 ↪ List Bool) :
       (planeEncoding encode) encode := .of_finite _
   have hsub : ComputableInPolyTime (fun p : ZMod 257 × ZMod 257 => p.1 - p.2)
       (planeEncoding encode) encode := .of_finite _
-  have hplane := ComputableInPolyTime.rotationMap_affinePlane hmul hsub
-  exact ((hplane.rotationMap_tensor hplane).rotationMap_zigzag hplane).rotationMap_zigzag hplane
+  fun_prop [RotationMap.affinePlaneTowerBase]
 
 -- Equivalent direct and let-bound spellings, with a supplied rotation on an arbitrary type.
 example {V D E : Type} (G : RotationMap V D) (H : RotationMap D E)
@@ -88,7 +86,6 @@ example {V D E : Type} (G : RotationMap V D) (H : RotationMap D E)
       (fun p : ((V × D) × (E × E)) × Bool => ((G.zigzag H).rot p.1, !p.2))
       (encPair (encPair (encPair vertex label) (encPair small small)) encBool)
       (encPair (encPair (encPair vertex label) (encPair small small)) encBool) := by
-  dsimp only [RotationMap.zigzag, RotationMap.zigzagRot]
   fail_if_success (clear hG; fun_prop)
   fail_if_success (clear hH; fun_prop)
   fun_prop
@@ -103,7 +100,21 @@ example {V D E : Type} (G : RotationMap V D) (H : RotationMap D E)
         (next, !p.2))
       (encPair (encPair (encPair vertex label) (encPair small small)) encBool)
       (encPair (encPair (encPair vertex label) (encPair small small)) encBool) := by
-  dsimp only [RotationMap.zigzag, RotationMap.zigzagRot]
+  fun_prop
+
+-- Tensor and zig-zag wrappers must lead search to their distinct rotation programs.
+example {V D W E : Type} (G : RotationMap V D) (H : RotationMap W E)
+    (vertex : V ↪ List Bool) (label : D ↪ List Bool)
+    (otherVertex : W ↪ List Bool) (otherLabel : E ↪ List Bool)
+    (hG : ComputableInPolyTime G.rot (encPair vertex label) (encPair vertex label))
+    (hH : ComputableInPolyTime H.rot
+      (encPair otherVertex otherLabel) (encPair otherVertex otherLabel)) :
+    ComputableInPolyTime
+      (fun p : ((V × W) × (D × E)) × Bool => ((G.tensor H).rot p.1, !p.2))
+      (encPair (encPair (encPair vertex otherVertex) (encPair label otherLabel)) encBool)
+      (encPair (encPair (encPair vertex otherVertex) (encPair label otherLabel)) encBool) := by
+  fail_if_success (clear hG; fun_prop)
+  fail_if_success (clear hH; fun_prop)
   fun_prop
 
 end ComplexityTests.ExplicitExpanders
diff --git a/ComplexityTests/MultiTapePolyTime.lean b/ComplexityTests/MultiTapePolyTime.lean
index 8fde4c4a0..2042aace5 100644
--- a/ComplexityTests/MultiTapePolyTime.lean
+++ b/ComplexityTests/MultiTapePolyTime.lean
@@ -139,7 +139,6 @@ example {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (c d : ℕ) :
     ComputableTidilyInPolyTime
       (fun a => List.range (Cslib.Complexity.CookLevin.parameters p c d enc a).2.2)
       enc (encList encUnary) := by
-  dsimp only [Cslib.Complexity.CookLevin.parameters]
   fun_prop
 
 private def finish (move : SignType) (symbol : Bool) : Turing.MultiTapeTM 0 Bool Unit :=