← Mathematical handbook

Example 1: the middle-quarter transposition is PLOD

noncomputable def Papers.AnsariRockel2026XiRho.plodShuffle : ProbabilityTheory.Copula 2

The four increasing strips have vertical order 0,2,1,3.

Equations

• Papers.AnsariRockel2026XiRho.plodShuffle = Verification.PermutationShuffle.copula 3 (Equiv.swap 1 2)

theorem Papers.AnsariRockel2026XiRho.plodShuffle_xi : plodShuffle.chatterjeeXi = 1

theorem Papers.AnsariRockel2026XiRho.plodShuffle_rho : plodShuffle.spearmanRho = 13 / 16

theorem Papers.AnsariRockel2026XiRho.plodShuffle_cdf (u v : ↑unitInterval) : plodShuffle.cdf ![u, v] = min (Verification.stripCut (1 / 4) 0 ↑u) (Verification.stripCut (1 / 4) 0 ↑v) + min (Verification.stripCut (1 / 4) (1 / 4) ↑u) (Verification.stripCut (1 / 4) (1 / 2) ↑v) + min (Verification.stripCut (1 / 4) (1 / 2) ↑u) (Verification.stripCut (1 / 4) (1 / 4) ↑v) + min (Verification.stripCut (1 / 4) (3 / 4) ↑u) (Verification.stripCut (1 / 4) (3 / 4) ↑v)

theorem Papers.AnsariRockel2026XiRho.plodShuffle_isPQD : plodShuffle.IsPQD

PLOD is proved at every point, including all strip edges.

theorem Papers.AnsariRockel2026XiRho.plod_counterexample : plodShuffle.IsPQD ∧ plodShuffle.chatterjeeXi = 1 ∧ plodShuffle.spearmanRho = 13 / 16 ∧ plodShuffle.spearmanRho < plodShuffle.chatterjeeXi

The source counterexample, with its exact values and strict failure of xi<=rho.