On the exact region between Chatterjee's rank correlation and Spearman's footrule

Verification map

Status: complete for corrected stated scope. Theorems 2.1, 2.4, 3.2, and 3.4, Propositions 2.2, 3.1, and 3.5, and Corollary 2.5 are checked. Theorem 3.3's convexity, entire xi=1 boundary, fixed-footrule interpolation, and exact nonnegative-footrule region are verified. Its inverse lower estimate is checked for footrule in [-1/2,0], with parameter uniqueness on [0,2]. Remark 2.3's asymmetric SI equality example is constructed and checked, including its derivative, xi=footrule=1/2, and asymmetry. The two-parameter density construction is checked on the full closed parameter square, including its independence and checkerboard endpoints. The full region is now proved closed and compact, and every boundary slice attains its extremum. The arXiv v1 LTD example is proved not LTD; the corrected example printed in the final JCAM article is verified with exact ranks. The exact lower-semilinear region is proved independently of stochastic increase. Finite nested ordinal sums of independence and comonotonic blocks are now proved SI and symmetric with xi=footrule; SI is also preserved by binary ordinal sums, and the interior equality converse is checked for SI components. Adjacent countable sums of independence blocks are now proved symmetric with binary splits at every partition endpoint, an exact Pi first component, a recursive tail decomposition, stochastic increase, and xi=footrule equality. For arbitrary adjacent countable blocks, SI and exchangeability hold exactly when they hold in each block; in the SI class xi=footrule also holds exactly when it holds in each block. In particular, every adjacent countable Pi/M sum is symmetric, SI and has xi=footrule. The arbitrary-interval converse cited from [15, Thm. 5.1] in final JCAM Remark 1 is external and outside this formal scope. Every original named result in the corrected stated scope is matched to the final JCAM PDF in SOURCE_COMPARISON.md.

Source and proof scope

Source: arXiv:2509.07232v1. Selected final JCAM statements are compared in SOURCE_COMPARISON.md.

The proof uses an exact squared-distance identity for conditional CDFs: for the Fréchet mixture $D_a=(1-a)\Pi+aM$,

Nonnegativity gives the bound. Vanishing distance identifies the copula, which proves uniqueness, including the endpoints. This is an alternative proof of the result: it does not claim to formalize the paper's KKT argument or its general optimization lemmas.

Source correspondence

The copula is represented as a probability measure with uniform marginals. The explicit CDF of the extremizing family is proved below. Footrule is $6\int_0^1 C(t,t)\,dt-2$, with range $[-1/2,1]$. Xi conditions coordinate 1 on coordinate 0. The derivative formula from equation (1) is checked via the almost-everywhere fundamental theorem of calculus; no density assumption is added. The auxiliary constant extension of a CDF section outside $[0,1]$ has the same derivative in the interior; the two endpoints have zero measure.

The lower endpoint has an independent proof through the sharp xi-beta theorem in the companion supplement; the source checkerboard is identified by its explicit CDF. This avoids assuming a general checkerboard approximation inequality.

For Proposition 2.2, the equality case of the scalar diagonal moment bound is proved by a nonnegative algebraic defect. At almost every response threshold, it forces the antitone conditional-CDF section to take only the values 1, one intermediate level, and 0 almost everywhere. The canonical cut functions are the lengths of its one and positive level sets. Monotonicity in the response threshold proves that both cuts are nondecreasing and hence measurable. The uniform marginal determines the measurable middle level, with coincident cuts handled separately. The representation uses precisely the source's open intervals and nested almost-everywhere quantifiers. Both necessity and sufficiency are proved, including the first-partial-derivative formulation. No density assumption is imposed. The source's Lebesgue-Stieltjes integration-by-parts argument is not separately claimed verified.

For Theorem 3.2, a two-bin squared-distance identity proves the Jensen bound and its almost-everywhere equality criterion. An exact quadratic remainder proves that the source's piecewise pair is the global minimizer of the relaxed scalar problem, uniquely at every interior response threshold. The profile is measurable and feasible for all mu in [0,2], including the cutoff and parameter endpoints. Integrating the estimate proves the universal weighted bound for arbitrary copulas. The relaxed coefficients are defined by the exact kernel/CDF integrals with the source's normalization; Proposition 3.1's logarithmic closed forms, strict monotonicity, continuity, and endpoint values are now evaluated from those same integrals. This independent proof does not assert the source KKT argument separately.

The relaxed primitive is deliberately a real-valued function rather than a copula. A formal counterexample at mu=2 proves that it decreases in the second coordinate: its values at (3/10,1/5) and (3/10,3/10) are respectively 1/40 and 0. Thus the proved relaxed lower bound does not claim copula attainment.

The parameter inversion in Theorem 3.3 is proved for footrule y in [-1/2,0], with a unique parameter mu in [0,2]. This restriction matters: at y=-1/2 the cubic factors as (mu-2)^2(mu+1), so its real roots are not globally unique. The formal counterexample below records the correction to the source wording. The inverse estimate does not assert that the relaxed profile attains the copula boundary.

Convexity is proved independently of the curved boundary formulas. A first copula mixture preserves the desired affine coefficient and gives xi no larger than the target convex combination. A second mixture with a proved xi=1 witness at the same coefficient reaches the target xi by continuity. Both steps construct actual copulas, including singular laws and endpoint weights. This also proves attainment of every xi between an existing point and 1 at fixed coefficient; closedness and attainment of slice extrema are proved separately below.

Result map

Source references use arXiv v1 unless explicitly marked as JCAM resubmission or final JCAM; see SOURCE_COMPARISON.md. Proofs are in Definitions.lean, UpperBoundary.lean, LowerEndpoint.lean, SIRegion.lean, SIEquality.lean, AsymmetricEquality.lean, LowerBound.lean, ClosedCoefficients.lean, RegionGeometry.lean, TwoParameter.lean, ClosedRegion.lean, and LTDExample.lean. Axioms.lean prints and enforces the transitive axiom allowlist.

Exact Frechet optimization and the Table 2 parameter convention

FrechetMinimum.lean proves the analytic Frechet row of Table 2 exactly, and strengthens its minimum to the full Frechet simplex. The minimizing copula is (3/4)Pi+(1/4)W, with xi=1/16 and footrule=-1/8. The printed parameter 0.25 therefore denotes the W weight. In the prose convention lambda*Pi+(1-lambda)*W, the corresponding parameter is lambda=3/4. The other numerical table rows and plotted candidate boundaries remain excluded from verified claims. This family minimum does not establish the global negative-footrule boundary. The two-parameter construction is separately proved above.

Two-parameter density and null fibers

TwoParameter.lean proves Proposition 3.5 from the actual probability law with uniform density outside the exclusion band. Its first marginal is uniform; its second marginal is atomless with the density in equation (31). Applying that marginal's CDF gives a copula, and a proved almost-everywhere quantile inverse identifies its density with equation (32). This avoids assuming a strictly positive marginal density or differentiable inverse. Density values on null fibers are immaterial to the measure, so the proof does not claim the paper's pointwise marginal-density cancellation at zero denominators. The finite-mu path is admissible; its numerical objective values and suggested near-optimality remain numerical evidence.

Closedness and attained slice extrema

ClosedRegion.lean gives an independent proof of closedness. Finite predictor-bin averages give lower xi approximations that converge to xi for every copula and are continuous under pointwise CDF convergence. This proves lower semicontinuity. A weakly convergent copula subsequence preserves uniform marginals and footrule, and fixed-footrule interpolation raises xi to the desired limit. Compactness then proves that every vertical and horizontal slice attains its lower endpoint. No explicit negative-boundary formula is inferred.

Correction to Remark 2.6(d)

The arXiv v1 source's printed matrix (1/12)*[[4,0,0],[0,1,3],[0,3,1]] has the advertised ranks but is not LTD. Its CDF at (2/3,2/3) is 5/12, which is strictly below (2/3)*(2/3)=4/9, contradicting the PQD condition implied by LTD. This discrepancy is proved in Lean, not inferred from a plot.

The replacement (1/9)*[[3,0,0],[0,1,2],[0,2,1]] is proved LTD and has xi=38/81 and footrule=10/27, so it establishes the intended strict counterexample. The proof checks the LTD inequality for all thresholds and computes both coefficients exactly. The arXiv v1 false LTD assertion is not advertised as verified.

Lower-semilinear region

LowerSemilinearRegion.lean proves Remark 2.6(c). The shared definition uses the usual diagonal representation: q(t)=delta(t)/t for positive t, and q(t)/t=delta(t)/t^2 is nonincreasing. The value at zero is immaterial. Copula margins and monotonicity supply the remaining diagonal constraints. The proof bounds each conditional CDF by q(v), then integrates its square to obtain xi<=footrule. This applies to LSL copulas without an SI assumption. Both extremal families are LSL, and their mixtures at fixed footrule attain every point between the two boundaries.