The exact Spearman rho-footrule region via optimal transport with applications to finite rankings, mixability, and Chatterjee's rank correlation

Verification map

Status: complete for stated scope. The exact rho-footrule and mean-variance regions, finite-ranking inequalities, mixability infimum, and xi/correlation-ratio outer bounds are checked. Example 2.8 has its exact folded-uniform law, xi=1/4 and eta=0. Example 2.9 has a uniform quantitative gap. Proposition 2.10 is checked in full: the lower curve, every localized upper branch, compactness and full projection of the seed set, the attained concave upper envelope, and the entire inner enclosure. Remark 2.2 has the exact finite-ranking equality/divisibility criterion and strict correction away from contact means. Both finite-ranking moment bounds are asymptotically sharp at every admissible mean, via uniform approximation by actual permutation shuffles. The full comparison with the earlier rho-footrule curve is checked: equality on [-1/2,1/4], every contact point and the endpoint, and strict improvement on both line segments of every later contact interval. Compactness of the full xi-eta region and upper-maximum attainment at every xi are checked, including the quantitative quarter-xi maximum. Uniqueness of the optimizing copula is checked on every upper arc, at all junctions, and at the endpoint, including nonsymmetric and singular competitors. The stated main-result scope is complete.

Source and conventions

Source: arXiv:2608.20176v1, 20 August 2026.

The copula is a probability measure with uniform marginals. Rho uses 12 E[UV]-3 and footrule uses 6 integral C(t,t) dt-2. The exact moment identities are rho=1-6 E[(U-V)^2] and footrule=1-3 E[abs(U-V)]. The quadratic envelope follows from nonnegativity of the centered second moment. It is the classical upper bound in equations (16)-(17), not the article's sharper piecewise optimal boundary. No absolute-continuity hypothesis is added.

The contact family uses N equal diagonal blocks of a half-turn shuffle. Its coefficient values reach the universal quadratic bound, which proves global optimality at all discrete contact points without assuming the article's transport correction.

Result map

Proofs are in Moments.lean and Touchpoints.lean, imported by Main.lean. Axioms.lean prints and enforces the standard transitive axiom allowlist for every declaration below.

| Remark 2.2: general finite-ranking approximation | Papers.AnsariRockel2026RhoFootrule.ranking_moment_limits | verified | Every copula admits permutations of sizes N=1,2,... whose D/N^2 and S/N^3 approach its first absolute displacement moment and second moment. Proved by iid rank construction, an explicit uniform CDF rate, and continuity bounds for rho and footrule. | | Remark 2.2: both asymptotically sharp moment bounds | Papers.AnsariRockel2026RhoFootrule.ranking_lower_asymptotic_sharp; Papers.AnsariRockel2026RhoFootrule.ranking_upper_asymptotic_sharp | verified | For each prescribed mean m in [0,1/2], actual finite permutations approach (m,m^2+Vmin(m)) and (m,(1-sqrt(1-2m)^3)/3), respectively. Endpoints are included. Means approach m; exact attainment for each finite size is not asserted. |

The completed scope comprises the mapped main results: Theorem 1.1, Corollary 1.2, Proposition 1.6, Corollary 1.7, Theorems 2.1, 2.4 and 2.6, Examples 2.8 and 2.9, Proposition 2.10, and the mapped refinements and applications. Supporting transport arguments are verified in the concrete forms needed for these conclusions; this does not separately assert every abstract auxiliary statement or externally cited theorem. Numerical experiments and plots are outside the formal scope.

Latest package integration

The dependency is pinned to copula commit 5926399c46f83d307127fd34b3aa2e416c940786. New application modules: MeanVariance.lean, VarianceMaximum.lean, FiniteRankings.lean, CorrelationRatio.lean, Mixability.lean. Every mapped declaration is compiled and transitively audited against the standard Lean axiom allowlist. Uniqueness of a numerical boundary value does not imply uniqueness of its copula witness.

The folded model is proved by an explicit two-uniform sampler and then identified with the stated single-uniform graph law. Exact conditional-CDF integration gives xi=1/4; the constant conditional mean gives eta=0. The quantitative gap uses the endpoint bounds of every conditional CDF, so it does not assume compactness of the attainable set. Independence mixtures scale both xi and eta quadratically and supply the entire horizontal inner segment.

The central-revelation kernel preserves the uniform response marginal by an exact prefix-integral identity. Its conditional-CDF squares and conditional-mean variance give the entire lower inner curve. The upper binary model uses the flat-topped tent min(a,v,1-v), whose first two moments are evaluated exactly. Predictor tagging proves xi-eta convexity directly for arbitrary copulas, without assuming that either coefficient is affine under ordinary copula mixtures.

Proposition 2.10 is now complete. The affine conditional-block model is identified with the imported ordinal-sum copula, so its directional coefficient formulas apply to the package constructor, including singular components. Every upper seed and every point of its convex hull has a genuine copula witness. Compactness of the seed hull proves existence of the displayed inner upper maximum. Independently, laws of conditional distributions with a uniform barycenter form a compact space whose continuous coefficient image is exactly the entire attainable region. This proves full-region compactness and upper-boundary attainment without assuming weak continuity of xi on ordinary copula laws.

Optimizer uniqueness uses the package's exact dual potentials and their sharp Lipschitz bounds. Rademacher differentiability gives a unique upper contact almost everywhere; strict negativity excludes diagonal contact. Decomposing any optimizer into the forward graph and its transpose gives two marginal equations, whose finite-strip recursion identifies both component measures. The proof establishes equality of actual copulas and does not assume symmetry of an optimizer.