feat: identify retained nested selected roots in the reals

[kim-em]

Summary

Refs #10378. Interpret the actual retained interval-selected nested descriptors from the merged finite replay fixture in ordinary reals.

• Identify the stored first generator with α, and prove α² = 2, β² = α and β⁴ = 2.
• Prove both selected values lie in (1, 2), then identify α = √2 and β = √α.
• Prove each original descriptor interval contains exactly its retained selected root.
• Build the importing proof consumer in the existing CI experiment step and document its scope.

Both descriptors have empty derivative-sign lists. The whole-line nonempty Thom packet is a separate control and is not interpreted by this module. This fixture has no infinitesimal stage and does not complete the recursive ordinary-real exporter or close #10378.

Prerequisite

#10832 actually merged into upstream main as 8dec01eb291e7f9dc930cf9d0baf9011e98796f2. This PR targets main.

Verification

Exact final head: 033d116a002a7e37f8a65539a60618026b9cde33.

• lake build KernelReplay.FiniteTowerReal: PASS, 4,937 jobs.
• Full lake build: PASS, 14,490 jobs.
• Named admission audit: 394 import cones / 1,230 local modules, no admissions; all 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.
• Fresh exact-head Claude Opus review found no correctness or soundness blocker. Its build condition is satisfied by the full build and gates above; it could not independently run Lean. Optional concrete-form corollaries and a repeated raw-field rewrite are nonblocking follow-ups.

All eleven public theorem axiom guards pass with only propext, Classical.choice, and Quot.sound. No new admissions or native proof evaluation are introduced.