OAI/Analysis/CircleDomains/Topology/SubarcPointAvoidance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Point avoidance outside the original law's positive-hit set survives the actual subarc selector and compact conditioning.

  1. theorem OAI.CircleDomainRigidity.IsSubarcLawReduction.avoids_point line 16
  2. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.subarc_avoids_unmarked_point line 35
  3. def OAI.CircleDomainRigidity.RecursiveCodeLaw.extendedHitFlags line 54
  4. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.extendedHitFlags_countable line 60
  5. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.extendedHitFlags_subset line 67
  6. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.target_mem_extendedHitFlags line 77