OAI/Analysis/CircleDomains/Selection/PhysicalExitPenalty.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A genuine bounded indicator density pays for a first-exit passage through a relatively compact domain region. The estimate uses physical arclength and remains valid for paths with arbitrary dust contacts elsewhere.

  1. theorem OAI.CircleDomainRigidity.first_exit_indicator_cost_lower_bound line 22