OAI/Analysis/CircleDomains/Selection/AnchorTruncation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Truncation at a domain point of an anchor preserves the interior cost budget, so an omitted dust endpoint is never charged during attachment.

  1. theorem OAI.CircleDomainRigidity.exists_domain_time_inside_anchor line 18
  2. theorem OAI.CircleDomainRigidity.interiorPhysicalTollCost_affine_le line 38
  3. theorem OAI.CircleDomainRigidity.exists_allowed_suffix_from_anchor line 54
  4. theorem OAI.CircleDomainRigidity.exists_allowed_prefix_to_anchor line 73