[kim-em]

Summary

Refs #10378. Integrate provider-key reconciliation with immutable shared tower contexts, dependency caches, complete live requests, catalog selection and the prescribed algebraic union.

• Use one staged lifting recursion for ordered subsequences and checked provider reordering. Prove exact factory acceptance, sign/value preservation and agreement of accepted maps; expose packed-handle laws.
• Retain native coefficient maps in nominal context conversions. Reconstruct canonical source histories from the validated target and prove agreement with supplied source and ordered models.
• Generalize canonical owner/cache consumers to the retained reader. Gather reordered and incomparable source paths into an installed jointly validated catalog prefix, retaining every requested infinitesimal predecessor and the dependency closure.
• Realize original and refreshed finite live inventories with one ordinary partial reader. Link this reader to a provider model of the actual selected prefix and depth.
• Identify gathered native values with the prescribed union: arithmetic, signs, order, parent embeddings, owner coherence, registration, generator coverage and union extension. Compare ordered and reconciled reader paths wherever the ordered factory accepts.

The native catalog stores validated prefixes. Its semantic invariant asserts existence of a provider model for each prefix; it does not store the original insertion witness as runtime data. The selector checks key metadata and uses the first eligible prefix. It cannot manufacture a missing joint provider history.

Verification

Final head: b9079e92131731928f687fe0f25c471075401356.
Base: actual upstream main 15a478e2bddd1e2bd445d40979b7de6e3f882c14. #10834 and #10821 are already merged. The unmerged layers are included here; this PR has no unmerged implementation prerequisite.

• Full lake build: 14,512 jobs, successful.
• Integrated catalog/live/union/staged/provider regression targets: 10,878 jobs, successful.
• Named admission audit: 414 import cones / 1,247 local modules, no admissions; 11 scanner tests passed.
• Mathlib-free audit: 64 benchmark executables and 398 build-only proof probes.
• DAG, Phase 4 registration, copyright and file-size gates passed.
• Exact final-head Claude Opus review: no merge blocker; the complete review was read and checked. One minor companion wording correction is retained with the enlargement documentation update.

Compiled controls exercise the actual Liouville provider, infinitesimal-dependent selected roots, ancestor/cache reuse, descriptor revalidation, maximum-depth catalog choice, stale contexts and missing joint prefixes. Literal reversed/incomparable key controls test the exact selector predicate. Two-provider reverse-order theorem tests are conditional on actual supplied provider histories; no compiled two-independent-provider fixture is claimed. Their union regression asserts ordered rejection, two accepted owner orders, owner and target inverses, coherence and parent embedding.

Remaining #10378 scope

Reconciled enlargement naturality is being implemented separately. The general recursive accepted finite-evidence exporter, one ordinary point through arbitrary interleaved stages, remaining independent conformance and specified Phase 4 evidence remain open. This delivery does not close #10378 or claim Phase 4 readiness.