From 2de39686a35d513b6b899b9c9fcef1cf6d2c7370 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 16:23:50 -0400 Subject: [PATCH 1/2] fix(automation): restore folded fun_prop clients on rc2 Expose six packaging definitions at reducible transparency so original rotation and Cook-Levin clients work with default fun_prop. Prune the resulting redundant parameters registration to keep specialized arithmetic out of generic tuple search. Restore the original client forms and guards, add tensor and full-parameters regressions, and repair affected proof reductions without changing statements, definition bodies, models or resource bounds. AI assistance: Codex worker codex-worker-fun-prop-1654 diagnosed, implemented and validated this layer under coordinator codex-coord-20261029-1732. All six scripts/check.sh gates and source checks passed on frozen rc2 parent bb3e910dfc197e46f4b11e0c666b6546a075b7c8. Curated abstracts and rendering are unaffected. --- .../Algorithms/Reachability/ReingoldEval.lean | 2 +- .../Complexity/CookLevin/Parameters.lean | 3 ++- .../Complexity/CookLevin/Reduction.lean | 4 +++- .../Complexity/PolyTime/RotationMap.lean | 4 ++++ .../PolyTime/RotationMap/TowerTable.lean | 8 +++---- .../RotationMap/TowerTable/Family.lean | 2 +- .../Computability/PCP/Encoded/Preprocess.lean | 4 ++-- .../Combinatorics/Expander/AffinePlane.lean | 1 + .../Combinatorics/Expander/Contraction.lean | 1 + .../Combinatorics/Expander/Reindex.lean | 1 + .../Combinatorics/Expander/Tensor.lean | 1 + .../Combinatorics/Expander/Zigzag.lean | 1 + ComplexityTests/CookLevinPolyTime.lean | 6 +++++ ComplexityTests/ExpanderContraction.lean | 3 +-- ComplexityTests/ExpanderFamily.lean | 3 +-- ComplexityTests/ExplicitExpanders.lean | 23 ++++++++++++++----- ComplexityTests/MultiTapePolyTime.lean | 1 - 17 files changed, 47 insertions(+), 21 deletions(-) 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..f1ecbe925 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean @@ -21,6 +21,10 @@ 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. + 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 := From c57307c8ffb3cb38ef21eb543a97f290ed8ca315 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 19:03:19 -0400 Subject: [PATCH 2/2] doc(automation): explain simp rotation normal forms Record that default simp exposes the functional Rot programs while the rotation equations remain usable through explicit rewrites. The reviewed automation layer is otherwise unchanged after restacking onto final pin 0d38523e96f8b431aeadc86c548c9994714f9b00. AI assistance: Codex worker codex-worker-fun-prop-1654 added this requested review note and verified the restack. All six scripts/check.sh gates, source hygiene, changed-file lints, tidy-surface checks and diff checks passed on this source. Curated abstracts, models and resource bounds are unaffected. --- .../Turing/MultiTape/Complexity/PolyTime/RotationMap.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean index f1ecbe925..587bf13be 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean @@ -24,6 +24,9 @@ intermediate pairs. The affine-plane rotation similarly composes multiplication 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