Heitmeier, Chuang and Baayen (2026): The Discriminative Lexicon

This file formalizes the relation between linearity and regularity in [heitmeier-chuang-baayen-2026] (§16.6). The book's linear production maps handle inflectional systems with irregular forms: trained on empirical embeddings, its English past-tense model produces 94% of the regular and 74% of the irregular training verbs (§12.9). Meanings can instead be constructed, the meaning of walked as the meaning of walk plus a past-tense vector (Table 12.7; conceptualization is vector addition, (5.3), §16.3), which regularizes a system into "a reasonable approximation of a truly regular system, and for such a system, linear mappings appear to work quite well" (§16.6, Table 16.2); but with the meanings of held-out verbs reconstructed this way, "none of the irregular verbs was produced correctly" (§12.9). The file states why, in word-and-paradigm terms (Morphology.IsAnalogicallyRegular), on the Morphology.Realization interface: over imputed semantics, a lexeme vector plus an inflectional-function vector (imputed, the "imputed embeddings for stems and exponents" of §16.6), a linear map's form table satisfies proportional analogy by construction, so a table violating analogy is the paradigm of no linear DLM (not_exists_paradigm_eq_of_not_regular) and forces positive training loss (pos_weightedLoss_of_not_regular), and when the lexeme and function vectors are jointly independent a table is the paradigm of some linear DLM iff it is analogically regular (exists_paradigm_imputed_eq_iff). Over word-specific embeddings, by contrast, any table is the paradigm of some linear DLM as soon as the embeddings are linearly independent (exists_paradigm_eq_of_linearIndependent), which fills the irregular-linear cell of Table 16.2. The English past tense at the book's letter-trigram coding (§12.9) is the irregular table: walk, walked against go, went.

References

• [heitmeier-chuang-baayen-2026]

Imputed semantics

theorem HeitmeierChuangBaayen2026.not_exists_paradigm_eq_of_not_regular {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) {f : Lexeme → Cell → DiscriminativeLexicon.FormVec n} (hf : ¬Morphology.IsAnalogicallyRegular f) : ¬∃ (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)), D.paradigm (DiscriminativeLexicon.imputed σ ε) = f

A table violating proportional analogy is the paradigm of no linear DLM over imputed semantics: irregular forms cannot be produced from constructed meanings (§12.9).

Interpolation

theorem HeitmeierChuangBaayen2026.exists_linear_of_linearIndependent {d n : ℕ} {ι : Type u_3} {v : ι → DiscriminativeLexicon.MeaningVec d} (hv : LinearIndependent ℝ v) (w : ι → DiscriminativeLexicon.FormVec n) : ∃ (G : DiscriminativeLexicon.MeaningVec d →ₗ[ℝ] DiscriminativeLexicon.FormVec n), ∀ (i : ι), G (v i) = w i

A linearly independent family of meanings can be sent anywhere by a linear map.

theorem HeitmeierChuangBaayen2026.exists_paradigm_eq_of_linearIndependent {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} {s : Lexeme → Cell → DiscriminativeLexicon.MeaningVec d} (hs : LinearIndependent ℝ (Function.uncurry s)) (f : Lexeme → Cell → DiscriminativeLexicon.FormVec n) : ∃ (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)), D.paradigm s = f

Over word-specific, linearly independent embeddings any form table is the paradigm of some linear DLM, irregulars included: the irregular-linear cell of Table 16.2, the English past tense on empirical embeddings (§12.9).

theorem HeitmeierChuangBaayen2026.exists_paradigm_imputed_eq_iff {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) [Nonempty Lexeme] [Nonempty Cell] (hind : LinearIndependent ℝ (Sum.elim σ ε)) (f : Lexeme → Cell → DiscriminativeLexicon.FormVec n) : (∃ (D : DiscriminativeLexicon.Linear ℝ (DiscriminativeLexicon.FormVec n) (DiscriminativeLexicon.MeaningVec d)), D.paradigm (DiscriminativeLexicon.imputed σ ε) = f) ↔ Morphology.IsAnalogicallyRegular f

When the lexeme and inflectional-function vectors are jointly linearly independent, a table is the paradigm of some linear DLM over imputed semantics iff it is analogically regular: for a regularized system, linearity and regularity are the same constraint (§16.6).

The English past tense

inductive HeitmeierChuangBaayen2026.Letter : Type

The letters of walk, walked, go, went.

• w : Letter
• a : Letter
• l : Letter
• k : Letter
• e : Letter
• d : Letter
• g : Letter
• o : Letter
• n : Letter
• t : Letter

@[instance_reducible]

instance HeitmeierChuangBaayen2026.instDecidableEqLetter : DecidableEq Letter

Equations

• HeitmeierChuangBaayen2026.instDecidableEqLetter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive HeitmeierChuangBaayen2026.Verb : Type

A regular and a suppletive verb.

• walk : Verb
• go : Verb

inductive HeitmeierChuangBaayen2026.Tense : Type

The base and past cells.

• base : Tense
• past : Tense

def HeitmeierChuangBaayen2026.form : Verb → Tense → List Letter

The orthographic forms.

Equations

• One or more equations did not get rendered due to their size.
• HeitmeierChuangBaayen2026.form HeitmeierChuangBaayen2026.Verb.go HeitmeierChuangBaayen2026.Tense.base = [HeitmeierChuangBaayen2026.Letter.g, HeitmeierChuangBaayen2026.Letter.o]

def HeitmeierChuangBaayen2026.trigram : Fin 13 → Augmented Letter

The letter-trigram cue inventory of the four forms (§12.9 codes forms as letter trigrams).

Equations

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

def HeitmeierChuangBaayen2026.pastTense (v : Verb) (t : Tense) : DiscriminativeLexicon.FormVec 13

The past-tense form table at the trigram coding.

Equations

• HeitmeierChuangBaayen2026.pastTense v t = DiscriminativeLexicon.cueVector 3 HeitmeierChuangBaayen2026.trigram (HeitmeierChuangBaayen2026.form v t)

theorem HeitmeierChuangBaayen2026.pastTense_not_regular : ¬Morphology.IsAnalogicallyRegular pastTense

The English past tense violates proportional analogy: walked adds the cue ed# to walk, went adds nothing to go. So no linear DLM produces it from constructed meanings (not_exists_paradigm_eq_of_not_regular), while independent embeddings realise it (exists_paradigm_eq_of_linearIndependent), as in §12.9.

Training on a paradigm

noncomputable def HeitmeierChuangBaayen2026.paradigmExperience {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) [Fintype Lexeme] [Fintype Cell] (f : Lexeme → Cell → DiscriminativeLexicon.FormVec n) : DiscriminativeLexicon.TrainingExperience (Fintype.card (Lexeme × Cell)) n d

The paradigm as a training experience: imputed semantics as the semantic matrix, the form table as the form matrix.

Equations

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

theorem HeitmeierChuangBaayen2026.pos_weightedLoss_of_not_regular {d n : ℕ} {Lexeme : Type u_1} {Cell : Type u_2} (σ : Lexeme → DiscriminativeLexicon.MeaningVec d) (ε : Cell → DiscriminativeLexicon.MeaningVec d) [Fintype Lexeme] [Fintype Cell] {f : Lexeme → Cell → DiscriminativeLexicon.FormVec n} (hf : ¬Morphology.IsAnalogicallyRegular f) {q : DiscriminativeLexicon.FrequencyVector (Fintype.card (Lexeme × Cell))} (hq : ∀ (i : Fin (Fintype.card (Lexeme × Cell))), 0 < q i) (G : Matrix (Fin d) (Fin n) ℝ) : 0 < DiscriminativeLexicon.weightedLoss (paradigmExperience σ ε f) q G

Irregularity forces positive training loss: no mapping matrix fits a suppletive paradigm exactly, so every trained matrix carries residual error.