RetainedCircleModel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble the actual graded real seed, countable open exclusion selection, common mixed models and their normal limit into a circle uniformization.

structure OAI.CircleDomainRigidity.RetainedRealCircleModel line 29
Source documentation
A circle-domain normal limit with the original finite scalar list retained on the actual finite-transfer exhaustion. Sobolev continuation of its traces is a separate conclusion proved from these data.
```
structure RetainedRealCircleModel (base : PathCodeData Sphere Sphere) (π : Sphere → Sphere)
    {m : ℕ} (Q : Fin m → PhysicalRealCoordinate base π) where
…
```
Mentions: OAI.CircleDomainRigidity.PathCodeData, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.PhysicalRealCoordinate
theorem OAI.CircleDomainRigidity.exists_retained_real_circle_model line 43