Psychophysics: Stevens' Power Law and Multidimensional Stimuli @cite{luce-1959}

@cite{luce-1959} §2.B–C: the power-law specialization of the Fechnerian framework and its extension to multi-dimensional stimulus continua.

§2.B: Stevens' Power Law (pp. 44–49)

Stevens' magnitude estimation experiments yield ψ(s) = k · sⁿ — a power function relating physical stimulus intensity to psychological magnitude. Luce shows this is not an independent discovery but a corollary of the Fechnerian framework (luce_fechnerian_exp in RationalAction.lean) under a change of variables.

The key insight: if we work with log-intensity u = log s rather than raw intensity s, then the ratio scale v(s) = C · sⁿ = C · exp(n · log s) is exactly the exponential form forced by the Cauchy equation. In other words, Stevens' power law IS Fechner's log law, viewed in different coordinates:

• Fechner (interval scale on log-intensity): v = C · exp(n · u)
• Stevens (ratio scale on raw intensity): v = C · sⁿ

The pairwise choice probability under Stevens' power law is:

P(s₁, s₂) = s₁ⁿ / (s₁ⁿ + s₂ⁿ)

which is the Luce choice rule with score(s) = sⁿ.

§2.C: Interaction of Stimulus Continua (pp. 49–53)

When stimuli vary along multiple dimensions simultaneously (e.g., both loudness and brightness), Luce shows the choice rule decomposes multiplicatively:

v(a₁, a₂) = v₁(a₁) · v₂(a₂)

provided the dimensions contribute independently to discriminability. This DimensionIndependence axiom says that the relative discriminability along one dimension does not depend on the value along the other.

structure Core.StevensScale : Type

A Stevens power-law scale: ψ(s) = k · sⁿ.

The exponent n characterizes the sensory modality (e.g., n ≈ 0.67 for brightness, n ≈ 3.5 for electric shock). The coefficient k is a unit constant that depends on the choice of measurement units.

This is the ratio-scale representation of psychophysical magnitude. Under change of variables u = log s, it becomes the exponential form v = k · exp(n · u) — exactly the Fechnerian characterization.

• n : ℝ

  Power-law exponent (sensory modality parameter).

• k : ℝ

  Scale coefficient (unit-dependent constant).

• hn_pos : 0 < self.n

  Exponent is positive (higher intensity → higher magnitude).

• hk_pos : 0 < self.k

  Coefficient is positive (magnitudes are positive).

noncomputable def Core.StevensScale.psi (σ : StevensScale) (s : ℝ) : ℝ

The Stevens power function: ψ(s) = k · sⁿ. Requires s > 0 (stimulus intensities are positive reals).

Equations

• σ.psi s = σ.k * s ^ σ.n

theorem Core.StevensScale.psi_pos (σ : StevensScale) {s : ℝ} (hs : 0 < s) : 0 < σ.psi s

Stevens scale values are positive for positive stimuli.

noncomputable def Core.StevensScale.choiceProb (σ : StevensScale) (s₁ s₂ : ℝ) : ℝ

Pairwise choice probability under Stevens' power law: P(s₁, s₂) = s₁ⁿ / (s₁ⁿ + s₂ⁿ).

This is the Luce choice rule with score function score(s) = sⁿ. The coefficient k cancels in the ratio.

Equations

• σ.choiceProb s₁ s₂ = s₁ ^ σ.n / (s₁ ^ σ.n + s₂ ^ σ.n)

theorem Core.StevensScale.choiceProb_complement (σ : StevensScale) {s₁ s₂ : ℝ} (h₁ : 0 < s₁) (h₂ : 0 < s₂) : σ.choiceProb s₁ s₂ + σ.choiceProb s₂ s₁ = 1

Choice probabilities sum to 1 for positive stimuli.

theorem Core.StevensScale.choiceProb_nonneg (σ : StevensScale) {s₁ s₂ : ℝ} (h₁ : 0 < s₁) (h₂ : 0 < s₂) : 0 ≤ σ.choiceProb s₁ s₂

Choice probability is between 0 and 1 for positive stimuli.

theorem Core.StevensScale.choiceProb_eq (σ : StevensScale) {s : ℝ} (hs : 0 < s) : σ.choiceProb s s = 1 / 2

Equal stimuli give probability 1/2 (indifference).

theorem Core.StevensScale.choiceProb_mono (σ : StevensScale) {s₁ s₂ s₃ : ℝ} (h₁ : 0 < s₁) (h₂ : 0 < s₂) (h₃ : 0 < s₃) (hle : s₁ ≤ s₂) : σ.choiceProb s₁ s₃ ≤ σ.choiceProb s₂ s₃

Monotonicity: higher stimulus → higher choice probability. Follows from rpow_le_rpow and monotonicity of x / (x + c).

noncomputable def Core.stevens_is_luce {Stimulus : Type u_1} [Fintype Stimulus] (σ : StevensScale) (intensity : Stimulus → ℝ) (h_pos : ∀ (s : Stimulus), 0 < intensity s) : RationalAction Unit Stimulus

Stevens' power law choice probabilities satisfy the Luce model.

Given a finite set of stimuli with positive intensities, the choice rule score(s) = sⁿ defines a valid RationalAction. The coefficient k drops out of the normalized policy.

Equations

• Core.stevens_is_luce σ intensity h_pos = { score := fun (x : Unit) (s : Stimulus) => intensity s ^ σ.n, score_nonneg := ⋯ }

theorem Core.stevens_luce_pairwise {σ : StevensScale} {s₁ s₂ : ℝ} (h₁ : 0 < s₁) (h₂ : 0 < s₂) : have ra := stevens_is_luce σ ![s₁, s₂] ⋯; ra.policy () 0 = σ.choiceProb s₁ s₂

The Luce model from Stevens' power law recovers the pairwise choice probability as a special case (for a two-element choice set).

theorem Core.stevens_fechner_equivalence (σ : StevensScale) {s : ℝ} (hs : 0 < s) : σ.psi s = σ.k * Real.exp (σ.n * Real.log s)

Stevens–Fechner equivalence (@cite{luce-1959}, §2.B): Stevens' power law on raw intensity is equivalent to Fechner's exponential law on log-intensity.

If v(s) = k · sⁿ (Stevens), define u(s) = log s. Then: v(s) = k · exp(n · u(s)) which is exactly the Fechnerian form from luce_fechnerian_exp.

This shows the two "laws" are the same mathematical structure viewed in different coordinates: Stevens works on the multiplicative scale of physical intensity, Fechner on the additive scale of log-intensity.

theorem Core.StevensScale.ratio_depends_on_ratio (σ : StevensScale) {s₁ s₂ : ℝ} (h₁ : 0 < s₁) (h₂ : 0 < s₂) : σ.psi s₁ / σ.psi s₂ = (s₁ / s₂) ^ σ.n

The ratio of Stevens scale values depends only on the intensity ratio, confirming it is a ratio scale.

theorem Core.stevens_cauchy (σ : StevensScale) (u₁ u₂ : ℝ) : Real.exp (σ.n * (u₁ + u₂)) = Real.exp (σ.n * u₁) * Real.exp (σ.n * u₂)

Stevens' power law satisfies the Cauchy multiplicative equation on log-intensity: g(u₁ + u₂) = g(u₁) · g(u₂) where g(u) = exp(n · u).

This is the bridge to cauchy_mul_exp: the function mapping log-intensity differences to scale ratios is the exponential.

structure Core.MultidimStimulus (D : Type u_1) (S : D → Type u_2) : Type (max u_1 u_2)

A multi-dimensional stimulus has components along each dimension. Each dimension has its own psychophysical scale function.

Example: a stimulus varying in both loudness (dim 1) and brightness (dim 2) is represented as a pair (a₁, a₂) with independent scale functions v₁ and v₂.

• scale (d : D) : S d → ℝ

  Scale function for each dimension.

• scale_pos (d : D) (s : S d) : 0 < self.scale d s

  Scale values are positive.

structure Core.DimensionIndependence {D : Type u_1} [Fintype D] [DecidableEq D] {S : D → Type u_2} (v : ((d : D) → S d) → ℝ) (ms : MultidimStimulus D S) : Prop

Independence axiom for multi-dimensional stimuli (@cite{luce-1959}, §2.C): the relative discriminability along one dimension does not depend on the value along the other dimensions.

Formally: for a two-dimensional stimulus, the ratio v(a₁, a₂) / v(b₁, a₂) depends only on a₁ and b₁, not on a₂. This forces the overall scale to decompose as a product: v(a₁, a₂) = v₁(a₁) · v₂(a₂).

We state this for an arbitrary (finite) number of dimensions.

• v_pos (a : (d : D) → S d) : 0 < v a

  Overall scale is positive.

• ratio_indep (d : D) (a : (d : D) → S d) (s : S d) : v (Function.update a d s) / v a = ms.scale d s / ms.scale d (a d)

  Independence: replacing the value along dimension d scales v by a factor depending only on d and the old/new values, not on the values along other dimensions.

  For all stimuli a, if we change dimension d from a d to s, the ratio v(a[d↦s]) / v(a) depends only on a d and s.

theorem Core.multidimensional_decomposition {D : Type u_1} [Fintype D] [DecidableEq D] {S : D → Type u_2} (v : ((d : D) → S d) → ℝ) (ms : MultidimStimulus D S) (ind : DimensionIndependence v ms) (a₀ : (d : D) → S d) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : (d : D) → S d), v a = C * ∏ d : D, ms.scale d (a d)

Multidimensional decomposition (@cite{luce-1959}, §2.C, Theorem): Under dimension independence, the overall scale function factors as a product of per-dimension scales (up to a global constant).

v(a) = C · ∏ d, scale d (a d)

where C absorbs the normalization.

theorem Core.multidim_two_decomposition {S₁ : Type u_1} {S₂ : Type u_2} [Nonempty S₁] [Nonempty S₂] (v : S₁ × S₂ → ℝ) (v₁ : S₁ → ℝ) (v₂ : S₂ → ℝ) (hv_pos : ∀ (a : S₁ × S₂), 0 < v a) (hv₁_pos : ∀ (s : S₁), 0 < v₁ s) (hv₂_pos : ∀ (s : S₂), 0 < v₂ s) (h_indep₁ : ∀ (s₁ s₁' : S₁) (s₂ : S₂), v (s₁, s₂) / v (s₁', s₂) = v₁ s₁ / v₁ s₁') (h_indep₂ : ∀ (s₁ : S₁) (s₂ s₂' : S₂), v (s₁, s₂) / v (s₁, s₂') = v₂ s₂ / v₂ s₂') : ∃ (C : ℝ), 0 < C ∧ ∀ (a₁ : S₁) (a₂ : S₂), v (a₁, a₂) = C * v₁ a₁ * v₂ a₂

For two dimensions, decomposition gives the explicit product form: v(a₁, a₂) = C · v₁(a₁) · v₂(a₂).

The original h_factor hypothesis (per-pair C) was too weak — different pairs could have different constants. The correct hypothesis is ratio-independence: the ratio v(s₁, s₂)/v(s₁', s₂) depends only on s₁, s₁' (not on s₂), and symmetrically for dimension 2. This is the two-dimensional specialization of DimensionIndependence.ratio_indep.

noncomputable def Core.multidim_luce {D : Type u_1} [Fintype D] [DecidableEq D] {S : D → Type u_2} {Alt : Type u_3} [Fintype Alt] (ms : MultidimStimulus D S) (stimulus : Alt → (d : D) → S d) : RationalAction Unit Alt

The Luce choice rule for multi-dimensional stimuli with independent dimensions decomposes into a product of per-dimension contributions.

For a choice between multi-dimensional alternatives, the choice probability factors: P(a, T) ∝ ∏ d, scale d (a d)

Equations

• Core.multidim_luce ms stimulus = { score := fun (x : Unit) (a : Alt) => ∏ d : D, ms.scale d (stimulus a d), score_nonneg := ⋯ }

theorem Core.multidim_marginal_recovery {S₁ : Type u_1} {S₂ : Type u_2} (v₁ : S₁ → ℝ) (v₂ : S₂ → ℝ) {a b : S₁} {c : S₂} (_ha : 0 < v₁ a) (_hb : 0 < v₁ b) (hc : 0 < v₂ c) : v₁ a * v₂ c / (v₁ a * v₂ c + v₁ b * v₂ c) = v₁ a / (v₁ a + v₁ b)

Independence implies that the multi-dimensional Luce model recovers the single-dimension choice probability when all other dimensions are held constant.

structure Core.PosReal : Type

Positive reals: the natural domain for stimulus intensities. Wraps a real number with a proof of positivity.

• val : ℝ
• pos : 0 < self.val

noncomputable def Core.multidimStevens {D : Type u_1} [Fintype D] (exponents : D → StevensScale) : MultidimStimulus D fun (x : D) => PosReal

A multi-dimensional Stevens scale: each dimension has its own power-law exponent. The overall scale is the product of per-dimension power functions.

Example: for loudness (n₁ ≈ 0.67) × brightness (n₂ ≈ 0.33), v(s₁, s₂) = C · s₁^0.67 · s₂^0.33.

The domain is PosReal (positive reals) because stimulus intensities are inherently positive, and rpow requires a positive base.

Equations

• Core.multidimStevens exponents = { scale := fun (x : D) (s : Core.PosReal) => s.val ^ (exponents x).n, scale_pos := ⋯ }

theorem Core.multidimStevens_fechner_per_dim {D : Type u_1} [Fintype D] (exponents : D → StevensScale) (d : D) {s : ℝ} (hs : 0 < s) : s ^ (exponents d).n = Real.exp ((exponents d).n * Real.log s)

Each dimension of a multi-dimensional Stevens model satisfies the Fechner equivalence independently.