Semiorder–Ranking Bridge @cite{luce-1959}

Connects the two halves of @cite{luce-1959} that are formalized independently in ChoiceApproximations.lean (§1.G) and RankOrderings.lean (§2.F):

• §1.G defines pairwise choice probabilities P(x,y) = v(x)/(v(x)+v(y)), JND thresholds, the semiorder (L(π), I(π)), and the trace ordering.
• §2.F defines ranking probabilities as products of successive pChoice values from shrinking alternative sets.

The bridge connects them via five results:

1. fromScale: Construct a RationalAction from a raw scale v : A → ℝ.
2. pairwiseProb_eq_pChoice: Binary choice probability equals pChoice restricted to the pair {x, y}.
3. rankProbRec_swap_ratio: Swapping two adjacent elements in a ranking changes the probability by the ratio (v(x) + S_rest) / (v(y) + S_rest).
4. JND effects on rankings: Indistinguishable items have bounded swap ratio; discriminable items have ordered ranking probability.
5. Trace–expected rank: The trace ordering matches expected rank ordering.

noncomputable def Core.RationalAction.fromScale {A : Type u_1} [Fintype A] (v : A → ℝ) (hv : ∀ (a : A), 0 ≤ v a) : RationalAction Unit A

Construct a RationalAction from a raw positive scale v : A → ℝ, the type used throughout ChoiceApproximations (§1.G).

This lets us apply the RankOrderings (§2.F) machinery — rankProbRec, expectedRank — to the same scales that define pairwiseProb, jndL, jndI, and the trace.

Equations

• Core.RationalAction.fromScale v hv = { score := fun (x : Unit) (a : A) => v a, score_nonneg := ⋯ }

theorem Core.pairwiseProb_eq_pChoice {A : Type u_1} [Fintype A] [DecidableEq A] (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (x y : A) (hne : x ≠ y) : pairwiseProb v x y = (RationalAction.fromScale v ⋯).pChoice () {x, y} x

The fundamental connection between §1.G and §2.F: binary choice probability P(x, y) = v(x)/(v(x)+v(y)) from ChoiceApproximations equals pChoice from RationalAction on the two-element set {x, y}.

Proof: unfold both sides. pairwiseProb v x y = v x / (v x + v y). pChoice {x,y} x = v x / (∑ b ∈ {x,y}, v b) = v x / (v x + v y) when x ≠ y (so {x,y} has two elements).

theorem Core.rankProbRec_swap_ratio {A : Type u_1} [Fintype A] [DecidableEq A] (ra : RationalAction Unit A) (s : Unit) (x y : A) (rest : List A) (_hne : x ≠ y) (hx : x ∉ rest) (hy : y ∉ rest) (_hnd : rest.Nodup) (hpos : ∀ (b : A), 0 < ra.score s b) : rankProbRec ra s (x :: y :: rest) / rankProbRec ra s (y :: x :: rest) = (ra.score s x + ∑ b ∈ rest.toFinset, ra.score s b) / (ra.score s y + ∑ b ∈ rest.toFinset, ra.score s b)

Swapping two adjacent elements in a ranking changes the probability by the ratio (v(x) + S_rest) / (v(y) + S_rest) where S_rest = ∑ b ∈ rest, v b.

This corrects the naive intuition that the ratio should be v(x)/v(y). The difference arises because the second step of each ranking draws from a different set: {y} ∪ rest vs {x} ∪ rest. Expanding:

rankProbRec(x::y::rest) / rankProbRec(y::x::rest) = [pChoice(T, x) · pChoice({y}∪R, y)] / [pChoice(T, y) · pChoice({x}∪R, x)] = [v(x)/S_T · v(y)/(v(y)+S_R)] / [v(y)/S_T · v(x)/(v(x)+S_R)] = (v(x)+S_R) / (v(y)+S_R)

where T = {x,y} ∪ R and S_R = ∑ b ∈ R, v b.

theorem Core.jndL_swap_ordered {A : Type u_1} [Fintype A] [DecidableEq A] (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (x y : A) (rest : List A) (hL : jndL v thr x y) (hx : x ∉ rest) (hy : y ∉ rest) (hnd : rest.Nodup) : rankProbRec (RationalAction.fromScale v ⋯) () (y :: x :: rest) < rankProbRec (RationalAction.fromScale v ⋯) () (x :: y :: rest)

If x is discriminably preferred to y at threshold π (i.e., xL(π)y), then the ranking with x before y is strictly more probable than the ranking with y before x.

From jndL, P(x,y) > π > 1/2, so v(x) > v(y), hence v(x) + S_R > v(y) + S_R, making the ranking x::y::rest more probable.

This is the ranking-probability counterpart of Theorem 5's L-transitivity: discriminable preference in pairwise choice implies discriminable preference in ranking probability.

theorem Core.jndI_swap_bounded {A : Type u_1} [Fintype A] [DecidableEq A] (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (thr : ℝ) (hthr_lower : 1 / 2 < thr) (hthr_upper : thr < 1) (x y : A) (rest : List A) (hI : jndI v thr x y) (hx : x ∉ rest) (hy : y ∉ rest) (hnd : rest.Nodup) : rankProbRec (RationalAction.fromScale v ⋯) () (x :: y :: rest) / rankProbRec (RationalAction.fromScale v ⋯) () (y :: x :: rest) ≤ thr / (1 - thr)

If x and y are indistinguishable at threshold π (i.e., xI(π)y), then swapping them in a ranking changes the probability by at most a factor of thr / (1 - thr).

From jndI, P(x,y) ≤ thr, so v(x)/(v(x)+v(y)) ≤ thr, giving v(x)/v(y) ≤ thr/(1-thr). Since (v(x)+S_R)/(v(y)+S_R) ≤ v(x)/v(y) when v(x) ≥ v(y) (adding a constant to both sides shrinks the ratio), the swap ratio is bounded by thr/(1-thr).

When v(x) ≤ v(y), the ratio is ≤ 1 < thr/(1-thr) (since thr > 1/2).

theorem Core.traceGe_iff_expectedRank_le {A : Type u_1} [Fintype A] [DecidableEq A] (v : A → ℝ) (hv : ∀ (a : A), 0 < v a) (T : Finset A) (x y : A) (hx : x ∈ T) (hy : y ∈ T) (hne : x ≠ y) : traceGe v x y ↔ expectedRank (RationalAction.fromScale v ⋯) () T x ≤ expectedRank (RationalAction.fromScale v ⋯) () T y

The trace ordering from §1.G (Definition 4) matches the expected rank ordering from §2.F: x ≥_T y iff E[rank(x)] ≤ E[rank(y)].

By trace_iff_scale_ge, x ≥_T y ↔ v(x) ≥ v(y). By expectedRank_lt_of_score_gt, v(x) > v(y) implies E[rank(x)] < E[rank(y)]. So the two orderings agree on strict preference.

The ≤ case (when v(x) = v(y)) follows from expectedRank_eq_of_score_eq.