chore: deprecate Turing files

[BoltonBailey]

This follow-up deprecates files moved in #35608

This PR was made with the assistance of Claude Code

---

• depends on: chore(Computability): move TM files to a single folder #35608

[github-actions]

PR summary 4009dd50cc

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Computability.TMComputable	955	1	-954 (-99.90%)
Mathlib.Computability.TMToPartrec	654	1	-653 (-99.85%)
Mathlib.Computability.TMConfig	633	1	-632 (-99.84%)
Mathlib.Computability.TuringMachine	500	1	-499 (-99.80%)
Mathlib.Computability.PostTuringMachine	471	1	-470 (-99.79%)
Mathlib.Computability.Tape	333	1	-332 (-99.70%)

Import changes for all files

Files	Import difference
Mathlib.Computability.TMComputable	-954
Mathlib.Computability.TMToPartrec	-653
Mathlib.Computability.TMConfig	-632
Mathlib.Computability.TuringMachine	-499
Mathlib.Computability.PostTuringMachine	-470
Mathlib.Computability.Tape	-332
Mathlib.Computability.StateTransition	-1

---

Declarations diff

- BlankExtends
- BlankExtends.above
- BlankExtends.above_of_le
- BlankExtends.below_of_le
- BlankExtends.refl
- BlankExtends.trans
- BlankRel
- BlankRel.above
- BlankRel.below
- BlankRel.equivalence
- BlankRel.refl
- BlankRel.setoid
- BlankRel.symm
- BlankRel.trans
- Cfg'
- Cfg.map
- Cfg.then
- Code
- Code.Ok
- Code.Ok.zero
- Code.eval
- Cont
- Cont'
- Cont.eval
- Cont.then
- Cont.then_eval
- Dir
- EvalsTo
- EvalsTo.refl
- EvalsTo.trans
- EvalsToInTime
- EvalsToInTime.refl
- EvalsToInTime.trans
- FinTM2
- K'
- K'.elim
- K'.elim_aux
- K'.elim_main
- K'.elim_rev
- K'.elim_stack
- K'.elim_update_aux
- K'.elim_update_main
- K'.elim_update_rev
- K'.elim_update_stack
- ListBlank
- ListBlank.append
- ListBlank.append_assoc
- ListBlank.append_mk
- ListBlank.cons
- ListBlank.cons_flatMap
- ListBlank.cons_head_tail
- ListBlank.cons_mk
- ListBlank.exists_cons
- ListBlank.ext
- ListBlank.flatMap
- ListBlank.flatMap_mk
- ListBlank.hasEmptyc
- ListBlank.head
- ListBlank.head_cons
- ListBlank.head_map
- ListBlank.head_mk
- ListBlank.induction_on
- ListBlank.inhabited
- ListBlank.liftOn
- ListBlank.map
- ListBlank.map_cons
- ListBlank.map_mk
- ListBlank.map_modifyNth
- ListBlank.mk
- ListBlank.modifyNth
- ListBlank.nth
- ListBlank.nth_map
- ListBlank.nth_mk
- ListBlank.nth_modifyNth
- ListBlank.nth_succ
- ListBlank.nth_zero
- ListBlank.tail
- ListBlank.tail_cons
- ListBlank.tail_map
- ListBlank.tail_mk
- Machine
- Machine.inhabited
- Machine.map
- Machine.map_respects
- Machine.map_step
- PointedMap.headI_map
- PointedMap.map_pt
- PointedMap.mk_val
- PointedMap.{u,
- StAct
- StAct.inhabited
- Stmt'
- Stmt.map
- TM2Computable
- TM2ComputableAux
- TM2ComputableInPolyTime
- TM2ComputableInPolyTime.toTM2ComputableInTime
- TM2ComputableInTime
- TM2ComputableInTime.toTM2Computable
- TM2Outputs
- TM2OutputsInTime
- TM2OutputsInTime.toTM2Outputs
- Tape
- Tape.exists_mk'
- Tape.inhabited
- Tape.left₀
- Tape.map
- Tape.map_fst
- Tape.map_mk'
- Tape.map_mk₁
- Tape.map_mk₂
- Tape.map_move
- Tape.map_write
- Tape.mk'
- Tape.mk'_head
- Tape.mk'_left
- Tape.mk'_left_right₀
- Tape.mk'_nth_nat
- Tape.mk'_right
- Tape.mk'_right₀
- Tape.mk₁
- Tape.mk₂
- Tape.move
- Tape.move_left_mk'
- Tape.move_left_nth
- Tape.move_left_right
- Tape.move_right_left
- Tape.move_right_mk'
- Tape.move_right_n_head
- Tape.move_right_nth
- Tape.nth
- Tape.nth_zero
- Tape.right₀
- Tape.right₀_nth
- Tape.write
- Tape.write_mk
- Tape.write_mk'
- Tape.write_move_right_n
- Tape.write_nth
- Tape.write_self
- addBottom
- addBottom_head_fst
- addBottom_map
- addBottom_modifyNth
- addBottom_nth_snd
- addBottom_nth_succ_fst
- case_eval
- clear_ok
- codeSupp
- codeSupp'
- codeSupp'_self
- codeSupp'_supports
- codeSupp_case
- codeSupp_comp
- codeSupp_cons
- codeSupp_fix
- codeSupp_self
- codeSupp_succ
- codeSupp_supports
- codeSupp_tail
- codeSupp_zero
- code_is_ok
- comp_eval
- cons_eval
- contStack
- contSupp
- contSupp_comp
- contSupp_cons₁
- contSupp_cons₂
- contSupp_fix
- contSupp_halt
- contSupp_supports
- cont_eval_fix
- copy_ok
- decidableEqK
- default_Γ'
- exists_code
- exists_code.comp
- exists_enc_dec
- fix_eval
- halt
- haltList
- head_eval
- head_main_ok
- head_stack_ok
- head_supports
- id
- idComputable
- idComputableInPolyTime
- idComputableInTime
- idComputer
- id_eval
- inhabitedCfg
- inhabitedEvalsToInTime
- inhabitedFinTM2
- inhabitedStmt
- inhabitedTM2Computable
- inhabitedTM2ComputableAux
- inhabitedTM2ComputableInPolyTime
- inhabitedTM2ComputableInTime
- inhabitedTM2EvalsTo
- inhabitedTM2Outputs
- inhabitedTM2OutputsInTime
- inhabitedσ
- initList
- instance : Inhabited (Λ' M)
- instance : Inhabited (Λ' Γ Λ)
- instance [Inhabited Λ] : Inhabited (Λ' Γ Λ σ)
- instance {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] : CoeFun (PointedMap Γ Γ') fun _ ↦ Γ → Γ'
- instance {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] : Inhabited (PointedMap Γ Γ')
- instance Γ'.fintype [DecidableEq K] [Fintype K] [∀ k, Fintype (Γ k)] : Fintype (Γ' K Γ)
- instance Γ'.inhabited : Inhabited (Γ' K Γ)
- instance Λ'.inhabited [Inhabited Λ] : Inhabited (Λ' K Γ Λ σ)
- instance Λ'.instDecidableEq : DecidableEq Λ' := fun a b => by
- instance Λ'.instInhabited : Inhabited Λ'
- map_init
- move
- moveExcl
- move_ok
- move₂
- move₂_ok
- natEnd
- nil
- nil_eval
- peek'
- pop'
- prec
- pred
- pred_eval
- pred_ok
- proj
- proj_map_nth
- push'
- read
- readAux
- ret_supports
- rfind
- splitAtPred
- splitAtPred_eq
- splitAtPred_false
- stRun
- stVar
- stWrite
- stepAux_move
- stepAux_read
- stepAux_write
- stepNormal
- stepNormal.is_ret
- stepNormal_eval
- stepNormal_then
- stepRet
- stepRet_eval
- stepRet_then
- step_run
- stk_nth_val
- stmtStRec.{l}
- succ_eval
- succ_ok
- supportsStmt_move
- supportsStmt_read
- supportsStmt_write
- supports_biUnion
- supports_insert
- supports_run
- supports_singleton
- supports_union
- tail_eval
- trAux
- trCfg_init
- trCont
- trContStack
- trInit
- trLList
- trList
- trList_ne_consₗ
- trNat
- trNat_default
- trNat_natEnd
- trNat_zero
- trNormal_respects
- trNormal_run
- trNormal_supports
- trNum
- trNum_natEnd
- trPosNum
- trPosNum_natEnd
- trStAct
- trStmts
- trStmts₁_run
- trStmts₁_self
- trStmts₁_supports
- trStmts₁_supports'
- trStmts₁_trans
- trTape
- trTape'
- trTape'_move_left
- trTape'_move_right
- trTape_mk'
- tr_clear
- tr_copy
- tr_eval_dom
- tr_init
- tr_move
- tr_pred
- tr_push
- tr_read
- tr_respects_aux
- tr_respects_aux₁
- tr_respects_aux₂
- tr_respects_aux₃
- tr_ret_comp
- tr_ret_cons₁
- tr_ret_cons₂
- tr_ret_fix
- tr_ret_halt
- tr_ret_respects
- tr_succ
- univ_supports
- unrev
- unrev_ok
- write
- writes
- zero
- zero'_eval
- zero_eval
- Λ'.Supports
-- Reaches
-- SupportsStmt
-- TrCfg
-- head
-- stepAux
-- stmts
-- stmts_supportsStmt
-- stmts_trans
-- stmts₁
-- stmts₁_self
-- stmts₁_supportsStmt_mono
-- stmts₁_trans
-- trStmts₁
-- trSupp
-- Γ'
--- Cfg.inhabited
--- Stmt.inhabited
--- eval
--- step_supports
--- trCfg
--- trNormal
--- tr_eval
---- Stmt
---- Supports
---- init
---- tr_supports
----- Cfg
----- step
----- tr
----- tr_respects
----- Λ'

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.26, 0.17)

Current number	Change	Type
467	-2	porting notes
135	-5	flexible linter exceptions
22	-1	disabled simpNF lints
626	-3	erw
13067	-6	backward.isDefEq
13	-1	backward.proofsInPublic

Current commit 1019a8da05
Reference commit 4009dd50cc

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(Computability): move TM files to a single folder #35608
  By Dependent Issues (🤖). Happy coding!