review: (first pass) refactor traversal to make it more reviewable

[thorimur]

This PR is very bulky, which makes it difficult to review the logic. Part of the issue here is using a bare continuation go for folding, and descending into children manually everywhere...which is fine for claude, but not so much for human reviewers!

So, this PR cuts ~60 lines off of the main file so we can better see what's going on. Most of the +130 is documentation or just cleaner abstractions that make it more readable.

---

[github-actions]

PR summary d300915bf1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
There are 6696 files with changed transitive imports taking up over 297229 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ A
+ B
+ Gr'
+ MyAction
+ MyPred
+ MySub₂
+ MySub₂.toAddSubgroup
+ Num'
+ Sm'
+ TraceResult
+ VisitStep
+ Zo'
+ analyzeTraces
+ b
+ dedupByString
+ extractInstName
+ instance : Gr' Int
+ instance : Membership ℕ (MyPred ℕ) where mem s a := s a
+ instance : Singleton ℕ (MyPred ℕ) where singleton a x := x = a
+ instance : Zo' Int
+ instance {G : Type} [AddCommGroup G] : CoeSort (MySub₂ G) Type
+ instance {n} : Num' Int n
+ instance {α} [Zo' α] : Num' α 0
+ instance {α} [h : Gr' α] : Sm' α := { h with }
+ myOp
+ myPredBoundedOrder
+ myPredCompleteLattice
+ myPredDistribLattice
+ myPred_disjoint_singleton_right
+ mySub₂AddCommGroup
+ mySub₂AddCommMonoid
+ mySub₂MyAction
+ myTestFun
+ onlyOnDefEqNodes
+ reportDefEqAbuse
+ stripTraceResultPrefix
+ testCoersion
+ testVirtualParent
+ testVirtualParentFixed
+ test_zo_cmd_abuse
+ traceResultOf
+ visitWithAndAscendM
+ visitWithM
+ zo_eq_iff
++ instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} :

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.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
11957	1	backward.isDefEq

Current commit d18f23e60c
Reference commit d300915bf1

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).