OAI/Analysis/CircleDomains/Selection/CountableConcatenationTolls.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact toll addition for collar pieces. Junctions lie in the physical domain, hence carry zero dust toll; the new limiting endpoint is omitted.

  1. theorem OAI.CircleDomainRigidity.timeToll_eq_of_zero_difference line 20
  2. theorem OAI.CircleDomainRigidity.timeToll_eq_interior_of_zero_endpoints line 32
  3. theorem OAI.CircleDomainRigidity.collarConcatenation_cell_toll line 46
  4. theorem OAI.CircleDomainRigidity.collarConcatenation_interior_toll line 58