SingleDustJunction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Replace two true-path sequences meeting at a collapsing dust junction. Both outer anchors stay in the domain; the junction is paid exactly once.

theorem OAI.CircleDomainRigidity.exists_path_through_single_dust_junction line 21