OAI/Analysis/CircleDomains/Rigidity/AssembledMaskedModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One actual grid, all terminal and filling caps, the common metric, and the principal finite model are constructed from the original masked coordinates. The boundary graphs are used only through their proved compatibility and the local real branches.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.physicalMask line 19
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_assembled_masked_model line 22