The overlay theorem: an MP bijection nearly achieves the cut distance (Rokhlin campaign, R3) #
This file proves the last live Rokhlin core, exists_mpEquiv_cutNormDiff_lt_add: on an
atomless standard Borel probability space, the cut distance — an infimum over pairs of
measure-preserving maps — is achieved up to any ε > 0 by pulling back one graphon along a
single measure-preserving bijection, leaving the other bare. This is the classical
overlay / bijection-density fact (Borgs–Chayes–Lovász–Sós–Vesztergombi Lemma 3.5, Janson
Theorem 6.9), needed by the completeness telescope in Graphon/Compactness.lean.
It lives in its own file because the proof needs the Frieze–Kannan regularity lemma and the
atomless carving primitives of Graphon/Regularity.lean, which sit downstream of
Graphon/CutDistance.lean in the import graph.
The proof follows docs/overlay-scoping.md §4: no Birkhoff / rational approximation.
For step graphons, the value of any coupling (φ, ψ) is realized exactly by an MP
bijection: the coupling matrix λ_{ik} = μ(φ⁻¹(S_i) ∩ ψ⁻¹(T_k)) has row and column sums
equal to the cell measures, so (atomlessly) both partitions can be refined into cells of
mass exactly λ_{ik}, and exists_controlled_cell_alignment — applied twice, once for the
answer bijection and once for a proof-only transfer — turns the matched refinements into the
required measure-preserving α ≃ᵐ α. The only ε comes from step approximation.
Roadmap (R3) #
- O1
exists_disjoint_subsets_of_measures— carve finitely many disjoint subsets of prescribed masses out of a measurable set;MeasurablePartition.ofCells— assemble a partition from disjoint cells plus a waste cell. - O2 the exact step-overlay transfer (double alignment).
- O3 assembly:
exists_mpEquiv_cutNormDiff_lt_add(relocated here fromGraphon/CutDistance.lean).
O1: prescribed-mass carving and partition assembly #
Prescribed-mass carving. Out of a measurable set C, carve finitely many pairwise
disjoint measurable subsets of any prescribed masses r i with ∑ i, r i ≤ μ C.
This generalizes exists_equal_chunks_inside (equal masses 1/q) to arbitrary prescribed
masses; it is the finite-matrix carving step of the overlay construction
(docs/overlay-scoping.md §4, step 1).
O1: partition from disjoint cells plus a waste cell #
Assemble a MeasurablePartition from finitely many pairwise disjoint measurable cells,
adding the complement of their union as a waste cell. Every input cell is a part
(mem_ofCells_parts).
Equations
- MeasurablePartition.ofCells A hmeas hdisj = { parts := insert (⋃ (i : Fin n), A i)ᶜ (Finset.image A Finset.univ), measurable_parts := ⋯, pairwiseDisjoint := ⋯, ae_covers := ⋯ }
Instances For
Each input cell is a part of MeasurablePartition.ofCells.
O2: the exact step-overlay transfer #
Splitting a measure along the preimages of a partition under a measure-preserving map:
∑_{T ∈ Q.parts} μ (X ∩ ψ⁻¹(T)) = μ X. (With ψ = id and X = univ this recovers that the
part measures of a MeasurablePartition sum to one.)
Two measure-preserving maps that a.e. land in a common part of P pull a stepified
graphon back to the same graphon. This is the transfer engine of the overlay proof: the
stepification only sees which part a point lies in, never the point itself.
The exact step overlay. For step graphons, the cut-norm value of any coupling
(φ, ψ) of measure-preserving maps is achieved exactly by a single measure-preserving
bijection σ, leaving the second graphon bare.
Construction (docs/overlay-scoping.md §4): the coupling matrix
λ_{ik} = μ(φ⁻¹(S_i) ∩ ψ⁻¹(T_k)) has row and column sums equal to the part measures, so
both partitions refine (atomlessly, exists_disjoint_subsets_of_measures) into cells of
mass exactly λ_{ik}. Aligning the positive-mass refined cells twice via
exists_controlled_cell_alignment — σ : T_{ik} → S_{ik} (the answer) and
τ : T_{ik} → φ⁻¹(S_i) ∩ ψ⁻¹(T_k) (a proof-only transfer) — makes φ ∘ τ and σ land in
a common part of P a.e., and ψ ∘ τ and id land in a common part of Q a.e.; then
pullback_stepify_congr plus invariance of cutNormDiff under the bijection τ give the
equality. No rational approximation or Birkhoff matching is needed.
O3: the overlay theorem #
An MP bijection nearly achieves the cut distance (corrected Rokhlin consequence 4).
On an atomless standard Borel probability space, the cut distance — an infimum over pairs of
measure-preserving maps — is achieved up to any ε by pulling back U along a single
measure-preserving bijection, leaving W bare.
This is the honest, true replacement for the false cutDistance_lt_add_of_pos_equiv
(Compactness) whose bijection witness was derived from the unprovable
exists_common_extension_maps. It is genuinely needed by the completeness/compactness
telescope: coherent frames require a bare reference, which forces invertibility (a coupling of
maps cannot make a graphon bare without re-pulling the whole history).
Proof (the overlay argument, docs/overlay-scoping.md): approximate U and W by step
graphons at ε/8 (regularity); take ε/8-optimal maps (φ, ψ) for the original pair
(cutDistance_lt_add_of_pos); realize the coupling value of the step approximations
exactly by an MP bijection (exists_mpEquiv_pullback_stepify_eq); transfer the step
approximation errors through the pullback contraction cutNormDiff_pullback_le and the
bijection invariance cutNormDiff_pullback_measurableEquiv. Total budget 5ε/8 < ε.