Article supplement / 2026

The exact region between Chatterjee's ξ and Blomqvist's β

Jacob Israel Orenday Lares · Marcus Rockel

arXiv preprint

arXiv:2606.30033v2 ↗Source folder ↗Lean module ↗

Complete for stated scope

Theorems 1.1 and 1.2, Lemmas 2.1, 5.1 and 5.2, Propositions 3.1, 3.2, 4.1, 4.2 and 5.3, Corollary 4.3, Remarks 3.3 and 5.4, the identities (2.2)-(2.4), (5.1)-(5.5), and the quantitative claims of the Introduction and Figure 1 are checked. This includes both exact regions (all copulas and stochastically increasing/decreasing copulas), the explicit interval-exchange copulas D_b and two-branch copulas R_b, all listed tent-copula properties, and density TP2/RR2 under arbitrary nonnegative measurable versions.

Stable identifier: OrendayLaresRockel2026XiBeta
Source for numbering: arXiv:2606.30033v2
Lean entry point: Papers.OrendayLaresRockel2026XiBeta.Main

Verification map

Status: complete for stated scope. Theorems 1.1 and 1.2, Lemmas 2.1, 5.1 and 5.2, Propositions 3.1, 3.2, 4.1, 4.2 and 5.3, Corollary 4.3, Remarks 3.3 and 5.4, the identities (2.2)-(2.4), (5.1)-(5.5), and the quantitative claims of the Introduction and Figure 1 are checked. This includes both exact regions (all copulas and stochastically increasing/decreasing copulas), the explicit interval-exchange copulas D_b and two-branch copulas R_b, all listed tent-copula properties, and density TP2/RR2 under arbitrary nonnegative measurable versions.

Source and conventions

Source: arXiv:2606.30033v2, 29 September 2026 (numbering as in v2; v1 numbered the same results differently, e.g. v1 Theorem 1 is now Theorem 1.1).

Beta is 4 C(1/2,1/2)-1, and xi conditions coordinate 1 on coordinate 0. Bounds are proved with regular conditional distributions, without a density assumption, so singular copulas are included. The left boundary is the signed tent family L_b of Section 3. The right boundary D_b of Proposition 4.2 is the copula of (U, T_b(U)) for the exact interval exchange T_b of the source; the alternative witnesses of the v1 supplement are kept as extra rows. The set S of median sections is encoded by a nonincreasing slope function p with integral 1/2; the convex function w of Lemma 5.2 is encoded by its nondecreasing slope d with |d| <= 1 (every use in the paper goes through d = 1-2p). Both parameter endpoints are included wherever the source allows them.

Result map

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

Source result	Lean declarations	Status	Hypotheses and scope
Section 2, (2.2): ξ formula via h=∂₁C	`Papers.OrendayLaresRockel2026XiBeta.xi_derivative_formula`; `Papers.OrendayLaresRockel2026XiBeta.one_sub_xi_eq`; `Papers.OrendayLaresRockel2026XiBeta.one_sub_xi_eq_deriv`	verified	All copulas; 1−ξ(C)=6∫∫h(1−h) with the derivative convention of the source.
Section 2, (2.3): ξ(Č)=ξ(C), β(Č)=−β(C)	`Papers.OrendayLaresRockel2026XiBeta.check_cdf`; `Papers.OrendayLaresRockel2026XiBeta.xi_check`; `Papers.OrendayLaresRockel2026XiBeta.beta_check`; `Papers.OrendayLaresRockel2026XiBeta.check_kernel`	verified	Č(u,v)=u−C(u,1−v), every copula.
Section 2, class convexity, SI⇒PQD, SD⇒NQD	`Papers.OrendayLaresRockel2026XiBeta.convex_univ`; `Papers.OrendayLaresRockel2026XiBeta.convex_pqd`; `Papers.OrendayLaresRockel2026XiBeta.convex_nqd`; `Papers.OrendayLaresRockel2026XiBeta.convex_si`; `Papers.OrendayLaresRockel2026XiBeta.convex_sd`; `Papers.OrendayLaresRockel2026XiBeta.convex_rs`; `Papers.OrendayLaresRockel2026XiBeta.convex_cls`; `Papers.OrendayLaresRockel2026XiBeta.convex_interSet`; `Papers.OrendayLaresRockel2026XiBeta.IsConvexClass.inter`; `Papers.OrendayLaresRockel2026XiBeta.isNQD_mix`; `Papers.OrendayLaresRockel2026XiBeta.isSD_mix`; `Papers.OrendayLaresRockel2026XiBeta.classSI_subset_classPQD`; `Papers.OrendayLaresRockel2026XiBeta.classSD_subset_classNQD`	verified	All five classes and their intersections are convex.
Section 2, kernel forms of SI/SD	`Papers.OrendayLaresRockel2026XiBeta.isSI_iff_antitone_version`; `Papers.OrendayLaresRockel2026XiBeta.isSD_iff_monotone_version`; `Papers.OrendayLaresRockel2026XiBeta.transpose_isSI_iff_concave`	verified	Per-v kernel versions; transpose SI iff u-concavity of C(u,·).
Section 2, (2.4): reflection of the regions	`Papers.OrendayLaresRockel2026XiBeta.isPQD_reflect_second_iff`; `Papers.OrendayLaresRockel2026XiBeta.isNQD_reflect_second_iff`; `Papers.OrendayLaresRockel2026XiBeta.isRadiallySymmetric_reflect_second_iff`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_pqd`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_nqd`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_si`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_sd`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_rs`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_univ`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_inter`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_cls`; `Papers.OrendayLaresRockel2026XiBeta.checkClass_interSet`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_checkClass`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_nqd_eq`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_sd_eq`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_rs_eq`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_interSet_check`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_sd_rs_eq`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_sd_eq_sd_rs`	verified	R^Ǎ = {(x,−y)} for the five classes and every intersection.
Lemma 2.1: interpolation	`Papers.OrendayLaresRockel2026XiBeta.interpolation_lemma`; `Papers.OrendayLaresRockel2026XiBeta.fixed_beta_intermediate_in_class`; `Papers.OrendayLaresRockel2026XiBeta.xi_mixture_continuous`; `Papers.OrendayLaresRockel2026XiBeta.beta_mixture_fixed`; `Papers.OrendayLaresRockel2026XiBeta.fixed_beta_intermediate`	verified	Convex subclass, equal β, target ξ between; continuity of ξ along mixtures.
Proposition 3.1: L_b is a copula with the stated density and kernel; β, ξ	`Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_paper`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_left_strip`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_right_strip`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_half`; `Papers.OrendayLaresRockel2026XiBeta.tent_distribution_functions`; `Papers.OrendayLaresRockel2026XiBeta.tentG_eq_zero`; `Papers.OrendayLaresRockel2026XiBeta.tentG_half`; `Papers.OrendayLaresRockel2026XiBeta.tentG_one_sub`; `Papers.OrendayLaresRockel2026XiBeta.tentG_neg`; `Papers.OrendayLaresRockel2026XiBeta.integral_tentG`; `Papers.OrendayLaresRockel2026XiBeta.integral_tentG_sq`; `Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_tentG`; `Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_ellFun`; `Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_tent_formula`; `Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_tent_formula_second`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_kernel_paper`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_deriv_paper`; `Papers.OrendayLaresRockel2026XiBeta.signedTentSlope_eq_tentGDeriv`; `Papers.OrendayLaresRockel2026XiBeta.tentDisplacement_eq_tentG`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_ae_eq_paper`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_density_paper`; `Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_values_ae`; `Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_left`; `Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_right`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_eq_integral_density`; `Papers.OrendayLaresRockel2026XiBeta.tent_kernel_sq_integral`; `Papers.OrendayLaresRockel2026XiBeta.xi_leftBoundary_from_kernel`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_beta`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_xi`; `Papers.OrendayLaresRockel2026XiBeta.left_boundary_attained`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_conditionalCDF`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_density`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_absolutelyContinuous`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_values`	verified	Every b∈[−1,1]; density c_b=1+σ(u)g_b′(v)∈{0,1,2} a.e.; kernel ∂₁L_b=v+σ(u)g_b(v); β(L_b)=b, ξ(L_b)=
Proposition 3.2(i): symmetries, exchangeability, special cases	`Papers.OrendayLaresRockel2026XiBeta.leftBoundary_check`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_survival`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_asymmetry`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_exchangeable_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_zero`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_zero_eq_independence`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_one_cdf`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_neg_one_cdf`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_one_eq_ordinalSum`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_neg_one_eq_check`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_quadrant_masses`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_reflect_first`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_reflect_second`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_radiallySymmetric`	verified	Ľ_b=L_{−b}, L̂_b=L_b, exchangeable iff b∈{−1,0,1}, L_0=Π, L_1 the ordinal sum of Π and Π at 1/2, L_{−1}=Ľ_1.
Proposition 3.2(ii)–(iii): monotonicity, quadrant dependence, reverse direction	`Papers.OrendayLaresRockel2026XiBeta.leftBoundary_si_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_sd_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_pqd_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_nqd_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_transpose_isSI_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_transpose_isSD_iff`	verified	SI/PQD iff b≥0, SD/NQD iff b≤0; transpose SI iff b∈{0,1}, SD iff b∈{0,−1}.
Proposition 3.2(iv): total positivity	`Papers.OrendayLaresRockel2026XiBeta.tentDensity_one`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_one_diagonal`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_one_antidiagonal`; `Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_nonneg`; `Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_ae_tp2_iff`; `Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_ae_rr2_iff`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_ae_tp2_iff`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_ae_rr2_iff`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_tp2_iff`; `Papers.OrendayLaresRockel2026XiBeta.tentDensity_rr2_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_density_version_ae_minors_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_hasMTP2Density_iff`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_hasRR2Density_iff`	verified	TP2 iff b∈{0,1}, RR2 iff b∈{0,−1}, for a.e. minors and for every nonnegative measurable density version.
Proposition 3.2(v): rank coefficients; Proposition 3.2 bundle	`Papers.OrendayLaresRockel2026XiBeta.leftBoundary_rho`; `Papers.OrendayLaresRockel2026XiBeta.leftBoundary_tau`; `Papers.OrendayLaresRockel2026XiBeta.proposition_3_2`	verified	ρ(L_b)=3b
Remark 3.3: tent is the unique minimizer	`Papers.OrendayLaresRockel2026XiBeta.abs_tentG_le_abs`; `Papers.OrendayLaresRockel2026XiBeta.tentG_sq_le`; `Papers.OrendayLaresRockel2026XiBeta.tent_minimizes`; `Papers.OrendayLaresRockel2026XiBeta.tent_minimizer_unique`	verified	Among 1-Lipschitz functions with value b/2 at 1/2, the tent minimizes ∫g² uniquely.
Proposition 4.1: sharp lower bound	`Papers.OrendayLaresRockel2026XiBeta.medianDisplacement_lipschitz`; `Papers.OrendayLaresRockel2026XiBeta.median_strip_energy`; `Papers.OrendayLaresRockel2026XiBeta.median_energy_le_xi`; `Papers.OrendayLaresRockel2026XiBeta.medianTent_le_abs_displacement`; `Papers.OrendayLaresRockel2026XiBeta.beta_cubic_le_two_xi`; `Papers.OrendayLaresRockel2026XiBeta.xi_eq_lower_iff`	verified
Proposition 4.2: explicit interval exchange D_b	`Papers.OrendayLaresRockel2026XiBeta.xchg_xchg`; `Papers.OrendayLaresRockel2026XiBeta.xchg_symm`; `Papers.OrendayLaresRockel2026XiBeta.coe_intervalExchange`; `Papers.OrendayLaresRockel2026XiBeta.intervalExchange_measurePreserving`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_ae_graph`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_completelyDependent`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_xi`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_cdf`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_cdf_low`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_cdf_mid`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_beta`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_exchangeable`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_radiallySymmetric`; `Papers.OrendayLaresRockel2026XiBeta.dExchange_pqd`; `Papers.OrendayLaresRockel2026XiBeta.proposition_4_2`	verified	The exact map T_b of the source, s_b=(1+b)/4, every b∈[−1,1]; measure preserving, ξ=1, β=b, exchangeable, radially symmetric, PQD for b≥0.
Proposition 4.2 (alternative witnesses, from v1)	`Papers.OrendayLaresRockel2026XiBeta.xi_twoBlockFlip`; `Papers.OrendayLaresRockel2026XiBeta.rightBoundary_beta`; `Papers.OrendayLaresRockel2026XiBeta.rightBoundary_xi`; `Papers.OrendayLaresRockel2026XiBeta.right_boundary_attained`; `Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_xi`; `Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_beta`; `Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_radiallySymmetric`; `Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_exchangeable`; `Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_pqd`; `Papers.OrendayLaresRockel2026XiBeta.symmetric_right_boundary_attained`	verified	Also proved with two other deterministic witnesses (kept from the v1 supplement).
Theorem 1.1: exact ξ–β region	`Papers.OrendayLaresRockel2026XiBeta.exact_xi_beta_region`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_1_region`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_1_inequality`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_1_right_boundary`	verified	R = {(x,y)∈[0,1]×[−1,1]:
Corollary 4.3: radially symmetric, PQD, NQD regions	`Papers.OrendayLaresRockel2026XiBeta.exactRegion_neg`; `Papers.OrendayLaresRockel2026XiBeta.region_of_witnesses`; `Papers.OrendayLaresRockel2026XiBeta.corollary_4_3_rs`; `Papers.OrendayLaresRockel2026XiBeta.corollary_4_3_pqd`; `Papers.OrendayLaresRockel2026XiBeta.corollary_4_3_nqd`; `Papers.OrendayLaresRockel2026XiBeta.exact_radiallySymmetric_xi_beta_region`; `Papers.OrendayLaresRockel2026XiBeta.exact_pqd_xi_beta_region`; `Papers.OrendayLaresRockel2026XiBeta.exact_pqd_radiallySymmetric_xi_beta_region`; `Papers.OrendayLaresRockel2026XiBeta.exact_nqd_xi_beta_region`	verified	R^RS=R; R^PQD=R^{PQD,RS}=R∩[0,1]²; R^NQD=R^{NQD,RS}=R∩([0,1]×[−1,0]).
Section 5, median sections and gap function	`Papers.OrendayLaresRockel2026XiBeta.exists_medianSection_of_isSI`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.concaveOn_A`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.convexOn_gap`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.abs_le_gap`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.gap_eq_integral`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.abs_gap_sub_le`	verified	The set S is encoded by a nonincreasing slope function; A concave, w convex, w≥
Lemma 5.1(i): Q_A is an SI copula with median section A, (5.1)	`Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion_of_le_half`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion_of_half_le`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.conditionalCDF_completion`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.kernelMeasure_real_Iic`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.completion_isSI`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_completion_half`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.completion_congr`	verified	Kernel mass p(u) at A(u) and 1−p(u) at B(u).
Lemma 5.1(ii)–(iii): maximal completion	`Papers.OrendayLaresRockel2026XiBeta.MedianSection.cdf_le_completion`; `Papers.OrendayLaresRockel2026XiBeta.xi_le_completion`; `Papers.OrendayLaresRockel2026XiBeta.eq_completion_of_xi_eq`; `Papers.OrendayLaresRockel2026XiBeta.integral_antitone_mul_nonneg`	verified	C≤Q_A for all copulas with C(·,1/2)=A; ξ(C)≤ξ(Q_A) for SI C, equality iff C=Q_A.
(5.2)–(5.3): 1−ξ(Q_A)=(3/2)J(w)	`Papers.OrendayLaresRockel2026XiBeta.MedianSection.xi_completion`; `Papers.OrendayLaresRockel2026XiBeta.MedianSection.one_sub_xi_completion`	verified	Also ξ(Q_A)=1−6∫p(1−p)w.
Lemma 5.2: sharp inequality for convex w	`Papers.OrendayLaresRockel2026XiBeta.SlopeData.w_sub_le`; `Papers.OrendayLaresRockel2026XiBeta.SlopeData.two_q_le_one`; `Papers.OrendayLaresRockel2026XiBeta.SlopeData.q_nonneg`; `Papers.OrendayLaresRockel2026XiBeta.SlopeData.two_q_sq_le_J`; `Papers.OrendayLaresRockel2026XiBeta.SlopeData.J_eq_two_q_sq_iff`	verified	Convex w encoded through its nondecreasing slope d with
(5.5): A_b and R_b	`Papers.OrendayLaresRockel2026XiBeta.rightSection_A`; `Papers.OrendayLaresRockel2026XiBeta.rightSection_gap`; `Papers.OrendayLaresRockel2026XiBeta.Rb_isSI`; `Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_half`; `Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_of_le_half`; `Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_of_half_le`; `Papers.OrendayLaresRockel2026XiBeta.Rb_zero_cdf_of_le_half`; `Papers.OrendayLaresRockel2026XiBeta.Rb_zero_cdf_of_half_le`	verified	b∈[0,1]; gap function w_b=max(
Proposition 5.3: law of (U,V_b)	`Papers.OrendayLaresRockel2026XiBeta.cdf_lawVb`; `Papers.OrendayLaresRockel2026XiBeta.measure_eq_of_real_Iic_eq`; `Papers.OrendayLaresRockel2026XiBeta.Rb_toMeasure_eq_lawVb`; `Papers.OrendayLaresRockel2026XiBeta.kerR_rightSection`; `Papers.OrendayLaresRockel2026XiBeta.marginals_Xb`; `Papers.OrendayLaresRockel2026XiBeta.Rb_eq_ofMap`; `Papers.OrendayLaresRockel2026XiBeta.Vb_uniform`; `Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_law`	verified	R_b is the copula of (U,V_b) with the source construction, b∈[0,1].
Proposition 5.3(i): singular, SI, radially symmetric, not exchangeable, transpose not SI, R_1=M	`Papers.OrendayLaresRockel2026XiBeta.Rb_singular`; `Papers.OrendayLaresRockel2026XiBeta.Rb_not_absolutelyContinuous`; `Papers.OrendayLaresRockel2026XiBeta.volume_supportGraphs`; `Papers.OrendayLaresRockel2026XiBeta.Rb_isRadiallySymmetric`; `Papers.OrendayLaresRockel2026XiBeta.Rb_not_exchangeable`; `Papers.OrendayLaresRockel2026XiBeta.Rb_transpose_not_isSI`; `Papers.OrendayLaresRockel2026XiBeta.Rb_one_eq_comonotonic`; `Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_i`	verified	Exchangeability and transpose claims for 0≤b<1.
Proposition 5.3(ii): ordinal-sum structure	`Papers.OrendayLaresRockel2026XiBeta.Rb_eq_finiteOrdinalSum`; `Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_ii`	verified	0<b<1: R_b is the ordinal sum of M, R_0, M over 0, b/2, 1−b/2, 1.
Proposition 5.3(iii)–(iv): β, ξ, τ, ρ of R_b	`Papers.OrendayLaresRockel2026XiBeta.Rb_beta`; `Papers.OrendayLaresRockel2026XiBeta.xi_Rb`; `Papers.OrendayLaresRockel2026XiBeta.integral_Rb`; `Papers.OrendayLaresRockel2026XiBeta.kendallTau_Rb`; `Papers.OrendayLaresRockel2026XiBeta.spearmanRho_Rb`; `Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_iii_iv`	verified	β=b, ξ=1−(3/4)(1−b)², τ=1−(1/2)(1−b)², ρ=1−(1/2)(1−b)³.
Theorem 1.2: inequality (1.5) and equality case	`Papers.OrendayLaresRockel2026XiBeta.si_beta_mem_Icc`; `Papers.OrendayLaresRockel2026XiBeta.xi_le_of_isSI`; `Papers.OrendayLaresRockel2026XiBeta.xi_eq_iff_of_isSI`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_inequality`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_inequality_alt`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_beta_lower`	verified	Every SI copula: ξ≤1−(3/4)(1−β)², equivalently β≥1−2√((1−ξ)/3); equality iff C=R_{β(C)}.
Theorem 1.2: exact SI region; SD by reflection	`Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_classSI_subset`; `Papers.OrendayLaresRockel2026XiBeta.siRegion_subset_xiBetaRegion_classSI_rs`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_region`; `Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_sd`; `Papers.OrendayLaresRockel2026XiBeta.siRegion_iff`	verified	R^SI=R^{SI,RS}={y³≤2x, 3(1−y)²≤4(1−x)}; R^SD=R^{SD,RS} its mirror image.
Remark 5.4(a): β=0 and R_0	`Papers.OrendayLaresRockel2026XiBeta.siRegion_fibre_beta_zero`; `Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_classSI_fibre_beta_zero`; `Papers.OrendayLaresRockel2026XiBeta.R0_upper_endpoint`; `Papers.OrendayLaresRockel2026XiBeta.V0_ae_eq`; `Papers.OrendayLaresRockel2026XiBeta.V0_floor_ae`; `Papers.OrendayLaresRockel2026XiBeta.R0_transpose_ae_graph`; `Papers.OrendayLaresRockel2026XiBeta.xi_R0_transpose`; `Papers.OrendayLaresRockel2026XiBeta.R0_SI_transpose_not_SI`	verified	SI fibre at β=0 is [0,1/4], ξ(R_0)=1/4, R_0^T completely dependent with ξ=1, R_0 SI but R_0^T not.
Remark 5.4(b): ξ≤τ≤ρ for R_b	`Papers.OrendayLaresRockel2026XiBeta.xi_le_tau_le_rho_Rb`	verified	b∈[0,1].
Introduction and Figure 1: claims about the regions	`Papers.OrendayLaresRockel2026XiBeta.leftBoundary_pm_one_xi`; `Papers.OrendayLaresRockel2026XiBeta.exists_mixture_leftBoundary_dExchange`; `Papers.OrendayLaresRockel2026XiBeta.horizontal_edges_attained`; `Papers.OrendayLaresRockel2026XiBeta.pqd_rho_eq_zero_iff`; `Papers.OrendayLaresRockel2026XiBeta.one_sub_sq_le_iff`; `Papers.OrendayLaresRockel2026XiBeta.xi_gt_quarter_beta_pos`; `Papers.OrendayLaresRockel2026XiBeta.abs_beta_le_rpow`; `Papers.OrendayLaresRockel2026XiBeta.figure1_dots`; `Papers.OrendayLaresRockel2026XiBeta.si_xi_gt_quarter_beta_pos`; `Papers.OrendayLaresRockel2026XiBeta.si_beta_zero_compatible`; `Papers.OrendayLaresRockel2026XiBeta.si_beta_zero_xi_le`; `Papers.OrendayLaresRockel2026XiBeta.figure1_si_boundary`; `Papers.OrendayLaresRockel2026XiBeta.figure1_si_dots`; `Papers.OrendayLaresRockel2026XiBeta.figure1_sd_boundary`	verified	L_{±1} attain ξ=1/2, mixtures fill the horizontal edges, ξ>1/4 forces β>0 for SI, β=0 compatible with every ξ∈[0,1/4], the dots Π, R_0, L_1, M and the boundary curves.
Remark 10 of v1 / Section 6: SI comparison family, inner intervals, rigidity at ξ=1	`Papers.OrendayLaresRockel2026XiBeta.stochasticUpper_isSI`; `Papers.OrendayLaresRockel2026XiBeta.stochasticUpper_beta`; `Papers.OrendayLaresRockel2026XiBeta.stochasticUpper_xi`; `Papers.OrendayLaresRockel2026XiBeta.si_inner_region_attained`; `Papers.OrendayLaresRockel2026XiBeta.sd_inner_region_attained`; `Papers.OrendayLaresRockel2026XiBeta.si_region_outer_bound`; `Papers.OrendayLaresRockel2026XiBeta.sd_region_outer_bound`; `Papers.OrendayLaresRockel2026XiBeta.si_xi_one_iff`; `Papers.OrendayLaresRockel2026XiBeta.sd_xi_one_iff`; `Papers.OrendayLaresRockel2026XiBeta.si_xi_one_beta`; `Papers.OrendayLaresRockel2026XiBeta.sd_xi_one_beta`	verified	Kept from the v1 supplement: bM+(1−b)Π; SI/SD and ξ=1 force M/W.

There are no pending rows within the declared scope. Not certified here: results the source cites from the literature (Sklar's theorem, existence of Markov kernels, Chatterjee's characterization that xi=1 forces V=f(U), the inequality xi <= tau for SI copulas of reference [27]); the intermediate steps of the proofs of Propositions 3.2(iii),(v) and 4.1 beyond the final statements listed above; the open problems of Section 6; and numerical plots and figures, which are not formal proofs.

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{OrendayLaresRockel2026XiBetaArxiv,
  author = {Orenday Lares, Jacob Israel and Rockel, Marcus},
  title = {The exact region between Chatterjee's $\xi$ and Blomqvist's $\beta$},
  year = {2026},
  eprint = {2606.30033},
  archivePrefix = {arXiv},
  primaryClass = {math.ST},
  note = {Version 1, 29 June 2026},
  url = {https://arxiv.org/abs/2606.30033v1}
}

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