OAI/Analysis/CircleDomains/Rigidity/PrincipalAbsentMaskedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite circle models with absent masked coordinates. Closed collars realize absent coordinates by exterior constants. Every original masked differential and every retained value is preserved exactly.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.principal_absent_masked_transfer line 21