OAI/Analysis/CircleDomains/Modulus/JoinedJunctionCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Joining at a dust point incurs exactly one junction toll. This is the accounting used to replace collapsing jumps by actual paths.

  1. theorem OAI.CircleDomainRigidity.joinedPath_interior_toll_with_junction line 17
  2. theorem OAI.CircleDomainRigidity.interiorPhysicalTollCost_joined_with_junction line 63
  3. theorem OAI.CircleDomainRigidity.exists_allowed_joined_junction_cost line 74