OAI/Analysis/CircleDomains/Selection/PriorResidualContacts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pull the actual prior-law residual constraint back to independent samples of the earlier and later code laws.

  1. theorem OAI.CircleDomainRigidity.ae_later_residual_contact_in_prior_support line 18