← Mathematical handbook

The exact endpoint and complete d-coverage of Example 3.10

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.elementaryDStar : ℝ

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.elementaryDStar = (12 - 2 * √3) / 33

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.elementaryGStar : ℝ

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.elementaryGStar = (173 - 16 * √3) / 363

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_endpoint_constants : (ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift 1 ⋯).z / 2 = elementaryDStar ∧ ProbabilityTheory.Copula.RankRegion.RhoGamma.contactGamma 1 = elementaryGStar

Equation (20): the elementary arc ends at the source's explicit radical constants.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.elementary_d_coverage {d : ℝ} (hd : 0 < d) (hdstar : d ≤ elementaryDStar) : ∃ (s : ℝ) (hs : 1 ≤ s), (ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.halfShift s hs).z / 2 = d

Every positive corner size through d-star occurs in the half-shift family.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.five_piece_shuffle_realizes_boundary {d : ℝ} (hd : 0 < d) (hdstar : d ≤ elementaryDStar) (hdi : d ∈ Set.Icc 0 (1 / 2)) : ∃ (C : ProbabilityTheory.Copula 2), C.toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ![u, fivePieceMap d hdi u]) MeasureTheory.volume ∧ C.giniGamma = -1 + 8 * d - 10 * d ^ 2 ∧ C.spearmanRho = -1 + 12 * d - 24 * d ^ 2 + 13 * d ^ 3

Example 3.10, all d in its stated range: graph law and both exact coefficients.