refactor(Universal): assemble the UTM step with fun_prop

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

@@ -305,7 +305,7 @@ public theorem stepTime_iterate_le (x : List ℕ) (j : ℕ) :
   have hbits := ComputableTidilyInO.length_encNat_mono
     (show cfg.inputPos ≤ (encList encUnary x).length + 1 by omega)
   unfold stepTime stepBound
-  dsimp only
+  dsimp only [Ctx.desc, Ctx.input, Ctx.cfg]
   exact Nat.add_le_add
     (Nat.mul_le_mul (Nat.mul_le_mul_right _ (by omega)) (by omega))
     (Nat.mul_le_mul (by omega) (by gcongr))

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

@@ -382,7 +382,8 @@ lemma halted_inO {α : Type} {enc : α ↪ List Bool} {c : α → SCfg} {T S : 
   ((ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
     fun b : Bool => !b).inO_one.comp_linear
       ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
-        (state_inO.comp_linear h))).of_enc_eq fun a => by
+        -- bridge for #862: tidy client of the plain `state_inO`
+        (state_inO.tidy.comp_linear h))).of_enc_eq fun a => by
         simp only [Function.comp_apply]
         cases (c a).state <;> rfl
 
@@ -435,7 +436,8 @@ public lemma stepG_inO :
   have hc := fst eCtl (encPair encNat encUnary)
   have hg := hc.fst'.fst'
   have hsym := countSym_inO (inputPos_inO hg.snd') hc.snd'.fst' hc.snd'.snd'
-  refine (stepWith_inO.comp (hg.prod (hsym.of_enc_eq (g := fun s : CSt => gSym s.1)
+  -- bridge for #862: tidy client of the plain `stepWith_inO`
+  refine (stepWith_inO.tidy.comp (hg.prod (hsym.of_enc_eq (g := fun s : CSt => gSym s.1)
     fun _ => rfl))).mono 100 (fun s => ?_) fun s => ?_
   all_goals
     have hw := wTime_le' (s.1.1.1, gSym s.1)
@@ -464,7 +466,8 @@ public lemma stepF_inO : ComputableTidilyInO (fun s : CSt => stepWith s.1.1.2.1
   have hn := snd eCtl (encPair encNat encUnary)
   have hg := hc.fst'.snd'
   have hsym := countSym_inO (inputPos_inO hg.snd') hn.fst' hn.snd'
-  refine (stepWith_inO.comp (hg.prod (hsym.of_enc_eq (g := xSym)
+  -- bridge for #862: tidy client of the plain `stepWith_inO`
+  refine (stepWith_inO.tidy.comp (hg.prod (hsym.of_enc_eq (g := xSym)
     fun _ => rfl))).mono 100 (fun s => ?_) fun s => ?_
   all_goals
     have hw := wTime_le' (s.1.1.2, xSym s)
@@ -619,7 +622,8 @@ public lemma cEmit_inO : ComputableTidilyInO (fun s : CSt => gEmit s.1) eCSt enc
 public lemma cCont_inO : ComputableTidilyInO (fun s : CSt => s.1.1.1.2.state.isSome) eCSt encBool
     (fun s => ((eCSt s).length + 1) ^ 3) fun s => (eCSt s).length + 1 :=
   (((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
-    (state_inO.comp_linear (fst eCtl (encPair encNat encUnary)).fst'.fst'.snd'))).mono 1
+    -- bridge for #862: tidy client of the plain `state_inO`
+    (state_inO.tidy.comp_linear (fst eCtl (encPair encNat encUnary)).fst'.fst'.snd'))).mono 1
     (fun s => by
       have hL : (eCSt s).length + 1 ≤ ((eCSt s).length + 1) ^ 3 := Nat.le_self_pow (by norm_num) _
       dsimp only [eCSt] at *

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

@@ -423,7 +423,7 @@ lemma wTime_le (s : St) : wTime (s.1, symAt s) ≤ 9 * ((eSt s).length + 1) ^ 3
     Nat.mul_le_mul (Nat.mul_le_mul hl (by omega)) (by omega)
   have hdigits := Nat.pow_le_pow_left (Nat.succ_le_succ hpos) 2
   unfold wTime
-  dsimp only at hproduct hdigits ⊢
+  dsimp only [WCtx.desc, WCtx.cfg] at hproduct hdigits ⊢
   nlinarith [Nat.le_self_pow (show 2 ≠ 0 by decide) ((eSt s).length + 1)]
 
 /-- The step at the end of a pass. -/
@@ -446,7 +446,8 @@ public lemma stepAt_inO : ComputableTidilyInO stepAt eSt (encPair eCfg eSym)
       (enc := eSym)).inO_one.comp_linear hcur)).of_enc_eq fun s => by
         simp only [symAt, Function.comp_apply]
         split_ifs <;> simp_all
-  have hstep := stepWith_inO.comp (hdc.prod hsym)
+  -- bridge for #862: tidy client of the plain `stepWith_inO`
+  have hstep := stepWith_inO.tidy.comp (hdc.prod hsym)
   have hidle := hc.prod (const (encMid := eSym) none)
   refine (((ComputableInO.natIsZero.tidy.comp_linear hr).ite hidle hstep).of_enc_eq (g := stepAt)
     fun s => ?_).mono 100 (fun s => ?_) fun s => ?_
@@ -527,7 +528,8 @@ public lemma foldFinish_inO : ComputableTidilyInO foldFinish eSt eHalted
   refine (((ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := eHalted)
     fun b : Bool => !b).inO_one.comp_linear
       ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
-        (state_inO.comp_linear hc))).of_enc_eq (g := foldFinish) fun s => by
+        -- bridge for #862: tidy client of the plain `state_inO`
+        (state_inO.tidy.comp_linear hc))).of_enc_eq (g := foldFinish) fun s => by
         simp only [foldFinish, Function.comp_apply]
         cases s.1.2.state <;> rfl).mono 1 (fun s => ?_) fun s => ?_ <;>
   · have hL : (eSt s).length + 1 ≤ ((eSt s).length + 1) ^ 3 := Nat.le_self_pow (by norm_num) _

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

@@ -75,7 +75,8 @@ lemma round_inO : ComputableTidilyInO round eRun eRun (fun s => stepTime s.1 + (
     fun s => (eRun s).length := by
   have hctx := fst eCtx (encList encUnary)
   have hout := snd eCtx (encList encUnary)
-  have hstep := step_inO.comp hctx
+  -- bridge for #862: tidy client of the plain `step_inO`
+  have hstep := step_inO.tidy.comp hctx
   have hnewout := ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear
     hstep.snd').ite ((ComputableTidilyInDegree.snoc encUnary).inO_one.comp_linear
       (hout.prod ((ComputableTidilyInDegree.getD (enc₁ := encUnary) 0).inO_one.comp_linear
@@ -206,7 +207,8 @@ public theorem computableTidilyInO_universal :
       exact length_eRun_le i.1 i.2.1 hk)).tidy
   have hhalted := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
     (fun b : Bool => !b)).inO_one.comp_linear ((ComputableTidilyInDegree.isSome encUnary).inO_one
-      |>.comp_linear (state_inO.comp_linear hiter.fst'.snd'))
+      -- bridge for #862: tidy client of the plain `state_inO`
+      |>.comp_linear (state_inO.tidy.comp_linear hiter.fst'.snd'))
   refine ((hiter.snd'.prod hhalted).mono 16 (fun i => ?_) fun i => ?_).of_enc_eq fun i => ?_
   · have h₁ : (eDesc i.1).length ≤ (eIn i).length := length_le_encPair_left _ _ i
     have h₂ := Nat.pow_le_pow_left (Nat.add_le_add_right h₁ 1) 2

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

@@ -516,7 +516,8 @@ private lemma foldFinishS_inO : ComputableTidilyInO foldFinishS eSSt eOut
     (fun s => ((eSSt s).length + 1) ^ 3) fun s => (eSSt s).length + 1 := by
   have h₁ := fst eSt (encPair encUnary (encList encUnary))
   have h₂ := snd eSt (encPair encUnary (encList encUnary))
-  have hst := state_inO.comp_linear h₁.fst'.snd'
+  -- bridge for #862: tidy client of the plain `state_inO`
+  have hst := state_inO.tidy.comp_linear h₁.fst'.snd'
   have hnone := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
     fun b : Bool => !b).inO_one.comp_linear
       ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear hst)

scripts/tidy_surface_baseline.json

@@ -52,7 +52,6 @@
  "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5,
  "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2,
  "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2,
- "Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean": 6,
  "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,