Generalised Surprisal Configuration

@cite{giulianelli-etal-2026}

Enum-level configuration for the generalised surprisal family. The real-valued semantics of these enum tags lives in IAS.lean; this file just enumerates the parameter axes.

A generalised surprisal model has four parameters:

1. A warping function f mapping expected scores to processing measures
2. A scoring function g measuring how well alternatives match the target
3. A forecast horizon h: how many future symbols are considered
4. A representational level: the abstraction at which alternatives are compared

Standard surprisal is the special case (negLog, indicator, 1, predictive). Incremental information value is the family (identity, distance, h, l).

Scope note

Per linglib's processing-library scope (CLAUDE.md): this file formalizes the parameter space of a processing-theory family. It does not formalize psycholinguistic measurement instruments (N400, P600, RT, cloze, etc.) or empirical-fit tables — those are out of scope. Per-paper empirical findings about which (h, l) configuration best predicts which measure live in study-file docstring prose with citations, not as Lean theorems.

Main definitions

• SurprisalConfig: Complete generalised surprisal parameter tuple
• standardSurprisal: The configuration corresponding to @cite{levy-2008}
• informationValue: The IAS configuration at a given (horizon, level)
• ias_recovers_surprisal: Standard surprisal is a special case of IAS

inductive Theories.Processing.PredictiveUncertainty.WarpingFn : Type

Warping functions mapping expected scores to processing measures. γ(w;c) = f(E[g(a,w,c)]).

• negLog : WarpingFn

  f(x) = −log(x): standard surprisal (bits)

• identity : WarpingFn

  f(x) = x: information value (raw expected distance)

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instDecidableEqWarpingFn : DecidableEq WarpingFn

Equations

• Theories.Processing.PredictiveUncertainty.instDecidableEqWarpingFn x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Processing.PredictiveUncertainty.instReprWarpingFn.repr : WarpingFn → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instReprWarpingFn : Repr WarpingFn

Equations

• Theories.Processing.PredictiveUncertainty.instReprWarpingFn = { reprPrec := Theories.Processing.PredictiveUncertainty.instReprWarpingFn.repr }

inductive Theories.Processing.PredictiveUncertainty.ScoringFn : Type

Scoring functions measuring prediction accuracy. g(a, w, c) evaluates alternative a against target w in context c.

• indicator : ScoringFn

  𝟙{w ≤ a}: binary prefix match. With negLog → standard surprisal.

• distance : ScoringFn

  d_r(a, w): representational distance. With identity → information value.

• similarity : ScoringFn

  sim(r(a), r(w)): semantic similarity. @cite{meister-giulianelli-pimentel-2024}

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instDecidableEqScoringFn : DecidableEq ScoringFn

Equations

• Theories.Processing.PredictiveUncertainty.instDecidableEqScoringFn x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instReprScoringFn : Repr ScoringFn

Equations

• Theories.Processing.PredictiveUncertainty.instReprScoringFn = { reprPrec := Theories.Processing.PredictiveUncertainty.instReprScoringFn.repr }

def Theories.Processing.PredictiveUncertainty.instReprScoringFn.repr : ScoringFn → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Theories.Processing.PredictiveUncertainty.ForecastHorizon : Type

Forecast horizon: how many future symbols each alternative spans. h = 1 is standard surprisal's implicit horizon (next word only).

Equations

• Theories.Processing.PredictiveUncertainty.ForecastHorizon = Nat

inductive Theories.Processing.PredictiveUncertainty.RepLevel : Type

Representational level at which predictions are evaluated.

These tags name layers of abstraction — the kind of representational space in which alternatives are compared. They are not claims about specific layers of any particular neural network.

• lexical : RepLevel

  Decontextualised lexical identity (token / embedding)

• shallowSyntactic : RepLevel

  Shallow syntactic structure (linear order, POS)

• syntactic : RepLevel

  Compositional syntactic structure

• semantic : RepLevel

  Fully contextualised semantic content

• predictive : RepLevel

  Predictive distribution over next symbols

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instDecidableEqRepLevel : DecidableEq RepLevel

Equations

• Theories.Processing.PredictiveUncertainty.instDecidableEqRepLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instReprRepLevel : Repr RepLevel

Equations

• Theories.Processing.PredictiveUncertainty.instReprRepLevel = { reprPrec := Theories.Processing.PredictiveUncertainty.instReprRepLevel.repr }

def Theories.Processing.PredictiveUncertainty.instReprRepLevel.repr : RepLevel → Nat → Std.Format

Equations

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

structure Theories.Processing.PredictiveUncertainty.SurprisalConfig : Type

A generalised surprisal model: the complete parameter set for a specific processing measure.

• warp : WarpingFn
• scoring : ScoringFn
• horizon : ForecastHorizon
• level : RepLevel

def Theories.Processing.PredictiveUncertainty.instDecidableEqSurprisalConfig.decEq (x✝ x✝¹ : SurprisalConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instDecidableEqSurprisalConfig : DecidableEq SurprisalConfig

Equations

• Theories.Processing.PredictiveUncertainty.instDecidableEqSurprisalConfig = Theories.Processing.PredictiveUncertainty.instDecidableEqSurprisalConfig.decEq

@[implicit_reducible]

instance Theories.Processing.PredictiveUncertainty.instReprSurprisalConfig : Repr SurprisalConfig

Equations

• Theories.Processing.PredictiveUncertainty.instReprSurprisalConfig = { reprPrec := Theories.Processing.PredictiveUncertainty.instReprSurprisalConfig.repr }

def Theories.Processing.PredictiveUncertainty.instReprSurprisalConfig.repr : SurprisalConfig → Nat → Std.Format

Equations

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

def Theories.Processing.PredictiveUncertainty.standardSurprisal : SurprisalConfig

Standard surprisal: −log P(next word). @cite{levy-2008} @cite{smith-levy-2013}

Equations

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

def Theories.Processing.PredictiveUncertainty.informationValue (h : ForecastHorizon) (l : RepLevel) : SurprisalConfig

Incremental information value at temporal-representational resolution (h, l). @cite{giulianelli-etal-2026}

Equations

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

theorem Theories.Processing.PredictiveUncertainty.ias_recovers_surprisal : (have __src := informationValue 1 RepLevel.predictive; { warp := WarpingFn.negLog, scoring := ScoringFn.indicator, horizon := __src.horizon, level := __src.level }) = standardSurprisal

Standard surprisal is IAS at horizon 1 with predictive-level representation and negLog/indicator replacing identity/distance. Subsumption by construction.