The arbitrary-carrier coupling-cost triangle #
Step 5b of the step-approximation programme (#107 remains open): the assembly.
Everything here is at the level of the coupling cost at fixed couplings — the cut-norm difference of the two pullbacks. No infimum over couplings is taken, so nothing here is a statement about a coupling distance; this repository does not define a cross-carrier one.
cutNormDiff_gluedOuterCoupling_le — the finite-level cost triangle: on standard-Borel
factors,
the cost of the glued outer coupling is at most the sum of the two input costs. Every cost is
pulled back to the glued triple law, where a single cutNormDiff_triangle applies; the
cross-carrier isometry identifies each pulled-back cost with the original one, so no error is
incurred by the transport.
The standard-Borel hypothesis here is discharged at the point of use by the finite factors
of FiniteFactorApproximation; the graphon carriers themselves stay arbitrary.
The coupling-cost triangle at the factor level. The cost of the glued outer coupling is at
most the sum of the two input costs — exactly, with no error term. All three costs are pulled
back to the glued triple law, where one application of cutNormDiff_triangle finishes; the
cross-carrier isometry (cutNormDiff_pullback_eq_measurePreserving) identifies each pulled-back
cost with the corresponding original, so the transport is lossless.
The arbitrary-carrier coupling-cost triangle. Given couplings of
(U₁, U₂) and (U₂, U₃) and a finite-factor approximation of each graphon — with the same
approximation of the middle graphon used on both sides — there is a coupling of (U₁, U₃) whose
cost is at most the sum of the two given costs plus 2 * (e₁ + e₂ + e₃).
The carriers Ω₁, Ω₂, Ω₃ are arbitrary probability spaces: no standard-Borel hypothesis.
Gluing happens on the finite factors, where standard Borel is automatic. The chain is: push both
couplings to the finite factors (their middle marginals agree precisely because the middle
approximation is shared), glue there, lift the glued factor law back to the carriers by
countableFactorLift, transport the cost exactly, and pay one approximation error at each of the
three cost comparisons — (e₁ + e₃) + (e₁ + e₂) + (e₂ + e₃) = 2 * (e₁ + e₂ + e₃).
The coupling-cost triangle up to an arbitrarily small error. No approximation data is
supplied: exists_finiteFactorApproximation is invoked at scale ε / 6 for each graphon, and
the three shared errors contribute 2 * (ε/6 + ε/6 + ε/6) = ε. The middle graphon's
approximation is chosen once and reused on both sides, which is what makes the two factor laws
share a middle marginal and lets them be glued.