← Mathematical handbook

Proposition 3.3: the six-strip upper seed

These are exactly the six positive-slope segments in the paper, including the degenerate endpoint shuffles. All coefficients use the resulting copula.

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeedStrip (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) (i : Fin 6) : Verification.ShuffleStrip

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeedShuffle (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : Verification.PositiveShuffle 6

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeedShuffle q hq = { strip := Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeedStrip q hq, total := ⋯, tile_x := ⋯, tile_y := ⋯ }

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeed (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : ProbabilityTheory.Copula 2

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeed q hq = (Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeedShuffle q hq).copula

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeed_footrule (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).spearmanFootrule = 12 * q ^ 2 - 1 / 2

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeed_beta (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).blomqvistBeta = 8 * q - 1

def Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeedPermutation : Equiv.Perm (Fin 6)

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeed_tau (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).kendallTau = 8 * q ^ 2

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.upperSeed_coefficients (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).kendallTau = 8 * q ^ 2 ∧ (upperSeed q hq).spearmanFootrule = 12 * q ^ 2 - 1 / 2 ∧ (upperSeed q hq).blomqvistBeta = 8 * q - 1