The exact region and an inequality between Chatterjee's and Spearman's rank correlations

Verification map

Status: complete for stated scope. Theorems 1-3, Corollary 1, Propositions 1-5, and Example 1 are checked for the corrected arXiv v3 copula, including all boundary and equality cases. The family has an explicit density, convex topological support, MTP2, asymmetry, all three rank formulas, ordering and uniform limits. Journal equation (19) lacks a necessary boundary term; its literal formula is disproved in Lean. Lemma 8 uses equality almost everywhere. Alternative proofs replace unused optimization and rearrangement intermediates.

Source and conventions

Source: arXiv:2506.15897v3, 19 May 2026. Journal reference: DOI 10.1016/j.jmva.2026.105630; statement comparison and corrections are recorded below.

Xi conditions coordinate 1 on coordinate 0. Equation (3) is matched to the conditional-CDF definition by the almost-everywhere derivative theorem, without a density assumption. FGM uses the full signed parameter interval [-1,1]. CI and CD in the FGM classification assert conditional monotonicity in both directions, so in particular include the direction used by the source. Within this family the equality case is exactly parameter zero. The general SI/SD inequality and its complete equality classification are proved in StochasticBounds.lean and StochasticEquality.lean. The proof constructs an antitone conditional-CDF version from concavity and compares squared differences with absolute differences. Equality makes almost every conditional CDF either constant or binary; monotonicity in the response threshold excludes mixing the two types at interior thresholds. This is an alternative to the source maximum-principle proof, without a density assumption. The source maximum-principle and extreme-point intermediate assertions are not separately claimed verified.

Lemma 8 is formalized modulo null sets: equality holds exactly when the decreasing function is almost everywhere constant v or the indicator of [0,v]. The source phrases its alternatives pointwise, but changes on null sets cannot affect the integral. Endpoint values and the choice between closed and open cut intervals therefore do not affect our statement. The formal version also includes means v=0 and v=1.

For the vertical boundary, a centered countermonotonic block with identity outside has xi=1 and rho=1-2 alpha^3. Varying alpha over [0,1] realizes the entire rho interval. The interior boundary and its explicit formulas are now proved separately below.

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; the full explicit region is now established separately below.

Journal comparison and precise conventions

The author-posted journal text, uploaded by Marcus Rockel on 14 April 2026, was compared with arXiv v3. The region, optimization, SI/SD and rank statements retain their numbering. MTP2 is Proposition 4(ii).

Journal equation (19) omits the term $b\min(a_v,0)^2/2$ present in arXiv v3. At $b=1$, $u=0$, $v=1/8$, its literal expression is $-1/8$. The Lean counterexample proves it cannot be a copula CDF; the corrected formula is proved at every point. Thus completion refers to the corrected arXiv statements, not literal verification of the uncorrected journal formula.

The density uses the open band in equation (23); changing values on its null boundary preserves the law. Topological support includes the boundary, unlike the source's identification with the density's positive set. Both its exact closed band and convexity are proved. Lemma 8's equality alternatives are interpreted almost everywhere.

Result map

Proofs are in SelectedResults.lean, RightBoundary.lean, StochasticBounds.lean, StochasticEquality.lean, RegionGeometry.lean, DiagonalBandUnit.lean, SharpGap.lean, SharpSlice.lean, and BandOptimization.lean, imported by Main.lean. Axioms.lean prints and enforces the standard transitive axiom allowlist for every declaration below.

Completion covers the explicitly mapped corrected statements. Unused proof intermediates, the separate regression-model and measure-inducing interpretations, numerical experiments and plots are not claimed as formal proofs.

Sharp gap and normalized diagonal-band optimization

Corollary 1 is proved independently of the remaining explicit full-region formula. For a clamped candidate D with section clamp(a(v)-b*u,0,1), the scalar projection inequality, followed by the shared marginal constraint, gives

where d squared is the integrated squared difference of conditional CDFs. Its nonnegativity proves global optimality; its zero characterization proves uniqueness of the copula itself. Every competing copula is included, without an absolute-continuity or SI hypothesis.

At b=1 the explicit intercept is sqrt(2v) below v=1/2 and 2-sqrt(2(1-v)) above. Exact integration proves xi=3/10 and rho=7/10, so the maximum gap is 2/5. This finishes Corollary 1. Theorem 1 is now also proved in full by the general formulas and inverse below. The exact xi=3/10 slice also follows by reflection and the already verified convexity theorem.

For general b>=0 the intercept is selected from the proved equation integral clamp(a-b*u,0,1) du=v. The explicit piecewise intercept in equation (20) is proved to satisfy this same equation; support uniqueness identifies the constructed source copula with the normalized optimizer. Exact integration gives both branches of Proposition 5's xi and rho formulas. The trigonometric and radical expressions in equation (5) invert xi on its full interior range. The sharp support bound and convexity then prove every inclusion and witness in the exact region, with uniqueness of both curved boundary copulas.

Parameter ordering follows from equal means and ordered slopes of clamped sections. Radial symmetry follows from uniqueness of the support optimizer. Uniform convergence is quantitative: CDF errors are bounded by b at independence and by 1/b at M or W. These results do not assume a density. The remaining family properties are now proved independently: an exact sampling law evaluates Kendall tau and identifies the topological support; integrating an explicit density gives equality with the source measure. Ordered band endpoints prove MTP2. The support also proves asymmetry for both parameter signs.