Article supplement / 2026

The exact region determined by Spearman's rho and Gini's gamma

Jonathan Ansari · Marcus Rockel · Stefanie Steinmaßl

arXiv preprint

arXiv:2609.19890v1 ↗Source folder ↗Lean module ↗

Complete for stated scope

Theorem 1.1, Corollaries 2.1 and 2.4, Remark 2.2, Proposition 2.3, Lemmas 3.1-3.7, Definition 3.8, Proposition 3.9, Example 3.10, Lemma 4.1 and Theorem 4.2 are checked. This includes the original theta formulas, all junctions and endpoint limits, full parameter coverage, exact shuffle graph laws, the uniform cubic asymptotic and attained strong duality for every positive multiplier.

Stable identifier: AnsariRockelSteinmassl2026RhoGamma
Source for numbering: arXiv:2609.19890v1
Lean entry point: Papers.AnsariRockelSteinmassl2026RhoGamma.Main

Verification map

Status: complete for stated scope. Theorem 1.1, Corollaries 2.1 and 2.4, Remark 2.2, Proposition 2.3, Lemmas 3.1-3.7, Definition 3.8, Proposition 3.9, Example 3.10, Lemma 4.1 and Theorem 4.2 are checked. This includes the original theta formulas, all junctions and endpoint limits, full parameter coverage, exact shuffle graph laws, the uniform cubic asymptotic and attained strong duality for every positive multiplier.

Source and conventions

Source: arXiv:2609.19890v1, 17 September 2026.

The pair is ordered (rho,gamma). Rho=12 E[UV]-3 and gamma=4 integral (C(t,t)+C(t,1-t)) dt-2. The moment formula proves gamma=2 E[abs(U+V-1)-abs(U-V)]. Reflection of the second coordinate negates both coefficients. The set-theoretic convexity and central-symmetry proofs apply to the actual attainable set, independently of any unproved boundary formula. Both directions of the sign-magnitude representation are checked below. The converse accepts an arbitrary probability space and a measurable Boolean sign; true represents +1 and false represents -1. The joint law is recovered, with zero-magnitude events proved null.

Result map

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

Source result	Lean declaration	Status	Hypotheses and scope
Lemma 3.1, equation (28): moment identities	`Papers.AnsariRockelSteinmassl2026RhoGamma.moment_representation`	verified	All copulas; both directions of the sign-magnitude representation are checked separately below.
Theorem 1.1 proof: one-coordinate reflection	`Papers.AnsariRockelSteinmassl2026RhoGamma.reflection_pair`	verified	Second-coordinate reflection negates rho and gamma.
Theorem 1.1 proof: fixed-gamma interpolation	`Papers.AnsariRockelSteinmassl2026RhoGamma.fixed_gamma_intermediate`	verified	Supplied copulas share gamma and bracket the target rho; no optimal-boundary assertion.
Theorem 1.1: convexity of the attainable set	`Papers.AnsariRockelSteinmassl2026RhoGamma.region_convex`	verified	Actual coefficient range over all bivariate copulas.
Theorem 1.1: central symmetry of the attainable set	`Papers.AnsariRockelSteinmassl2026RhoGamma.region_centrally_symmetric`	verified	Every attainable (rho,gamma) has attainable (-rho,-gamma).
Lemma 3.1: uniform magnitudes	`Papers.AnsariRockelSteinmassl2026RhoGamma.rankMagnitude_uniform`; `Papers.AnsariRockelSteinmassl2026RhoGamma.magnitude_marginal`	verified	The map u to abs(2u-1) preserves uniform measure; both magnitudes under every copula are uniform. Their joint law defines magnitudeCopula.
Lemma 3.1, equation (29): pointwise identities and moments	`Papers.AnsariRockelSteinmassl2026RhoGamma.sign_product_identity`; `Papers.AnsariRockelSteinmassl2026RhoGamma.sign_min_magnitude_identity`; `Papers.AnsariRockelSteinmassl2026RhoGamma.sign_magnitude_rho`; `Papers.AnsariRockelSteinmassl2026RhoGamma.sign_magnitude_gamma`	verified	Rho=3 E[SAB] and gamma=2 E[S min(A,B)] under the original copula law; sign is zero on median lines. The converse is checked in the following rows.
Equation (30): supporting functional and magnitude bound	`Papers.AnsariRockelSteinmassl2026RhoGamma.supporting_functional`; `Papers.AnsariRockelSteinmassl2026RhoGamma.supporting_functional_le`	verified	Every copula with its actual magnitude law; both statements hold for every real multiplier t, hence in particular t>=0.
Lemma 3.3(i): weak duality	`Papers.AnsariRockelSteinmassl2026RhoGamma.transport_weak_duality`	verified	Any continuous feasible potential and any uniform-marginal copula; no optimizer or strong duality is assumed.
Lemma 3.3(ii): contact-set certificate	`Papers.AnsariRockelSteinmassl2026RhoGamma.transport_contact_value`; `Papers.AnsariRockelSteinmassl2026RhoGamma.transport_contact_optimal`	verified	Almost-everywhere contact proves the exact value, optimality over all couplings and optimality over all continuous feasible potentials.
Lemma 3.5, theta<=1: explicit dual potential	`Papers.AnsariRockelSteinmassl2026RhoGamma.halfShiftPotential_zero`; `Papers.AnsariRockelSteinmassl2026RhoGamma.halfShiftPotential_integral`; `Papers.AnsariRockelSteinmassl2026RhoGamma.halfShiftPotential_feasible`	verified	s=1/theta>=1. The potential has the source formula, normalization and integrated value; its dual inequality holds on the whole square.
Lemma 3.5, theta<=1: potential regularity	`Papers.AnsariRockelSteinmassl2026RhoGamma.halfShiftPotential_lipschitz`; `Papers.AnsariRockelSteinmassl2026RhoGamma.halfShiftPotential_deriv_bound`	verified	Lipschitz constant s-1, with a derivative bound for the same formula extended to the real line. Includes s=1.
Lemma 3.5 and sufficient direction of Lemma 3.6	`Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_cost`; `Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_optimal`; `Papers.AnsariRockelSteinmassl2026RhoGamma.halfShiftPotential_contact`	verified	The constructed half-turn copula attains cost 1/4-s/2 and potential equality almost everywhere; it is globally optimal for s>=1. The converse for s<1 is checked below.
Lemma 3.1 converse: complete joint-law realization	`Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_joint_law`; `Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_magnitude_law`	verified	Any probability space with two measurable uniform magnitudes and an arbitrary measurable sign, including conditional randomness. The constructed copula recovers the joint magnitude/sign law, not only its moments; zero magnitudes are null.
Lemma 3.1 converse: coefficient identities	`Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_rho`; `Papers.AnsariRockelSteinmassl2026RhoGamma.signCopula_gamma`	verified	The constructed copula has rho=3 E[SAB] and gamma=2 E[S min(A,B)] under the supplied law.
Lemma 3.2: sign-bound attainment	`Papers.AnsariRockelSteinmassl2026RhoGamma.signOptimizer_magnitude`; `Papers.AnsariRockelSteinmassl2026RhoGamma.signOptimizer_value`; `Papers.AnsariRockelSteinmassl2026RhoGamma.sign_bound_attained`	verified	For every magnitude copula D and every real t, an explicit sign choice produces a copula with magnitude law D and supporting value 3 integral c_t dD.
Equation (32): equivalence of optimization bounds	`Papers.AnsariRockelSteinmassl2026RhoGamma.supporting_bound_iff_transport_bound`; `Papers.AnsariRockelSteinmassl2026RhoGamma.transport_optimizer_lifts`	verified	Every real t; equivalent upper-bound problems, and every optimal magnitude coupling yields an optimal copula.
Equations (31)-(32): existence and equality of attained maxima	`Papers.AnsariRockelSteinmassl2026RhoGamma.transportValue_attained`; `Papers.AnsariRockelSteinmassl2026RhoGamma.supporting_maximum`	verified	Uniform-marginal measures form a weakly compact set and the cost is continuous. Both maxima exist, and the support maximum is exactly three times the independently defined transport supremum; no optimizer is assumed.
Lemma 3.3(ii): attained supporting-line certificate	`Papers.AnsariRockelSteinmassl2026RhoGamma.transport_contact_support`	verified	Any continuous feasible potential and supplied magnitude copula with almost-everywhere contact give a universal supporting bound and a constructed copula attaining it.
Theorem 1.1 / Proposition 3.9: explicit boundary construction and coefficients	`Papers.AnsariRockelSteinmassl2026RhoGamma.boundary_coefficients`; `Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_parameter`	verified	All arithmetic half-shift and left/right branches, plus W and M. No optimizer is supplied by the caller.
Theorem 1.1: both universal bounds and boundary attainment	`Papers.AnsariRockelSteinmassl2026RhoGamma.sharp_upper_bound`; `Papers.AnsariRockelSteinmassl2026RhoGamma.sharp_lower_bound`; `Papers.AnsariRockelSteinmassl2026RhoGamma.upper_boundary_attained`; `Papers.AnsariRockelSteinmassl2026RhoGamma.lower_boundary_attained`	verified	Every gamma in [-1,1], including both endpoints; all bivariate copulas are allowed.
Theorem 1.1, equation (6): full exact region	`Papers.AnsariRockelSteinmassl2026RhoGamma.exact_region`	verified	Both directions for the actual (rho,gamma) range. Reflection gives the lower boundary and fixed-gamma mixtures attain every interior point.
Theorem 1.1: compactness	`Papers.AnsariRockelSteinmassl2026RhoGamma.region_compact`	verified	The actual region is a continuous image of the compact set of uniform-marginal probability measures.
Theorem 1.1: boundary shape and endpoint values	`Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_concave`; `Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_strictMono`; `Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_endpoints`	verified	Concavity and strict increase throughout [-1,1], with boundary values -1 and 1.
Theorem 1.1: boundary continuity including limiting endpoints	`Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_continuous`	verified	Continuity on the full closed interval; endpoint limits use compactness and the unique copulas at gamma=+/-1.
Theorem 1.1: consistency at all arc junctions	`Papers.AnsariRockelSteinmassl2026RhoGamma.boundary_value_unique`	verified	Coincident gamma parameters have exactly the same rho boundary value.
Lemma 4.1 / Theorem 4.2: glued potential and sharp support	`Papers.AnsariRockelSteinmassl2026RhoGamma.glued_dual_feasible`; `Papers.AnsariRockelSteinmassl2026RhoGamma.sharp_supporting_bound`	verified	The package constructs AuxiliaryCertificate instances for every half-shift, left and right branch. The global potential inequality and attained supporting bound apply to each such instance.
Corollary 2.1: elementary arc formulas	`Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_arc_coefficients`; `Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_arc_closed`	verified	Exact polynomial formulas in d=z/2 and the radical expression in gamma, for every s>=1.
Corollary 2.1: full elementary-arc coverage and scalar boundary	`Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_arc_coverage`; `Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_upper_boundary`	verified	Every gamma from -1 through the first contactGamma(1); W is handled separately at -1.
Proposition 2.3: exact maximizing point and supporting multiplier	`Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancy_coefficients`; `Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancy_support_slope`; `Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancy_value`	verified	The constructed optimizer has d=(14-2sqrt(10))/39 and supporting multiplier one; its rho-gamma value is (1064+160sqrt(10))/4563.
Proposition 2.3: sharp absolute largest discrepancy	`Papers.AnsariRockelSteinmassl2026RhoGamma.rho_sub_gamma_le`; `Papers.AnsariRockelSteinmassl2026RhoGamma.abs_rho_sub_gamma_le`; `Papers.AnsariRockelSteinmassl2026RhoGamma.maximal_discrepancy_attained`	verified	Universal bound and actual attainment; reflection supplies the opposite signed discrepancy.
Corollary 2.4: exact zero slices	`Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_zero`; `Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_neg_gammaThreshold`; `Papers.AnsariRockelSteinmassl2026RhoGamma.zero_gamma_slice`; `Papers.AnsariRockelSteinmassl2026RhoGamma.zero_rho_slice`	verified	At gamma=0 exactly abs(rho)<=(144+9sqrt(6))/500; at rho=0 exactly abs(gamma)<=(72-3sqrt(69))/169. Both slice endpoints are attained.
Corollary 2.4: sharp sign thresholds	`Papers.AnsariRockelSteinmassl2026RhoGamma.same_sign_of_abs_rho_gt`; `Papers.AnsariRockelSteinmassl2026RhoGamma.same_sign_of_abs_gamma_gt`	verified	Above either strict absolute threshold the product rho*gamma is positive. The attained zero slices establish sharpness.
Lemma 3.6: full half-shift regime	`Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_not_optimal`; `Papers.AnsariRockelSteinmassl2026RhoGamma.halfShift_optimal_iff`	verified	For positive s=1/theta, the half-shift is optimal iff s>=1. For 0<s<1 an explicit finite-path copula has strictly smaller cost.
Remark 3.4: all positive multipliers	`Papers.AnsariRockelSteinmassl2026RhoGamma.supporting_slope_covered`; `Papers.AnsariRockelSteinmassl2026RhoGamma.transport_primal_dual_attained`; `Papers.AnsariRockelSteinmassl2026RhoGamma.transport_strong_duality`; `Papers.AnsariRockelSteinmassl2026RhoGamma.transportValue_eq_dual_infimum`	verified	Constructed primal and continuous symmetric dual optimizers for every t>0; the dual infimum equals the primal supremum without a supplied certificate.
Equation (18) and Lemma 3.7: source normalization	`Papers.AnsariRockelSteinmassl2026RhoGamma.source_splitting_formulas`; `Papers.AnsariRockelSteinmassl2026RhoGamma.source_parameter_inequalities`; `Papers.AnsariRockelSteinmassl2026RhoGamma.source_alpha_matching`	verified	Exact theta=1/s and alpha normalization, matching equation, and all source parameter inequalities for every branch certificate.
Equations (16)-(17): both finite branches	`Papers.AnsariRockelSteinmassl2026RhoGamma.right_source_data`; `Papers.AnsariRockelSteinmassl2026RhoGamma.left_source_data`	verified	The original signed delta, first and second distance moments, and endpoint potential value agree with the library formulas.
Lemma 3.5 / equations (15)-(17): original theta-indexed construction	`Papers.AnsariRockelSteinmassl2026RhoGamma.thetaCertificate_s`; `Papers.AnsariRockelSteinmassl2026RhoGamma.thetaCertificate_data`; `Papers.AnsariRockelSteinmassl2026RhoGamma.sourceTheta_thetaCertificate`	verified	For every theta>0 the construction uses N=floor(theta) and the source midpoint branch selection; its multiplier, moments and endpoint potential are exact.
Theorem 1.1 / Proposition 3.9: original theta boundary formulas	`Papers.AnsariRockelSteinmassl2026RhoGamma.theta_splitting`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_boundary_coefficients`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_boundary_maximizes`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_boundary_value`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_parameter_inequalities`	verified	Equations (18)-(19) give the actual copula coefficients and attained global maximum for every theta>0.
Example 3.10: exact five-piece graph identification	`Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_shuffle_support`; `Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_shuffle_graph`; `Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_shuffle_law`; `Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_shuffle_measurePreserving`	verified	Equality of the constructed copula measure with the source graph map, with the stated endpoint convention; the map preserves the uniform law.
Equation (20) / Example 3.10: full parameter range	`Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_endpoint_constants`; `Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_d_coverage`; `Papers.AnsariRockelSteinmassl2026RhoGamma.five_piece_shuffle_realizes_boundary`	verified	Exact d-star and g-star radicals; every 0<d<=d-star occurs, with the graph law and both polynomial rank coefficients.
Remark 2.2 / equation (23): uniform endpoint expansion	`Papers.AnsariRockelSteinmassl2026RhoGamma.upper_boundary_cubic_remainder`; `Papers.AnsariRockelSteinmassl2026RhoGamma.upper_boundary_asymptotic`	verified	The source big-O statement as gamma approaches 1 from below follows from an explicit uniform cubic remainder bound on all arcs.
Theorem 1.1: continuity across all source theta junctions	`Papers.AnsariRockelSteinmassl2026RhoGamma.continuous_thetaInput`; `Papers.AnsariRockelSteinmassl2026RhoGamma.continuous_theta_coordinates`; `Papers.AnsariRockelSteinmassl2026RhoGamma.continuous_theta_coordinates_nonnegative`	verified	Both midpoint and integer joins are checked; the original coordinate pair is continuous on every finite nonnegative theta, including zero.
Remark 2.2: explicit integer junctions	`Papers.AnsariRockelSteinmassl2026RhoGamma.thetaAlpha_integer`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_integer_coordinates`	verified	For every integer N>=1, alpha=(2+sqrt(3))/4 and both G(N), P(N) agree with the source closed formulas.
Theorem 1.1 / Remark 2.2: both limiting endpoints	`Papers.AnsariRockelSteinmassl2026RhoGamma.thetaG_tendsto_atTop`; `Papers.AnsariRockelSteinmassl2026RhoGamma.thetaG_tendsto_zero`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_coordinates_tendsto_atTop`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_coordinates_tendsto_zero`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_coordinates_zero`	verified	The full original parametrization tends to (-1,-1) at zero and (1,1) at infinity; the zero formulas have exactly the stated endpoint value.
Theorem 1.1: full source-parameter coverage	`Papers.AnsariRockelSteinmassl2026RhoGamma.theta_gamma_coverage`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_gamma_full_range`	verified	Every interior gamma is attained by a positive finite theta; the two endpoint conventions complete exactly [-1,1].
Lemma 3.5 / equations (34)-(37): original auxiliary potential	`Papers.AnsariRockelSteinmassl2026RhoGamma.thetaCertificate_width`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_auxiliary_potential`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_potential_derivative`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_discriminant_inequalities`	verified	The source width, endpoint normalization, global feasible inequality, almost-sure contact and almost-everywhere differentiability with the stated derivative bound are checked.
Section 2.1: complete distance law and junction mass	`Papers.AnsariRockelSteinmassl2026RhoGamma.theta_distance_distribution`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_atom_mass_bounds`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_delta_bound`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_midpoint_atom_zero`	verified	The law is an atom of mass p at ell plus a uniform interval component of mass 1-p. Equality holds against every continuous test function. Both weights, the delta bound and vanishing midpoint atom are checked.
Definition 3.8: exact probability construction	`Papers.AnsariRockelSteinmassl2026RhoGamma.glued_copula_probability_law`	verified	Equality of probability measures with the source lower diagonal/opposite-sign block and upper auxiliary/equal-sign block, each randomized by a fair common sign.
Theorem 4.2 / equations (46)-(47): original theta support values	`Papers.AnsariRockelSteinmassl2026RhoGamma.theta_transport_value`; `Papers.AnsariRockelSteinmassl2026RhoGamma.theta_supporting_inequality`	verified	Exact equality of the attained primal, dual and source supporting values, and the universal supporting inequality for every copula.

There are no pending rows within the declared scope. The numbered mathematical results, original boundary parametrization and its stated consequences are mapped above. A source audit on 24 September 2026 checked the 17 labeled results of arXiv v1 against this map, including Remark 3.4 (strong duality); 118 declarations are listed in Axioms.lean. The source construction is identified at the level of probability measures. Numerical experiments and plots are not counted as formal proofs.

Additional proof modules: SignMagnitude.lean, Transport.lean, HalfShift.lean, SignConverse.lean, SignAttainment.lean.

Latest package integration

The dependency is pinned to copula commit 72a596ebd8c111cb11a046be0d5c5cd64a878954. New proof modules: ExactRegion.lean, BoundaryGeometry.lean, SharpDiscrepancy.lean, SignThresholds.lean, ElementaryArc.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.

Validation on 24 September 2026

The full root build completed successfully (4,622 jobs) with Lean 4.34.0 and the dependency pin above, including this paper's 118 printed and asserted coverage declarations. The root coverage checker, its seven regression tests, and the handbook link/search checks also passed. There are no pending rows within this paper's stated scope.

Inspect the formalization

DefinitionsGenerated Lean documentation →MainGenerated Lean documentation →AxiomsGenerated Lean documentation →

Reproduce this snapshot

Run the full project build to check every source file. The pinned toolchain and dependencies live at the repository root.

git clone https://github.com/Corrram/lean-verifications.git
cd lean-verifications
git checkout --detach 0ac8668a9c4c9007ec374694abc14296edbeae75
lake exe cache get
lake build

Cite this supplement

Use the permanent folder at commit 0ac8668 to identify the exact software snapshot. Cite the original article separately. This handbook follows the latest deployed commit.

Article bibliography (BibTeX)

@misc{AnsariRockelSteinmassl2026RhoGammaArxiv,
  author = {Ansari, Jonathan and Rockel, Marcus and Steinma{\ss}l, Stefanie},
  title = {The exact region determined by Spearman's rho and Gini's gamma},
  year = {2026},
  eprint = {2609.19890},
  archivePrefix = {arXiv},
  primaryClass = {math.ST},
  note = {Version 1, 17 September 2026},
  url = {https://arxiv.org/abs/2609.19890v1}
}

% Cite the Lean supplement separately using its folder and full commit permalink.