OAI/Analysis/CircleDomains/Transfer/RetainedTestCrossings.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Crossing segments for an actual retained test

The source test has value one on an inner retained contour and zero on an outer one. Their actual finite-model images produce the common crossings used in line payment, with anchors derived from source points.

  1. theorem OAI.CircleDomainRigidity.values_on_image_jordan_boundary line 22
  2. theorem OAI.CircleDomainRigidity.eventually_crossings_of_retained_test line 52