refactor(Universal): use plain description decoder certificates

Complexity/Computability/Complexity/Classes/Hierarchy.lean

@@ -269,10 +269,9 @@ theorem computableInO_diagonal :
       fun x => 2 ^ (2 * x.length) := by
   have this : ComputableTidilyInO diagonal encBits encBool (fun x => 2 ^ (4 * x.length))
       fun x => 2 ^ (2 * x.length) := by
-    obtain ⟨dd, ed, hdec⟩ := exists_computableTidilyInDegree_decodeDesc
-    have hu : ComputableTidilyInDegree unframe encBits encBits 1 1 :=
-      .of_linear (.of_unframe fun _ => rfl)
-    have hdesc := (hdec.comp hu).inO
+    obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc
+    have hu := Internal.DecoderWords.unframe_degree
+    have hdesc := (hdec.comp hu).inO.tidy
     have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one
     have hclock := (ComputableTidilyInDegree.two_pow_length encBits).inO_one
     have hpre := hdesc.prod (hsym.prod hclock)

Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean

@@ -120,10 +120,10 @@ space linear in the description, the budget and the lengths of the clock and of
 theorem computableInO_spaceDiagonal {G : ℕ → ℕ} (hG : SpaceConstructible G) :
     ∃ T, ComputableInO (spaceDiagonal G) encBits encBool T
       fun x => x.length + G x.length := by
-  obtain ⟨dd, ed, hdec⟩ := exists_computableTidilyInDegree_decodeDesc
+  obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc
   have hu : ComputableInO unframe encBits encBits (fun x => x.length) fun x => x.length :=
     ComputableInO.of_linear (.of_unframe fun _ => rfl)
-  have hdesc := hdec.inO.computableInO.comp hu
+  have hdesc := hdec.inO.comp hu
   have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one.computableInO
   obtain ⟨TG, hGb⟩ := hG.computableInO
   have hGu := ComputableInO.natToUnary.comp hGb

Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean

@@ -251,10 +251,10 @@ theorem computableInO_timeDiagonal {J : ℕ → ℕ} (hJ : TimeConstructible J)
   have this : ComputableTidilyInO (timeDiagonal J) encBits encBool
       (fun x => (x.length + 1) ^ 5 * (J x.length + 1) ^ 3) fun x => (x.length + 1) ^ 5 *
       (J x.length + 1) ^ 3 := by
-    obtain ⟨dd, ed, hdec⟩ := exists_computableTidilyInDegree_decodeDesc
+    obtain ⟨dd, ed, hdec⟩ := exists_computableInDegree_decodeDesc
     have hu : ComputableTidilyInO unframe encBits encBits (fun x => x.length) fun x => x.length :=
       ComputableTidilyInO.of_linear (.of_unframe fun _ => rfl)
-    have hdesc := hdec.inO.comp hu
+    have hdesc := hdec.inO.tidy.comp hu
     have hsym := Universal.computableTidilyInDegree_map_eBit.inO_one
     have hclock := hJ.computableInO.tidy
     have hU := computableTidilyInO_universal.comp (hdesc.prod (hsym.prod hclock))

Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean

@@ -576,8 +576,8 @@ polynomial time. -/
 theorem computableInPolyTime_selfHardwire :
     ComputableInPolyTime (fun y : List Bool => eDesc (hardwire (decodeDesc y) (frame y)))
       encBits encBits := by
-  obtain ⟨_, _, hdec⟩ := exists_computableTidilyInDegree_decodeDesc
-  have hpair := hdec.computableTidilyInPolyTime.computableInPolyTime.prod
+  obtain ⟨_, _, hdec⟩ := exists_computableInDegree_decodeDesc
+  have hpair := hdec.computableInPolyTime.prod
     (ComputableInPolyTime.bitsFrame encBits)
   exact (ComputableInPolyTime.of_eq (f := fun d : Desc => eDesc d) (encIn := eDesc)
     (encOut := encBits) fun _ => rfl).comp (computableInPolyTime_hardwire.comp hpair)

Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean

@@ -15,7 +15,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decod
 
 Every word decodes to a description of a machine (`Turing.MultiTapeTM.Universal.descDecoder`):
 the decoder inverts the encoding `Turing.MultiTapeTM.Universal.eDesc` of descriptions, returns a
-description of polynomial encoded length on every other word, and is tidily computable within
+description of polynomial encoded length on every other word, and is computable within
 bounds of fixed degrees. It is assembled from the generic decoders of
 `Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder` along the fields of a
 description, its transitions, their keys and their actions.
@@ -32,7 +32,7 @@ to any length.
 
 * `Turing.MultiTapeTM.Universal.decodeDesc_eDesc`: decoding inverts the encoding.
 * `Turing.MultiTapeTM.Universal.decodeDesc_unframe_frame_append`: padded descriptions.
-* `Turing.MultiTapeTM.Universal.exists_computableTidilyInDegree_decodeDesc`: decoding is tidily
+* `Turing.MultiTapeTM.Universal.exists_computableInDegree_decodeDesc`: decoding is
   computable within bounds of fixed degrees.
 -/
 
@@ -91,13 +91,11 @@ theorem decodeDesc_unframe_frame_append (d : Desc) (pad : List Bool) :
     decodeDesc (unframe (frame (eDesc d) ++ pad)) = d := by
   rw [unframe_frame_append, decodeDesc_eDesc]
 
-/-- **Decoding is efficient.** It is tidily computable, and the decoded descriptions have
+/-- **Decoding is efficient.** It is computable, and the decoded descriptions have
 encoded length polynomial in the length of the word, within bounds of fixed degrees. -/
-theorem exists_computableTidilyInDegree_decodeDesc :
-    ∃ d e, ComputableTidilyInDegree decodeDesc encBits eDesc d e := by
-  obtain ⟨d, e, h⟩ := descDecoder.computable
-  obtain ⟨t, s, ht, hs, k, Q, hfin, tm, htm⟩ := Internal.NormalForm.degree h
-  exact ⟨d, e, ⟨t, s, ht, hs, k, Q, hfin, tm, htm⟩, h.2⟩
+theorem exists_computableInDegree_decodeDesc :
+    ∃ d e, ComputableInDegree decodeDesc encBits eDesc d e :=
+  descDecoder.computable
 
 end Universal
 

Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean

@@ -40,8 +40,7 @@ single bit, independently of hierarchy theorems and Ladner's language.
 
 * `Turing.MultiTapeTM.Universal.computableTidilyInDegree_map_eBit`: input symbols in linear time
   and output size.
-* `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_decodeDesc`,
-  `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_map_eBit`,
+* `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_map_eBit`,
   `Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_eBit`,
   `Turing.MultiTapeTM.Universal.computableInPolyTime_decodeDesc`,
   `Turing.MultiTapeTM.Universal.computableInPolyTime_map_eBit`,
@@ -132,14 +131,6 @@ theorem computableTidilyInDegree_map_eBit :
     (ComputableTidilyInDegree.of_linear (encIn := encBits) (encMid := encTrueDoubled) (f := id)
       (trueDoubleT.computableTidilyInLinearTimeAndSpace fun x => (trueDoubleT_run x).symm))
 
-
-/-- Decoding a machine description is polynomial-time in the input word. -/
-@[fun_prop]
-theorem computableTidilyInPolyTime_decodeDesc :
-    ComputableTidilyInPolyTime decodeDesc encBits eDesc :=
-  let ⟨_, _, h⟩ := exists_computableTidilyInDegree_decodeDesc
-  h.computableTidilyInPolyTime
-
 /-- The input of a machine as symbols is linear. -/
 @[fun_prop]
 theorem computableTidilyInPolyTime_map_eBit :
@@ -232,7 +223,8 @@ theorem computableTidilyInPolyTime_universal :
 @[fun_prop]
 theorem computableInPolyTime_decodeDesc :
     ComputableInPolyTime decodeDesc encBits eDesc :=
-  .of_tidy computableTidilyInPolyTime_decodeDesc
+  let ⟨_, _, h⟩ := exists_computableInDegree_decodeDesc
+  h.computableInPolyTime
 
 /-- Plain polynomial-time certificate for coding a bit string as unary symbol numbers. -/
 @[fun_prop]

ComplexityTests/TimeHierarchy.lean

@@ -41,10 +41,15 @@ example :
 
 /-- Every word decodes to a description of polynomial encoded length. -/
 example : ∃ e c : ℕ, ∀ w : List Bool, (eDesc (decodeDesc w)).length ≤ c * (w.length + 1) ^ e := by
-  obtain ⟨_d, e, h⟩ := exists_computableTidilyInDegree_decodeDesc
+  obtain ⟨_d, e, h⟩ := exists_computableInDegree_decodeDesc
   obtain ⟨c, hc⟩ := h.2
   exact ⟨e, c, fun w => hc w⟩
 
+/-- Plain automation composes description decoding with framing of its input. -/
+example : ComputableInPolyTime (fun w : List Bool => (decodeDesc w, frame w)) encBits
+    (encPair eDesc encBits) := by
+  fun_prop
+
 /-! ### The clock -/
 
 example :

scripts/tidy_surface_baseline.json

@@ -53,10 +53,9 @@
  "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2,
  "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2,
  "Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean": 7,
- "Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean": 1,
  "Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean": 9,
  "Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean": 2,
- "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 5,
+ "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 4,
  "Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean": 2,
  "Complexity/Computability/Probabilistic/Adaptive.lean": 5,
  "Complexity/Computability/Probabilistic/CoinTape.lean": 5,