OAI/Analysis/CircleDomains/Transfer/RealTransferStage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Data retained from one actual real finite transfer

This record keeps the geometric and analytic outputs needed by the countable model sequence. Its existence is proved by the assembled construction, with the same explicit published inputs.

  1. structure OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_real_transfer_stage line 68