← Mathematical handbook

theorem Papers.Rockel2026XiFootrule.countableOrdinal_exchangeable (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hC : ∀ (k : ℕ), (C k).IsExchangeable) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsExchangeable

Countable ordinal sums inherit exchangeability from every block.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_diagonal_fixed (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (n : ℕ) : (ProbabilityTheory.Copula.countableOrdinalSum P C).diagonal (P.point n) = ↑(P.point n)

Every countable ordinal-sum partition endpoint is a diagonal fixed point.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_has_binary_split (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (n : ℕ) : ∃ (D : ProbabilityTheory.Copula 2) (E : ProbabilityTheory.Copula 2), D.ordinalSum E (P.point (n + 1)) = ProbabilityTheory.Copula.countableOrdinalSum P C

Every positive countable partition endpoint gives an actual binary split.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_first_lower_component (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).lowerOrdinalComponent (P.point 1) ⋯ ⋯ = C 0

The first rescaled component of an arbitrary adjacent countable sum is its first block.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_upper_component_tail (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).upperOrdinalComponent (P.point 1) ⋯ ⋯ = ProbabilityTheory.Copula.countableOrdinalSum (countableTailPartition P) fun (k : ℕ) => C (k + 1)

The remaining rescaled component is the shifted countable sum.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_recursive (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) : ProbabilityTheory.Copula.countableOrdinalSum P C = (C 0).ordinalSum (ProbabilityTheory.Copula.countableOrdinalSum (countableTailPartition P) fun (k : ℕ) => C (k + 1)) (P.point 1)

Canonical binary recursion for arbitrary adjacent countable ordinal sums.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_gap_recursive (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).chatterjeeXi - (ProbabilityTheory.Copula.countableOrdinalSum P C).spearmanFootrule = ↑(P.point 1) ^ 2 * ((C 0).chatterjeeXi - (C 0).spearmanFootrule) + (1 - ↑(P.point 1)) ^ 2 * ((ProbabilityTheory.Copula.countableOrdinalSum (countableTailPartition P) fun (k : ℕ) => C (k + 1)).chatterjeeXi - (ProbabilityTheory.Copula.countableOrdinalSum (countableTailPartition P) fun (k : ℕ) => C (k + 1)).spearmanFootrule)

The rank-coefficient gap contracts by the square of the tail width.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_xi_eq_footrule (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hC : ∀ (k : ℕ), (C k).chatterjeeXi = (C k).spearmanFootrule) : (ProbabilityTheory.Copula.countableOrdinalSum P C).chatterjeeXi = (ProbabilityTheory.Copula.countableOrdinalSum P C).spearmanFootrule

Any adjacent countable ordinal sum of rank-equality blocks again has ξ=ψ.

theorem Papers.Rockel2026XiFootrule.countablePiM_symmetric_rank_equality (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hC : ∀ (k : ℕ), C k = ProbabilityTheory.Copula.independence 2 ∨ C k = ProbabilityTheory.Copula.comonotonic 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsExchangeable ∧ (ProbabilityTheory.Copula.countableOrdinalSum P C).chatterjeeXi = (ProbabilityTheory.Copula.countableOrdinalSum P C).spearmanFootrule

Any adjacent countable sequence of Π and M blocks is symmetric with ξ=ψ.