perf: special case single-child nodes in DiscrTree

[robsimmons]

This PR adds a new branch to the DiscrTree data structure, giving a memory-optimized way of representing discrimination tree keys with no values and a single node. The value .child k v is treated as equivalent to .node #[] #[(k, v)].

Rationale: in many applications, many or most of the nodes in a trie are single-child-no-value-carrying nodes (the robot assistant claimed this was >80% in the case of the Simp post-tree for all of Mathlib, but I wouldn't stand behind that). Special-casing this common case is often an easy win for memory usage and for performance, and this PR is in part a generalization of the match optimization from #11889.

Memory usage reduction

The big change not captured in benchmarking is that this PR makes it ~9% less expensive, in terms of unshared memory usage, for a file worker to import Lean, and about ~20% less expensive for a file worker to import Mathlib. To easily see the ~9% improvement on a linux/x86 system, you can create a lean file Mem.lean

import Lean
#eval do IO.println (← IO.FS.readFile "/proc/self/smaps_rollup")

and then run these commands:

elan run leanprover/lean4:nightly-2026-08-11 \
  lean Mem.lean | grep -E 'Pss_Anon|Private_Dirty'

elan run leanprover/lean4-pr-releases:pr-release-14805-08ea7af \
  lean Mem.lean | grep -E 'Pss_Anon|Private_Dirty'

(you may need to rerun it a few times until the Pss_Anon and Private_Dirty are close to each other, the number isn't stable right when the toolchain downloads for reasons I don't fully understand)

Full Glossy Claude Writeup if that interests you.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5594178cba78098b6b42b5a13c3506234b64f7a5 --onto 6e91fff236ea9c68465989c1ecdf79b60e2f6bff. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-17 20:30:19)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-17 21:20:37)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 13:14:55)
• 💥 Mathlib branch lean-pr-testing-14805 build failed against this PR. (2026-08-21 01:11:24) View Log
• 💥 Mathlib branch lean-pr-testing-14805 build failed against this PR. (2026-08-28 13:47:12) View Log
• 💥 Mathlib branch lean-pr-testing-14805 build failed against this PR. (2026-08-28 18:13:22) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5594178cba78098b6b42b5a13c3506234b64f7a5 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-17 20:30:21)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-17 21:20:39)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-20 13:14:57)
• ✅ Reference manual branch lean-pr-testing-14805 has successfully built against this PR. (2026-08-21 01:13:00) View Log
• 🟡 Reference manual branch lean-pr-testing-14805 build against this PR didn't complete normally. (2026-08-21 01:14:36) View Log
• ✅ Reference manual branch lean-pr-testing-14805 has successfully built against this PR. (2026-08-28 13:46:19) View Log
• 🟡 Reference manual branch lean-pr-testing-14805 build against this PR didn't complete normally. (2026-08-28 13:47:22) View Log
• ✅ Reference manual branch lean-pr-testing-14805 has successfully built against this PR. (2026-08-28 18:10:47) View Log
• 🟡 Reference manual branch lean-pr-testing-14805 build against this PR didn't complete normally. (2026-08-28 18:11:55) View Log

[downstream-lean4]

The adaptation PR for this PR is leanprover/downstream-lean4#23.

[nomeata]

Related attempt: #12838

[robsimmons]

Aah cool @nomeata! This is intentionally trying to be less ambitious, and @Vtec234 convinced me that there were some reasons to be cautious about the path construct — depending on insertion patterns some things might go quadratic there. If you read the claude report, it seemed convinced that given the shape of mathlib's simp data, special casing chains of stars, instead of arrays of arbitrary keys, would be a neater win.

I think your separation of leaf nodes (values) from path/branch nodes also really makes sense, but from a "that's a good refactor that makes the data structure operations clearer" sense, I doubt it would be a huge optimization.

[leanprover-radar]

Benchmark results for 0ad131b against e991a05 are in. There are significant results. @robsimmons

• ✅ build//instructions: -29.5G (-0.26%)

Large changes (3🟥)

• 🟥 compiled/rbmap_checkpoint//instructions: +3.0G (+23.49%)
• 🟥 compiled/rbmap_checkpoint//task-clock: +431ms (+29.60%)
• 🟥 compiled/rbmap_checkpoint//wall-clock: +448ms (+30.62%)

Medium changes (7✅)

• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -1.1G (-1.26%)
• ✅ compiled/incr_header_save//task-clock: -164ms (-11.20%)
• ✅ compiled/incr_header_save//wall-clock: -166ms (-11.07%)
• ✅ elab/big_beq_rec//maxrss: -20MiB (-1.08%)
• ✅ elab/sym_let_to_have_nested//maxrss: -20MiB (-1.07%)
• ✅ lake/inundation/build/clean//instructions: -8.5G (-2.64%)
• ✅ lake/inundation/build/clean//task-clock: -4s (-5.12%)

Small changes (266✅, 4🟥)

• ✅ build/module/Init.Data.Array.Sort//instructions: -4.0M (-0.74%)
• ✅ build/module/Init.Data.Array//instructions: -5.7M (-1.00%)
• ✅ build/module/Init.Data.Char.Ordinal//instructions: -26.4M (-0.45%)
• ✅ build/module/Init.Data.Float.Model.Unpacked//instructions: -5.7M (-1.02%)
• ✅ build/module/Init.Data.FloatArray//instructions: -5.7M (-1.03%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic//instructions: -3.9M (-0.74%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Combinators//instructions: -5.3M (-0.96%)
• ✅ build/module/Init.Data.Iterators.Lemmas//instructions: -5.5M (-1.00%)
• ✅ build/module/Init.Data.Range.Polymorphic//instructions: -11.5M (-1.86%)
• ✅ build/module/Init.Data.SInt//instructions: -9.5M (-1.61%)
• ✅ build/module/Init.Data.String.Lemmas.Pattern.Find.Basic//instructions: -16.9M (-0.72%)
• ✅ build/module/Init.Data.String.Lemmas.Pattern.Find//instructions: -5.9M (-1.07%)
• ✅ build/module/Init.Data.String.Lemmas.Pattern.TakeDrop//instructions: -4.9M (-0.89%)
• ✅ build/module/Init.Data.String.Lemmas//instructions: -4.2M (-0.74%)
• ✅ build/module/Init.Data.String.Substring//instructions: -22.5M (-0.61%)
• ✅ build/module/Init.Data.UInt//instructions: -4.5M (-0.84%)
• ✅ build/module/Init.Data.Vector//instructions: -13.4M (-2.02%)
• ✅ build/module/Init.Data//instructions: -20.3M (-2.60%)
• ✅ build/module/Init.Grind.Homo.Int16//instructions: -9.2M (-1.52%)
• ✅ build/module/Init.Grind.Homo//instructions: -9.4M (-1.61%)
• and 250 more

[robsimmons]

downstream-lean4's mathlib radar shows a significant -104MB decrease in maxrss for import Mathlib — the percentage is only ~3.6% because it's counting shared mmapped pages as part of maxrss.