OAI/Analysis/CircleDomains/Transfer/RealGridTransfer.lean

Real-coordinate transfer on the actual finite completion

The geometric completion, actual reciprocal-grid collars and selected wedge cost produce transferred coordinates on the whole completed region and a spherical-background metric with total and localized energy bounds. This assembles the real-coordinate part of finite transfer; periodic coordinates and the terminal oscillation bookkeeping remain separate.