structure ProcessingModel.ProcessingProfile : Type

A processing profile characterizing the difficulty of a linguistic dependency.

Each dimension is ordinal (higher = more of that factor). Comparison is via Pareto dominance — no numeric aggregation.

• locality : Nat

  Distance (words/nodes) between filler and integration site

• boundaries : Nat

  Clause or phrase boundaries crossed

• referentialLoad : Nat

  Referential processing load from intervening material (0 = none/pronominal, 1 = indefinite, 2 = definite/proper name)

• ease : Nat

  Retrieval facilitation: richer fillers, higher predictability (higher = easier retrieval, so this dimension is inverted in comparison)

def ProcessingModel.instReprProcessingProfile.repr : ProcessingProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance ProcessingModel.instReprProcessingProfile : Repr ProcessingProfile

Equations

• ProcessingModel.instReprProcessingProfile = { reprPrec := ProcessingModel.instReprProcessingProfile.repr }

def ProcessingModel.instDecidableEqProcessingProfile.decEq (x✝ x✝¹ : ProcessingProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ProcessingModel.instDecidableEqProcessingProfile : DecidableEq ProcessingProfile

Equations

• ProcessingModel.instDecidableEqProcessingProfile = ProcessingModel.instDecidableEqProcessingProfile.decEq

inductive ProcessingModel.CompareResult : Type

Result of comparing two processing profiles via Pareto dominance.

• harder : CompareResult
• easier : CompareResult
• equal : CompareResult
• incomparable : CompareResult

@[implicit_reducible]

instance ProcessingModel.instReprCompareResult : Repr CompareResult

Equations

• ProcessingModel.instReprCompareResult = { reprPrec := ProcessingModel.instReprCompareResult.repr }

def ProcessingModel.instReprCompareResult.repr : CompareResult → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance ProcessingModel.instDecidableEqCompareResult : DecidableEq CompareResult

Equations

• ProcessingModel.instDecidableEqCompareResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ProcessingModel.ProcessingProfile.compare (a b : ProcessingProfile) : CompareResult

Compare two processing profiles via Pareto dominance.

For cost dimensions (locality, boundaries, referentialLoad): higher = harder. For the benefit dimension (ease): higher = easier, so we invert.

Equations

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

class ProcessingModel.HasProcessingProfile (α : Type) : Type

Typeclass for types that can be mapped to processing profiles.

Any module claiming processing-based predictions must provide an instance, ensuring shared vocabulary across all comparison files.

• profile : α → ProcessingProfile

Monotonicity

These are the cognitive science claims underlying the processing model. Each states that increasing a cost dimension (or decreasing ease) cannot make processing easier. Stated as theorems with sorry per project convention.

These are provable from the Pareto dominance definition but not load-bearing — nothing downstream depends on them. Proof deferred in favor of deeper results.

theorem ProcessingModel.locality_monotone (p : ProcessingProfile) (k : Nat) : { locality := p.locality + k + 1, boundaries := p.boundaries, referentialLoad := p.referentialLoad, ease := p.ease }.compare p ≠ CompareResult.easier

More locality → not easier (working memory decay).

theorem ProcessingModel.boundaries_monotone (p : ProcessingProfile) (k : Nat) : { locality := p.locality, boundaries := p.boundaries + k + 1, referentialLoad := p.referentialLoad, ease := p.ease }.compare p ≠ CompareResult.easier

More boundaries → not easier (interference at retrieval).

theorem ProcessingModel.referentialLoad_monotone (p : ProcessingProfile) (k : Nat) : { locality := p.locality, boundaries := p.boundaries, referentialLoad := p.referentialLoad + k + 1, ease := p.ease }.compare p ≠ CompareResult.easier

More referential load → not easier (similarity-based interference).

theorem ProcessingModel.ease_monotone (p : ProcessingProfile) (k : Nat) : { locality := p.locality, boundaries := p.boundaries, referentialLoad := p.referentialLoad, ease := p.ease + k + 1 }.compare p ≠ CompareResult.harder

More ease → not harder (facilitation aids retrieval).

structure ProcessingModel.OrderingPrediction (α : Type) [HasProcessingProfile α] : Type

An ordering prediction: condition A should be harder than condition B.

• harder : α
• easier : α
• description : String

def ProcessingModel.instReprOrderingPrediction.repr {α✝ : Type} {inst✝ : HasProcessingProfile α✝} [Repr α✝] : OrderingPrediction α✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance ProcessingModel.instReprOrderingPrediction {α✝ : Type} {inst✝ : HasProcessingProfile α✝} [Repr α✝] : Repr (OrderingPrediction α✝)

Equations

• ProcessingModel.instReprOrderingPrediction = { reprPrec := ProcessingModel.instReprOrderingPrediction.repr }

def ProcessingModel.verifyOrdering {α : Type} [HasProcessingProfile α] (pred : OrderingPrediction α) : Bool

Verify that Pareto ordering matches the predicted direction.

Equations

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