Documentation

TauCeti.Combinatorics.DenseGraphLimits.CutMetric.Pullback.Validation

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 #