v1.4.23 — Add dbg_trace tracing to every genuinely recursive Lean block

Completes the dbg_trace initiative: every Lean code block in the book was surveyed chapter by chapter, and every genuine recursion now has a dbg_trace-annotated sibling definition showing the computation unwind one step at a time.

• Chapter 1 (pattern-setting installment): Vec.replicate, Vec.dot, double (via Nat.rec). Also documents a real limitation found along the way — myLength (via List.rec/#reduce) cannot be traced at all, since kernel reduction skips dbg_trace's side effect entirely.
• Chapter 10: natSmul.
• Chapter 11: Path.append and Path.length, traced together since Path has no Repr instance to observe Path.append in isolation.
• Chapter 14: the corresponding exercise-solution mirrors of the above.
• Chapters 2–9, 12, 13 confirmed to need no changes — surveyed and found to contain only non-recursive structures, instances, and tactic-mode proofs.

Full details in CHANGELOG v1.4.23.

Includes a source-bundle asset (-source.zip) alongside the PDF, per the usual release format.