DLM training: endstate and frequency-informed learning

A DLM is trained by solving SG = C in the least-squares sense: the mapping matrix G minimises the frequency-weighted loss ∑ᵢ qᵢ ‖(SG − C)ᵢ‖² over the semantic matrix S and form matrix C of the training experience. The weights are the cognitive commitment, uniform for endstate learning (EL) and token counts for frequency-informed learning (FIL, [heitmeier-chuang-axen-baayen-2024]); the optimisation is fixed. The loss separates over form coordinates, so each column of G is a vector least-squares problem for the √Q-scaled design √Q S, where Mathlib characterises the minimisers by the adjoint (Core.IsLeastSquares). That gives the normal equations SᵀQ(SG − C) = 0 of [gahl-baayen-2024]'s appendix and their closed form (SᵀQS)⁻¹SᵀQC, existence, uniqueness of the fitted values SG (hence of semSup at experienced meanings), the solution coset, and the identification of FIL under q with EL on the √Q-premultiplied experience ([heitmeier-2024]).

Main declarations

• TrainingExperience, FrequencyVector, weightedLoss, IsTrained, IsELTrained.
• isTrained_iff_forall_isLeastSquares, exists_isTrained: training is columnwise least squares, and solutions exist.
• isTrained_iff, isTrained_closedForm: the normal equations SᵀQ(SG − C) = 0 and their closed form.
• IsTrained.mul_eq, IsTrained.vecMul_eq_of_mem_span, IsTrained.exists_vecMul_ne, existsUnique_isTrained_iff: fitted values are unique exactly on the span of experience.
• isELTrained_sqrtScale_iff: FIL under q is EL on TrainingExperience.sqrtScale.
• Linear.IsTrainedOn and the semSup transfer theorems.
• IsTrained.sum_smul_mul_eq_of_decodable, Linear.IsELTrainedOn.production_centroid_eq_of_decodable: fitted and observed forms agree on every linearly decodable average, so a trained DLM sends the centroid of a linearly decodable set of meanings to the centroid of its forms.

References

• [Y.-Y. Chuang, M. J. Bell, Y.-H. Tseng and R. H. Baayen, Word-specific tonal realizations in Mandarin (2026)][chuang-bell-tseng-baayen-2026]
• [S. Gahl and R. H. Baayen, Time and thyme again (2024)][gahl-baayen-2024]
• [M. Heitmeier, Mappings in the Discriminative Lexicon Model (2024)][heitmeier-2024]
• [M. Heitmeier, Y.-Y. Chuang, S. D. Axen and R. H. Baayen, Frequency effects in linear discriminative learning (2024)][heitmeier-chuang-axen-baayen-2024]
• [M. Heitmeier, Y.-Y. Chuang and R. H. Baayen, The Discriminative Lexicon (2026)][heitmeier-chuang-baayen-2026]
• [Y. Lu, Y.-Y. Chuang and R. H. Baayen, The realization of tones in spontaneous spoken Taiwan Mandarin (2026)][lu-chuang-baayen-2026]

The training problem

structure DiscriminativeLexicon.TrainingExperience (numEvents formDim meaningDim : ℕ) : Type

A training experience: the papers' semantic matrix S and form matrix C, one usage event per row.

• S : Matrix (Fin numEvents) (Fin meaningDim) ℝ

  The semantic matrix: the experienced meanings as rows.

• C : Matrix (Fin numEvents) (Fin formDim) ℝ

  The form matrix: the observed forms as rows.

@[reducible, inline]

abbrev DiscriminativeLexicon.FrequencyVector (numEvents : ℕ) : Type

A frequency vector weights each usage event, the diagonal of the papers' Q. Uniform weights give EL, token counts FIL ([gahl-baayen-2024]'s appendix, which warns against log-transforming them).

Equations

• DiscriminativeLexicon.FrequencyVector numEvents = (Fin numEvents → NNReal)

def DiscriminativeLexicon.FrequencyVector.Q {m : ℕ} (q : FrequencyVector m) : Matrix (Fin m) (Fin m) ℝ

The weight matrix Q.

Equations

• q.Q = Matrix.diagonal fun (i : Fin m) => ↑(q i)

noncomputable def DiscriminativeLexicon.FrequencyVector.sqrtQ {m : ℕ} (q : FrequencyVector m) : Matrix (Fin m) (Fin m) ℝ

Its square root, the √Q of the papers' appendix.

Equations

• q.sqrtQ = Matrix.diagonal fun (i : Fin m) => √↑(q i)

@[simp]

theorem DiscriminativeLexicon.FrequencyVector.Q_one {m : ℕ} : Q 1 = 1

@[simp]

theorem DiscriminativeLexicon.FrequencyVector.sqrtQ_one {m : ℕ} : sqrtQ 1 = 1

@[simp]

theorem DiscriminativeLexicon.FrequencyVector.sqrtQ_transpose {m : ℕ} (q : FrequencyVector m) : q.sqrtQ.transpose = q.sqrtQ

theorem DiscriminativeLexicon.FrequencyVector.sqrtQ_mul_sqrtQ {m : ℕ} (q : FrequencyVector m) : q.sqrtQ * q.sqrtQ = q.Q

noncomputable def DiscriminativeLexicon.TrainingExperience.sqrtScale {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) : TrainingExperience m n d

The √Q-premultiplied experience (√Q S, √Q C) of the papers' appendix.

Equations

• data.sqrtScale q = { S := q.sqrtQ * data.S, C := q.sqrtQ * data.C }

@[simp]

theorem DiscriminativeLexicon.TrainingExperience.sqrtScale_S {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (i : Fin m) : (data.sqrtScale q).S i = √↑(q i) • data.S i

@[simp]

theorem DiscriminativeLexicon.TrainingExperience.sqrtScale_C {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (i : Fin m) : (data.sqrtScale q).C i = √↑(q i) • data.C i

def DiscriminativeLexicon.weightedLoss {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : ℝ

The frequency-weighted training loss ∑ᵢ qᵢ ‖(SG − C)ᵢ‖².

Equations

• DiscriminativeLexicon.weightedLoss data q G = ∑ i : Fin m, ↑(q i) * (data.S * G - data.C) i ⬝ᵥ (data.S * G - data.C) i

theorem DiscriminativeLexicon.weightedLoss_nonneg {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : 0 ≤ weightedLoss data q G

theorem DiscriminativeLexicon.weightedLoss_eq_zero_iff {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) (hq : ∀ (i : Fin m), 0 < q i) : weightedLoss data q G = 0 ↔ data.S * G = data.C

Under positive weights the loss vanishes exactly on interpolating maps.

def DiscriminativeLexicon.IsTrained {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : Prop

G is trained on data under q when it minimises the weighted loss over all mapping matrices: SG = C solved by least squares.

Equations

• DiscriminativeLexicon.IsTrained data q G = IsMinOn (DiscriminativeLexicon.weightedLoss data q) Set.univ G

@[reducible, inline]

abbrev DiscriminativeLexicon.IsELTrained {m n d : ℕ} (data : TrainingExperience m n d) (G : Matrix (Fin d) (Fin n) ℝ) : Prop

Endstate learning: training under uniform weights ([gahl-baayen-2024] appendix).

Equations

• DiscriminativeLexicon.IsELTrained data G = DiscriminativeLexicon.IsTrained data 1 G

theorem DiscriminativeLexicon.weightedLoss_smul {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) (c : NNReal) : weightedLoss data (c • q) G = ↑c * weightedLoss data q G

theorem DiscriminativeLexicon.isTrained_smul_iff {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) {c : NNReal} (hc : 0 < c) : IsTrained data (c • q) G ↔ IsTrained data q G

Only relative frequencies matter.

theorem DiscriminativeLexicon.weightedLoss_sqrtScale {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : weightedLoss (data.sqrtScale q) 1 G = weightedLoss data q G

The uniform-weight loss on the √Q-premultiplied experience is the q-weighted loss.

theorem DiscriminativeLexicon.isELTrained_sqrtScale_iff {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : IsELTrained (data.sqrtScale q) G ↔ IsTrained data q G

FIL under q is exactly EL on the √Q-premultiplied experience: [heitmeier-2024]'s FIL–EL equivalence, invertibility-free.

Training as columnwise least squares

The loss separates over form coordinates: column j of G is a least-squares solution of the √Q-scaled regression of column j of C on S, a vector problem in Euclidean space.

theorem DiscriminativeLexicon.weightedLoss_eq_sum_norm_sq {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : weightedLoss data q G = ∑ j : Fin n, ‖WithLp.toLp 2 ((q.sqrtQ * data.C).transpose j) - (Matrix.toEuclideanLin (q.sqrtQ * data.S)) (WithLp.toLp 2 (G.transpose j))‖ ^ 2

The weighted loss is the sum over form coordinates of the columns' squared residuals.

theorem DiscriminativeLexicon.isTrained_iff_forall_isLeastSquares {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : IsTrained data q G ↔ ∀ (j : Fin n), Core.IsLeastSquares (Matrix.toEuclideanLin (q.sqrtQ * data.S)) (WithLp.toLp 2 ((q.sqrtQ * data.C).transpose j)) (WithLp.toLp 2 (G.transpose j))

Training is columnwise least squares: each column of G minimises the residual of the corresponding scaled regression.

theorem DiscriminativeLexicon.exists_isTrained {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) : ∃ (G : Matrix (Fin d) (Fin n) ℝ), IsTrained data q G

Trained mapping matrices exist.

The normal equations

theorem DiscriminativeLexicon.isTrained_iff {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : Matrix (Fin d) (Fin n) ℝ) : IsTrained data q G ↔ data.S.transpose * q.Q * (data.S * G - data.C) = 0

Normal equations: G is trained iff SᵀQ(SG − C) = 0 ([gahl-baayen-2024] (A2), (A4)), from Mathlib's adjoint characterisation of least squares, column by column.

theorem DiscriminativeLexicon.isTrained_closedForm {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (hS : IsUnit (data.S.transpose * q.Q * data.S)) : IsTrained data q ((data.S.transpose * q.Q * data.S)⁻¹ * (data.S.transpose * q.Q * data.C))

Closed form: when SᵀQS is invertible, G = (SᵀQS)⁻¹SᵀQC is trained ([gahl-baayen-2024] (A2), (A4)).

theorem DiscriminativeLexicon.isELTrained_closedForm {m n d : ℕ} (data : TrainingExperience m n d) (hS : IsUnit (data.S.transpose * data.S)) : IsELTrained data ((data.S.transpose * data.S)⁻¹ * (data.S.transpose * data.C))

The endstate closed form G = (SᵀS)⁻¹SᵀC ([gahl-baayen-2024] (A2)).

theorem DiscriminativeLexicon.IsTrained.sum_smul_sub_eq_zero {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : Matrix (Fin d) (Fin n) ℝ} (hG : IsTrained data q G) (w : MeaningVec d →ₗ[ℝ] ℝ) : ∑ i : Fin m, (↑(q i) * w (data.S i)) • ((data.S * G) i - data.C i) = 0

The normal equations in vector form: the q-weighted residual rows, weighted further by any linear functional of the meanings, sum to zero.

theorem DiscriminativeLexicon.IsTrained.sum_smul_mul_eq_of_decodable {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : Matrix (Fin d) (Fin n) ℝ} (hG : IsTrained data q G) {P : Finset (Fin m)} {w : MeaningVec d →ₗ[ℝ] ℝ} (hw : ∀ (i : Fin m), w (data.S i) = if i ∈ P then 1 else 0) : ∑ i ∈ P, ↑(q i) • (data.S * G) i = ∑ i ∈ P, ↑(q i) • data.C i

Whenever membership in a set P of usage events is a linear functional of the meanings, the q-weighted sums of the fitted and of the observed forms over P agree.

Fitted values

theorem DiscriminativeLexicon.IsTrained.mul_eq {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : Matrix (Fin d) (Fin n) ℝ} (hq : ∀ (i : Fin m), 0 < q i) {G' : Matrix (Fin d) (Fin n) ℝ} (hG : IsTrained data q G) (hG' : IsTrained data q G') : data.S * G = data.S * G'

All trained matrices under positive weights produce the same predicted forms SG on the training events: fitted values are unique even when G is not.

theorem DiscriminativeLexicon.IsTrained.vecMul_eq_of_mem_span {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : Matrix (Fin d) (Fin n) ℝ} (hq : ∀ (i : Fin m), 0 < q i) {G' : Matrix (Fin d) (Fin n) ℝ} (hG : IsTrained data q G) (hG' : IsTrained data q G') {s : MeaningVec d} (hs : s ∈ Submodule.span ℝ (Set.range data.S)) : Matrix.vecMul s G = Matrix.vecMul s G'

Trained matrices agree at every meaning in the span of the experienced ones.

theorem DiscriminativeLexicon.IsTrained.add_of_mul_eq_zero {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : Matrix (Fin d) (Fin n) ℝ} (hG : IsTrained data q G) {H : Matrix (Fin d) (Fin n) ℝ} (hH : data.S * H = 0) : IsTrained data q (G + H)

Adding a matrix that annihilates every training meaning preserves training.

theorem DiscriminativeLexicon.IsTrained.exists_vecMul_ne {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : Matrix (Fin d) (Fin n) ℝ} [NeZero n] (hG : IsTrained data q G) {s : MeaningVec d} (hs : s ∉ Submodule.span ℝ (Set.range data.S)) : ∃ (G' : Matrix (Fin d) (Fin n) ℝ), IsTrained data q G' ∧ Matrix.vecMul s G ≠ Matrix.vecMul s G'

Off the span of experienced meanings, training is underdetermined: any trained matrix can be modified into another with a different prediction at an unexperienced meaning.

theorem DiscriminativeLexicon.existsUnique_isTrained_iff {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} [NeZero n] (hq : ∀ (i : Fin m), 0 < q i) : (∃! G : Matrix (Fin d) (Fin n) ℝ, IsTrained data q G) ↔ Submodule.span ℝ (Set.range data.S) = ⊤

The trained matrix is uniquely determined exactly when the experienced meanings span the meaning space: the coordinate-free form of the papers' full-column-rank condition on the closed-form solution ([gahl-baayen-2024] appendix; [heitmeier-2024]).

theorem DiscriminativeLexicon.IsTrained.mul_apply_eq_of_decodable {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : Matrix (Fin d) (Fin n) ℝ} (hq : ∀ (i : Fin m), 0 < q i) (hG : IsTrained data q G) {j₀ : Fin n} {w : MeaningVec d →ₗ[ℝ] ℝ} (hw : ∀ (i : Fin m), w (data.S i) = data.C i j₀) (i : Fin m) : (data.S * G) i j₀ = data.C i j₀

If some linear functional of the meanings reproduces column j₀ of the observed forms exactly, so does every trained matrix under positive weights, on every training event.

Trained lexicons

def DiscriminativeLexicon.Linear.productionMatrix {n d : ℕ} (D : Linear ℝ (FormVec n) (MeaningVec d)) : Matrix (Fin d) (Fin n) ℝ

The mapping matrix of the production map, acting on row vectors: ĉ = sG.

Equations

• D.productionMatrix = (LinearMap.toMatrix' D.production).transpose

theorem DiscriminativeLexicon.Linear.production_eq_vecMul {n d : ℕ} (D : Linear ℝ (FormVec n) (MeaningVec d)) (s : MeaningVec d) : D.production s = Matrix.vecMul s D.productionMatrix

theorem DiscriminativeLexicon.Linear.mul_productionMatrix_apply {m n d : ℕ} (data : TrainingExperience m n d) (D : Linear ℝ (FormVec n) (MeaningVec d)) (i : Fin m) : (data.S * D.productionMatrix) i = D.production (data.S i)

Row i of the fitted forms is the production map at the i-th experienced meaning.

@[simp]

theorem DiscriminativeLexicon.Linear.productionMatrix_mk {n d : ℕ} (F : FormVec n →ₗ[ℝ] MeaningVec d) (G : Matrix (Fin d) (Fin n) ℝ) : { comprehension := F, production := Matrix.toLin' G.transpose }.productionMatrix = G

def DiscriminativeLexicon.Linear.IsTrainedOn {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (D : Linear ℝ (FormVec n) (MeaningVec d)) : Prop

D is trained on data under weights q if its production matrix is. Only the production side is constrained, as in the papers' production models.

Equations

• DiscriminativeLexicon.Linear.IsTrainedOn data q D = DiscriminativeLexicon.IsTrained data q D.productionMatrix

@[reducible, inline]

abbrev DiscriminativeLexicon.Linear.IsELTrainedOn {m n d : ℕ} (data : TrainingExperience m n d) (D : Linear ℝ (FormVec n) (MeaningVec d)) : Prop

A DLM is EL-trained on data iff its production matrix is trained under uniform weights.

Equations

• DiscriminativeLexicon.Linear.IsELTrainedOn data D = DiscriminativeLexicon.Linear.IsTrainedOn data 1 D

theorem DiscriminativeLexicon.Linear.IsTrainedOn.semSup_eq_of_decodable {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {D : Linear ℝ (FormVec n) (MeaningVec d)} (hD : IsTrainedOn data q D) (hq : ∀ (i : Fin m), 0 < q i) {j₀ : Fin n} {w : MeaningVec d →ₗ[ℝ] ℝ} (hw : ∀ (i : Fin m), w (data.S i) = data.C i j₀) (i : Fin m) : semSup D (data.S i) j₀ = data.C i j₀

A trained DLM's semantic support at a linearly decodable form coordinate equals the observed form value on every training event.

theorem DiscriminativeLexicon.Linear.IsTrainedOn.semSup_eq {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {D D' : Linear ℝ (FormVec n) (MeaningVec d)} (hD : IsTrainedOn data q D) (hD' : IsTrainedOn data q D') (hq : ∀ (i : Fin m), 0 < q i) (i : Fin m) (j : Fin n) : semSup D (data.S i) j = semSup D' (data.S i) j

Two DLMs trained on the same experience and weights have identical semantic support at every experienced meaning: semSup is a property of the training experience, not of the particular trained matrix.

theorem DiscriminativeLexicon.Linear.IsTrainedOn.semSup_eq_of_mem_span {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {D D' : Linear ℝ (FormVec n) (MeaningVec d)} (hD : IsTrainedOn data q D) (hD' : IsTrainedOn data q D') (hq : ∀ (i : Fin m), 0 < q i) {s : MeaningVec d} (hs : s ∈ Submodule.span ℝ (Set.range data.S)) (j : Fin n) : semSup D s j = semSup D' s j

semSup is well-defined at novel meanings in the span of experienced ones.

theorem DiscriminativeLexicon.Linear.IsTrainedOn.semSupWord_eq_of_decodable {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {D : Linear ℝ (FormVec n) (MeaningVec d)} (hD : IsTrainedOn data q D) (hq : ∀ (i : Fin m), 0 < q i) {c : FormVec n} (hw : ∀ (j : Fin n), c j ≠ 0 → ∃ (w : MeaningVec d →ₗ[ℝ] ℝ), ∀ (i : Fin m), w (data.S i) = data.C i j) (i : Fin m) : semSupWord D (data.S i) c = data.C i ⬝ᵥ c

Semantic Support for Form ([gahl-baayen-2024] appendix) at a form vector equals the observed form's own support whenever each coordinate the form vector touches is linearly decodable from the meanings.

Centroids

theorem DiscriminativeLexicon.Linear.IsELTrainedOn.production_centroid_eq_of_decodable {m n d : ℕ} {data : TrainingExperience m n d} {D : Linear ℝ (FormVec n) (MeaningVec d)} (hD : IsELTrainedOn data D) {P : Finset (Fin m)} (hP : P.Nonempty) {w : MeaningVec d →ₗ[ℝ] ℝ} (hw : ∀ (i : Fin m), w (data.S i) = if i ∈ P then 1 else 0) : D.production (Finset.centroid ℝ P data.S) = Finset.centroid ℝ P data.C

Centroids under training ([chuang-bell-tseng-baayen-2026] §3.4, [lu-chuang-baayen-2026] §4.4): whenever membership in a nonempty set P of usage events is a linear functional of the meanings, an EL-trained DLM sends the centroid of P's meanings exactly to the centroid of P's observed forms. Linearity alone sends it to the centroid of the predicted forms (LinearMap.map_centroid); training makes those coincide with the observed ones.