FiniteMixedModel.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The same principal model transports both the real barriers and the masked circle coordinates, with exact energy identities for each.

theorem OAI.CircleDomainRigidity.FiniteTransfer.finite_metric_model_with_mixed_fillings line 14