← Mathematical handbook

The full constructive lower curve in equation (44)

noncomputable def Papers.AnsariRockel2026RhoFootrule.lowerInnerRatio (x : ℝ) : ℝ

The source lower inner curve, written with sqrt-cubed instead of a real exponent.

Equations

• Papers.AnsariRockel2026RhoFootrule.lowerInnerRatio x = if x ≤ 1 / 4 then 0 else √((4 * x - 1) / 3) ^ 3

theorem Papers.AnsariRockel2026RhoFootrule.lowerInnerRatio_formula (x : ℝ) (hx : 1 / 4 ≤ x) : lowerInnerRatio x = ((4 * x - 1) / 3) ^ (3 / 2)

The square-root convention agrees with the displayed exponent 3/2.

theorem Papers.AnsariRockel2026RhoFootrule.partialReveal_conditional_distribution (t v : ↑unitInterval) : (fun (u : ↑unitInterval) => (Verification.partialReveal t).conditionalCDF u v) =ᵐ[MeasureTheory.volume] Verification.partialRevealKernel t v

The constructed family reveals the central interval and pairs the remaining ranks.

theorem Papers.AnsariRockel2026RhoFootrule.partialReveal_coefficients (t : ↑unitInterval) : (Verification.partialReveal t).chatterjeeXi = (1 + 3 * ↑t ^ 2) / 4 ∧ copulaCorrelationRatio (Verification.partialReveal t) = ↑t ^ 3

The exact parameterized coefficient path includes t=0 and t=1.

theorem Papers.AnsariRockel2026RhoFootrule.curved_lower_inner_attained (x : ℝ) (hx : x ∈ Set.Icc (1 / 4) 1) : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ copulaCorrelationRatio C = ((4 * x - 1) / 3) ^ (3 / 2)

Every point of the curved lower inner boundary is attained by an actual copula.

theorem Papers.AnsariRockel2026RhoFootrule.lower_inner_attained (x : ℝ) (hx : x ∈ Set.Icc 0 1) : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ copulaCorrelationRatio C = lowerInnerRatio x

Equation (44): the complete lower inner curve, including the horizontal segment.