Gaussian Choice Bridge @cite{luce-1959}

Connects the two Gaussian choice models formalized independently in SignalDetection.lean (§2.E) and Thurstone.lean (§2.D):

• Thurstone Case V (§2.D): Paired comparison — each stimulus evokes a Gaussian discriminal process; choice probability is Φ((u(a)-u(b))/(σ√2)).
• SDT (§2.E): Detection — a single observation is compared to a criterion; hit rate is 1 - Φ(c - d'/2) = Φ(d'/2 - c).

Luce (§2.E, p. 60) notes that SDT is "essentially Thurstone's discriminal process theory applied to the two-alternative detection context." This file makes that connection precise via four results:

1. SDT as Thurstone (2AFC): The two-alternative forced choice (2AFC) correct-response probability Φ(d'/√2) equals Thurstone's choiceProb for signal vs noise with unit per-stimulus variance.
2. Yes/No SDT as Thurstone: The yes/no hit rate Φ(d'/2 - c) equals Thurstone's choiceProb with σ = 1/√2.
3. Logistic constant unification: SDT's logisticApproxConst = π/√3 equals Thurstone's thurstoneLuceK(1/√2).
4. Shared softmax embedding: Both approximate the same RationalAction under the logistic-normal approximation.

noncomputable def Core.SDTModel.twoAFC (m : SDTModel) : ℝ

Two-alternative forced choice (2AFC) correct-response probability.

In 2AFC, the observer sees two intervals — one containing signal+noise (from N(d'/2, 1)) and one containing noise only (from N(-d'/2, 1)) — and identifies which had the signal. The correct response probability is:

P(correct) = P(X_signal > X_noise) = Φ(d' / √2)

since X_signal - X_noise N(d', 2), so (X_signal - X_noise)/√2 N(d'/√2, 1).

Equations

• m.twoAFC = Core.normalCDF (m.d_prime / √2)

theorem Core.SDTModel.twoAFC_ge_half (m : SDTModel) : 1 / 2 ≤ m.twoAFC

2AFC probability is at least 1/2 when d' ≥ 0: the observer performs at or above chance.

noncomputable def Core.SDTModel.asThurstone2AFC (m : SDTModel) : ThurstoneCaseV (Fin 2)

Construct a Thurstone Case V model for the 2AFC detection task.

Signal and noise are treated as two stimuli with scale values d'/2 and -d'/2, both with unit discriminal dispersion (σ = 1). Fin 2: 0 = signal, 1 = noise.

Equations

• m.asThurstone2AFC = { scale := fun (i : Fin 2) => if i = 0 then m.d_prime / 2 else -(m.d_prime / 2), sigma := 1, sigma_pos := Core.SDTModel.asThurstone2AFC._proof_2 }

theorem Core.SDTModel.twoAFC_eq_thurstone (m : SDTModel) : m.twoAFC = m.asThurstone2AFC.choiceProb 0 1

SDT 2AFC = Thurstone Case V: the 2AFC correct-response probability equals the Thurstone choice probability for signal vs noise.

Both reduce to Φ(d' / √2):

• 2AFC: Φ(d' / √2) (by definition)
• Thurstone: Φ((d'/2 - (-d'/2)) / (1 · √2)) = Φ(d' / √2)

noncomputable def Core.SDTModel.asThurstonYesNo (m : SDTModel) : ThurstoneCaseV (Fin 2)

Construct a Thurstone Case V model for the yes/no SDT task.

The yes/no task (observe, then decide signal vs noise) is equivalent to a Thurstone model with σ = 1/√2 (so that σ√2 = 1), where:

• scale(signal) = d'/2 - c (effective signal advantage)
• scale(noise) = 0 Fin 2: 0 = signal, 1 = noise.

Equations

• m.asThurstonYesNo = { scale := fun (i : Fin 2) => if i = 0 then m.d_prime / 2 - m.criterion else 0, sigma := 1 / √2, sigma_pos := Core.SDTModel.asThurstonYesNo._proof_1 }

theorem Core.SDTModel.hitRate_eq_thurstone (m : SDTModel) : m.hitRate = m.asThurstonYesNo.choiceProb 0 1

Yes/No SDT = Thurstone: the hit rate equals the Thurstone choice probability for the yes/no model.

SDT hit rate: 1 - Φ(c - d'/2) = Φ(d'/2 - c) (by CDF symmetry). Thurstone with σ = 1/√2: Φ((d'/2 - c) / ((1/√2) · √2)) = Φ(d'/2 - c).

The key identity is (1/√2) · √2 = 1, so the Thurstone denominator is 1 and the two expressions coincide.

theorem Core.logisticApproxConst_eq_thurstoneLuceK : logisticApproxConst = thurstoneLuceK (1 / √2)

The SDT logistic approximation constant π/√3 equals Thurstone's thurstoneLuceK when σ = 1/√2.

This is because: thurstoneLuceK(1/√2) = π / ((1/√2) · √6) = π · √2 / √6 = π / √3

The identity √2 / √6 = 1/√3 follows from √2 · √3 = √6.

Significance: the logistic approximation that connects SDT to the Luce model (§2.E) is exactly the same as the approximation that connects Thurstone to the Luce model (§2.D), when we use the yes/no SDT parameterization (σ = 1/√2).

theorem Core.SDTModel.twoAFC_mono (m₁ m₂ : SDTModel) (h : m₁.d_prime < m₂.d_prime) : m₁.twoAFC < m₂.twoAFC

2AFC models with different d' can be compared via the Thurstone ordering.

Since twoAFC = Thurstone.choiceProb, and Thurstone satisfies strong stochastic transitivity, higher d' implies higher 2AFC P(correct).

Proof: d₁' > d₂' implies scale(signal) - scale(noise) = d' is larger, so the Thurstone argument d'/√2 is larger, and Φ is strictly monotone.

RUM Unification

Both Thurstone and Luce choice models are Random Utility Models (RUMs) — they differ only in the noise distribution:

Model	Noise Distribution	Choice Probability	Reference
Thurstone V	Gaussian(0, σ²)	Φ((u_a-u_b)/(σ√2))	Thurstone.lean
Gumbel-Luce	Gumbel(0, β)	logistic((u_a-u_b)/β)	GumbelLuce.lean

The Gumbel-Luce model gives exactly the softmax (Luce) choice rule (McFadden's theorem, mcfaddenIntegral_eq_softmax). The Thurstone model gives the normal CDF. These agree up to the Gaussian-logistic approximation Φ(y·√3/π) ≈ logistic(y) (max error ~0.023, variance matching; see thurstone_luce_identity).

The constant k = π/(σ√6) that appears in the Thurstone-Luce approximation (thurstoneLuceK) is the scale matching between Gaussian and Gumbel noise: it equates the variances σ² · 2 (Gaussian difference) and β² · π²/3 (logistic/Gumbel difference).

theorem Core.gumbelRUM_binary_eq_logistic (d' β : ℝ) (hβ : 0 < β) : mcfaddenIntegral (fun (i : Fin 2) => if i = 0 then d' / 2 else -(d' / 2)) β 0 = logistic (d' / β)

Gumbel-Luce binary = logistic (exact): A Gumbel RUM with utilities [d'/2, -d'/2] and scale β gives choice probability logistic(d'/β).

Compare with Thurstone Case V (hitRate_eq_thurstone), which gives Φ(d'/(σ√2)) — the same functional form but with the normal CDF instead of logistic.

The two models are both RUMs; they agree when Φ ≈ logistic, i.e., when the variance-matched scale β = σ√6/π (see thurstoneLuceK).