OAI/Analysis/CircleDomains/Rigidity/MaskedModelData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual masked coordinates and metric on one finite circle model. The record retains the exact source and transported energy identities, as well as the filling and core equalities needed by the limiting tests.

  1. structure OAI.CircleDomainRigidity.FiniteTransfer.MaskedModelData line 15