Atomic regressions for the map form of the cut distance #
The harder direction of cutDist_eq_cutDistPullback applies Janson's Thm A.9 to the coupling, so
the atomic cases to check are atomic couplings. These three elaboration checks run the equivalence
at a point-mass coupling, at a finitely atomic one, and at one mixing an atomic with a continuous
direction. Each fails to typecheck for any formulation that assumes the carriers, or the coupling,
atomless.
Keeping these roadmap design-validation checks separate avoids adding their Bernoulli dependency
to the canonical CutMetric.Pullback.Basic API module. The repository build includes this module,
so the regressions remain part of the build gate for the contract they test.
References #
- Roadmap:
TauCetiRoadmap/DenseGraphLimits/README.md, the Layer-5 design-validation milestone requiring Dirac, finite-atomic, and mixed regressions againstcutDist_eq_cutDistPullback.