Consolidate research results and choose the next bounded depth test

[GoGoKo699]

The recent compiler advances left a long chronological handoff and an overly broad suggestion to share sources across groups. This revision gathers the established results and identifies the actual remaining depth costs before selecting more construction work.

• Replace the 576-line workspace history with a 205-line checkpoint: theorem contracts, evidence maturity, current bounds, two remaining gaps, and proof homes.
• Record five separately charged linear-depth contributions. Sharing only phase preparation cannot remove the others.
• Select one explicitly unproved next component target: an exact dirty indicator with linear T/Clifford count and width, logarithmic address T-depth, literal phases and full dirty/reference return. A nonuniform chunk schedule is a concrete candidate with five proof obligations and stop conditions.
• State that this component alone would leave full-frame O(n) depth unchanged. Keep the high-precision endpoint deferred until a new global native identity has a symbolic ledger.
• Update the current real-frame comparator and verification pointer. Add narrowly scoped primary-source comparisons for recent magic-hierarchy lower bounds; neither is imported as a compiler premise.

No theorem, native circuit or test implementation changes. The previously verified scientific baseline has 476 tests. For this documentation-only revision, 51 focused math/presentation/narrative/literature/provenance checks, explicit checkpoint-anchor checks, and whitespace checks pass locally. All five remote checks pass, including rendered presentation; Python 3.11 and 3.13 each pass all 476 tests and reproduce all four exact receipt suites. Independent final review found no blocker.