[ejgallego]

This PR prevents early fine-grained traces from consuming the speculative profiling result before later hotspots and declaration phases are considered. It visits shallow trace nodes first, retains spans by inclusive duration together with their ancestors, and restores original tree order and parent indices. The retained cap is reduced to 128 spans; summary selection, labels, numeric precision, thread identities and the public schema are unchanged.

Traversal remains bounded by 16,384 visits and message depth 256. Omitted spans or exhausted traversal bounds continue to set truncated.

The frozen eight-case Mathlib qualification compares 6cae79f6 with f8a33b9b on Lean 4.34.0-rc2, with one warmup and three measured rounds per case. A pass requires successful execution, the reference hotspot in the first three summary entries, expected phases, stable leading entries, and a compact UTF-8 profile object at most 20,000 bytes. Whole-response bytes are not scored because Lean warnings add unrelated text. This corpus is external to CI.

Case	Before	After	Before max profile B	After max profile B	Delta B	Remaining failure
ring8	pass	pass	5413	5756	+343	—
nlin	pass	pass	13025	14579	+1554	—
decide2	pass	pass	19915	15623	-4292	—
ring8_tactic	pass	pass	1541	1977	+436	—
nlin_handle	pass	pass	7590	7980	+390	—
fdb_comp	fail	fail	129413	22029	-107384	missing Elab.def.maxSharing; profile exceeds 20,000 B
fdb_eraseMiddle	fail	fail	133494	22483	-111011	profile exceeds 20,000 B
fdb_isLittleO	fail	fail	125890	19740	-106150	grind ranks fourth

Score: 5/8 → 5/8, with no previously passing case regressed. All candidate cases pass execution and stability, and all expected Kernel phases are retained. This draft does not yet meet the 8/8 acceptance target. Pure duration retention still omits a short maxSharing phase; the preserved grind hotspot ranks after three genuinely longer scopes; two profile objects still exceed the budget. Raw-span compaction is reserved for a separate follow-up and is not included here.

• No new flags or response fields.