OAI/Analysis/CircleDomains/Topology/SeparatingChainPotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual truncated chain distance separates the anchor and terminal collar, obeys every true-path cost inequality, and has pointwise dust bands bounded by four times the original toll. No barrier function is assumed.

  1. theorem OAI.CircleDomainRigidity.exists_separating_chain_potential line 25