OAI/Analysis/CircleDomains/Selection/FirstExitFragmentProperties.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Frontier endpoints and vanishing endpoint tolls for actual first-exit fragments. These discharge the geometric premises of fragment splicing.

  1. theorem OAI.CircleDomainRigidity.firstExitFragmentArray_frontiers line 19
  2. theorem OAI.CircleDomainRigidity.firstExit_toll_zero line 40