DLM training: endstate vs frequency-informed learning

[BCSBB19] [GB24] [Hei24] [HCB26]

The DLM's trained production map, characterised as the minimiser of a frequency-weighted quadratic loss. The choice of frequency weights q is the cognitive commitment (uniform = endstate learning, token counts = frequency-informed learning); the optimisation is fixed across theories.

Main definitions

• TrainingExperience, FrequencyVector, weightedLoss, IsERMSolution, with IsELSolution the uniform special case.
• TrainingExperience.sqrtScale, residualPairing, predictionEnergy.

Main results

• isERMSolution_iff_rescaled: only the empirical distribution of q matters.
• isERMSolution_iff_coordResidual: ERM is columnwise-unbeatable regression.
• isELSolution_sqrtScale_iff: FIL under q is EL on the √q-premultiplied experience ([Hei24]'s FIL-EL equivalence, also [HCAB24]; invertibility-free).
• isERMSolution_iff_residualPairing_eq_zero: the normal equations SᵀQ(SG − C) = 0 as an invertibility-free iff.
• IsERMSolution.apply_eq_of_mem_span / exists_apply_ne: fitted values are unique exactly on the span of experienced meanings.

The identification of DLM training with weighted regression — and existence of ERM solutions — is in Regression.lean, via the least-squares keystone Core.IsLeastSquares. The endstate theory is rule-agnostic: composing isERMSolution_iff_forall_column with the orthogonality principle Core.sum_whCorrection_eq_zero_iff identifies the ERM set with the equilibria of any error-driven rule in the Widrow-Hoff family.

TODO

Matrix closed form G = (SᵀS)⁻¹SᵀC (the uniqueness half is existsUnique_isERMSolution_iff in Regression.lean); approximate-decodability gap bounds for semSup.

Substrate types

structure Processing.Lexical.Discriminative.TrainingExperience (numEvents formDim meaningDim : ℕ) : Type

A training experience is a finite indexed family of (meaning, form) observation pairs — the rows of the papers' S and C matrices.

• meanings : Fin numEvents → MeaningVec meaningDim
• forms : Fin numEvents → FormVec formDim

@[reducible, inline]

abbrev Processing.Lexical.Discriminative.FrequencyVector (numEvents : ℕ) : Type

A frequency vector assigns one weight to each usage event — the diagonal of the papers' Q ([GB24] appendix). The choice of q is the cognitive commitment: uniform weights give EL and token counts give FIL (log-transforms distort learning per [GB24]). Nonnegativity is a per-theorem hypothesis.

Equations

• Processing.Lexical.Discriminative.FrequencyVector numEvents = (Fin numEvents → ℝ)

def Processing.Lexical.Discriminative.uniformFrequency (m : ℕ) : FrequencyVector m

The constant-1 frequency vector counts every event once (endstate learning).

Equations

• Processing.Lexical.Discriminative.uniformFrequency m x✝ = 1

def Processing.Lexical.Discriminative.FrequencyVector.totalMass {m : ℕ} (q : FrequencyVector m) : ℝ

The sum of all event weights.

Equations

• q.totalMass = ∑ i : Fin m, q i

noncomputable def Processing.Lexical.Discriminative.FrequencyVector.normalize {m : ℕ} (q : FrequencyVector m) : FrequencyVector m

q.normalize rescales q to sum to 1, giving the empirical distribution over events. For the PMF cast use PMF.ofRealWeightFn.

Equations

• q.normalize i = q i / q.totalMass

@[simp]

theorem Processing.Lexical.Discriminative.FrequencyVector.normalize_apply {m : ℕ} (q : FrequencyVector m) (i : Fin m) : q.normalize i = q i / q.totalMass

The weighted loss

def Processing.Lexical.Discriminative.squaredDist {n : ℕ} (a b : FormVec n) : ℝ

Squared coordinate-distance Σⱼ (a j − b j)² between two form vectors.

Equations

• Processing.Lexical.Discriminative.squaredDist a b = ∑ j : Fin n, (a j - b j) ^ 2

theorem Processing.Lexical.Discriminative.squaredDist_self {n : ℕ} (a : FormVec n) : squaredDist a a = 0

theorem Processing.Lexical.Discriminative.squaredDist_eq_zero_iff {n : ℕ} {a b : FormVec n} : squaredDist a b = 0 ↔ a = b

theorem Processing.Lexical.Discriminative.squaredDist_nonneg {n : ℕ} (a b : FormVec n) : 0 ≤ squaredDist a b

def Processing.Lexical.Discriminative.weightedLoss {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) : ℝ

The frequency-weighted training loss Σᵢ qᵢ · squaredDist (G (meanings i)) (forms i). This is the variational characterisation of the papers' procedural √Q normal-equations specification ([GB24] appendix; see weightedLoss_sqrtScale).

Equations

• Processing.Lexical.Discriminative.weightedLoss data q G = ∑ i : Fin m, q i * Processing.Lexical.Discriminative.squaredDist (G (data.meanings i)) (data.forms i)

theorem Processing.Lexical.Discriminative.weightedLoss_nonneg {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) (hq : ∀ (i : Fin m), 0 ≤ q i) : 0 ≤ weightedLoss data q G

theorem Processing.Lexical.Discriminative.weightedLoss_eq_zero_iff {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) (hq : ∀ (i : Fin m), 0 < q i) : weightedLoss data q G = 0 ↔ ∀ (i : Fin m), G (data.meanings i) = data.forms i

Under positive weights the loss vanishes exactly on interpolating maps.

Solution Props: ERM and EL

def Processing.Lexical.Discriminative.IsERMSolution {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) : Prop

G is an empirical risk minimiser (ERM) for data under q if no linear map achieves a smaller weighted loss.

Equations

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

@[reducible, inline]

abbrev Processing.Lexical.Discriminative.IsELSolution {m n d : ℕ} (data : TrainingExperience m n d) (G : MeaningVec d →ₗ[ℝ] FormVec n) : Prop

An endstate-learning (EL) solution is an ERM solution under uniform weights ([GB24] appendix).

Equations

• Processing.Lexical.Discriminative.IsELSolution data G = Processing.Lexical.Discriminative.IsERMSolution data (Processing.Lexical.Discriminative.uniformFrequency m) G

Structural theorems

theorem Processing.Lexical.Discriminative.weightedLoss_smul_frequency {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) (c : ℝ) : weightedLoss data (c • q) G = c * weightedLoss data q G

The weighted loss is linear in the frequency vector.

theorem Processing.Lexical.Discriminative.isERMSolution_iff_rescaled {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) {c : ℝ} (hc : 0 < c) : IsERMSolution data (c • q) G ↔ IsERMSolution data q G

ERM solutions are invariant under positive rescaling of the frequency vector — only relative frequencies matter.

Per-coordinate residual optimality

The loss separates across form coordinates — each column of G regresses one cue's support on the semantic dimensions, "optimal in the least-squares sense" ([HCB26] ch. 6) — so ERM is exactly columnwise unbeatability.

def Processing.Lexical.Discriminative.coordResidual {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (pred : Fin m → ℝ) (j₀ : Fin n) : ℝ

Weighted squared residual of a predicted column pred against form coordinate j₀ of the training data.

Equations

• Processing.Lexical.Discriminative.coordResidual data q pred j₀ = ∑ k : Fin m, q k * (pred k - data.forms k j₀) ^ 2

theorem Processing.Lexical.Discriminative.coordResidual_nonneg {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (hq : ∀ (i : Fin m), 0 ≤ q i) (pred : Fin m → ℝ) (j₀ : Fin n) : 0 ≤ coordResidual data q pred j₀

theorem Processing.Lexical.Discriminative.weightedLoss_eq_sum_coordResidual {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) : weightedLoss data q G = ∑ j : Fin n, coordResidual data q (fun (k : Fin m) => G (data.meanings k) j) j

The weighted loss is the sum over form coordinates of the per-coordinate residuals — each column of the production map is an independent regression.

theorem Processing.Lexical.Discriminative.isERMSolution_iff_coordResidual {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) : IsERMSolution data q G ↔ ∀ (j₀ : Fin n) (w : MeaningVec d →ₗ[ℝ] ℝ), coordResidual data q (fun (k : Fin m) => G (data.meanings k) j₀) j₀ ≤ coordResidual data q (fun (k : Fin m) => w (data.meanings k)) j₀

G is an ERM solution iff at every form coordinate its column's residual is at most that of any linear functional of the meanings — ERM is columnwise-unbeatable regression. No sign condition on q.

Rescaling invariance

The "frequency-vector-as-counts" view (DLM-paper-faithful) and the "frequency-vector-as-empirical-distribution" view (Bayesian-tradition) make identical predictions about which production maps are ERM-optimal. For the PMF (Fin m) cast of q.normalize, call PMF.ofRealWeightFn from Core.Probability.Constructions directly.

theorem Processing.Lexical.Discriminative.isERMSolution_normalize_iff {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) (h : 0 < q.totalMass) : IsERMSolution data q.normalize G ↔ IsERMSolution data q G

A frequency vector and its empirical distribution agree on which production maps are ERM solutions.

√Q transport

[GB24]'s appendix computes EL from the normal equations of regression and FIL by solving the EL problem on √Q-premultiplied S and C matrices; [HCB26] gives the same construction, and [Hei24] proves the equivalence with frequency-replicated training data via the closed-form normal-equations solution, under invertibility. Here the premultiplied experience is TrainingExperience.sqrtScale and the equivalence (isELSolution_sqrtScale_iff) is stated invertibility-free at the level of ERM solution sets. (Regression.lean applies the same √q scaling inside its design map.)

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

The √q-premultiplied training experience scales event i by √(q i) in both meaning and form — the √Q-premultiplication of S and C of [GB24]'s appendix and [HCB26].

Equations

• data.sqrtScale q = { meanings := fun (i : Fin m) => √(q i) • data.meanings i, forms := fun (i : Fin m) => √(q i) • data.forms i }

theorem Processing.Lexical.Discriminative.squaredDist_smul {n : ℕ} (c : ℝ) (a b : FormVec n) : squaredDist (c • a) (c • b) = c ^ 2 * squaredDist a b

Normal equations: ERM ⟺ residual orthogonality

[GB24]'s appendix and [Hei24] compute the mappings from the normal equations of regression (SᵀQ(SG − C) = 0 premultiplied into closed form under invertibility). Stated invertibility-free: G is an ERM solution iff every residual-prediction pairing vanishes — the first-order condition of the quadratic loss. Fitted values on experienced meanings are therefore unique across ERM solutions, which is what makes the model's predictions (and the semSup measures) well-defined properties of the training experience.

def Processing.Lexical.Discriminative.residualPairing {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G H : MeaningVec d →ₗ[ℝ] FormVec n) : ℝ

The q-weighted pairing ∑ᵢ qᵢ ⟨G(sᵢ) − cᵢ, H(sᵢ)⟩ of G's residuals with H's predictions. The normal equations say this vanishes for every H exactly at the ERM solutions.

Equations

• Processing.Lexical.Discriminative.residualPairing data q G H = ∑ i : Fin m, q i * ∑ j : Fin n, (G (data.meanings i) j - data.forms i j) * H (data.meanings i) j

def Processing.Lexical.Discriminative.predictionEnergy {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (H : MeaningVec d →ₗ[ℝ] FormVec n) : ℝ

The q-weighted squared magnitude of H's predictions on the training meanings.

Equations

• Processing.Lexical.Discriminative.predictionEnergy data q H = ∑ i : Fin m, q i * ∑ j : Fin n, H (data.meanings i) j ^ 2

theorem Processing.Lexical.Discriminative.predictionEnergy_nonneg {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (hq : ∀ (i : Fin m), 0 ≤ q i) (H : MeaningVec d →ₗ[ℝ] FormVec n) : 0 ≤ predictionEnergy data q H

theorem Processing.Lexical.Discriminative.residualPairing_smul {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G : MeaningVec d →ₗ[ℝ] FormVec n) (t : ℝ) (H : MeaningVec d →ₗ[ℝ] FormVec n) : residualPairing data q G (t • H) = t * residualPairing data q G H

theorem Processing.Lexical.Discriminative.predictionEnergy_smul {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (t : ℝ) (H : MeaningVec d →ₗ[ℝ] FormVec n) : predictionEnergy data q (t • H) = t ^ 2 * predictionEnergy data q H

theorem Processing.Lexical.Discriminative.weightedLoss_add {m n d : ℕ} (data : TrainingExperience m n d) (q : FrequencyVector m) (G H : MeaningVec d →ₗ[ℝ] FormVec n) : weightedLoss data q (G + H) = weightedLoss data q G + 2 * residualPairing data q G H + predictionEnergy data q H

Perturbing the weighted loss around G by H adds twice the residual pairing plus the energy of the perturbation.

ERM characterisations, uniqueness, and transport

theorem Processing.Lexical.Discriminative.IsERMSolution.abs_coord_sub_le {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 < q i) (hG : IsERMSolution data q G) {j₀ : Fin n} {w : MeaningVec d →ₗ[ℝ] ℝ} {ε : ℝ} (hw : coordResidual data q (fun (k : Fin m) => w (data.meanings k)) j₀ ≤ ε) (i : Fin m) : |G (data.meanings i) j₀ - data.forms i j₀| ≤ √(ε / q i)

Graded transfer: if some linear functional of the meanings decodes coordinate j₀ within total weighted squared error ε, then any ERM solution's prediction at a positively-weighted event deviates from the observed value by at most √(ε / q i). Exact decodability is the ε = 0 case (IsERMSolution.coord_eq_of_decodable).

theorem Processing.Lexical.Discriminative.IsERMSolution.coord_eq_of_decodable {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 < q i) (hG : IsERMSolution data q G) {j₀ : Fin n} {w : MeaningVec d →ₗ[ℝ] ℝ} (hw : ∀ (i : Fin m), w (data.meanings i) = data.forms i j₀) (i : Fin m) : G (data.meanings i) j₀ = data.forms i j₀

If some linear functional w of the meanings exactly reproduces coordinate j₀ of the observed forms, then any ERM solution under positive weights also reproduces it exactly on the training events — the ε = 0 case of IsERMSolution.abs_coord_sub_le.

theorem Processing.Lexical.Discriminative.isERMSolution_of_interpolates {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 ≤ q i) (hG : ∀ (i : Fin m), G (data.meanings i) = data.forms i) : IsERMSolution data q G

A map that reproduces every training form exactly is an ERM solution under any nonnegative weights — IsERMSolution is nonvacuous whenever the data are linearly interpolable.

theorem Processing.Lexical.Discriminative.isERMSolution_iff_residualPairing_eq_zero {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 ≤ q i) : IsERMSolution data q G ↔ ∀ (H : MeaningVec d →ₗ[ℝ] FormVec n), residualPairing data q G H = 0

G is an ERM solution iff every residual-prediction pairing vanishes. This is the first-order condition of the quadratic loss, with no invertibility hypothesis.

theorem Processing.Lexical.Discriminative.isERMSolution_iff_forall_column {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 ≤ q i) : IsERMSolution data q G ↔ ∀ (j : Fin n) (w : MeaningVec d →ₗ[ℝ] ℝ), ∑ i : Fin m, q i * ((G (data.meanings i) j - data.forms i j) * w (data.meanings i)) = 0

In the papers' columnwise form of the normal equations, G is an ERM solution iff at every form coordinate the q-weighted residual column is orthogonal to every linear functional of the meanings. Quantifying over functionals is SᵀQ(SG − C) = 0 with Sᵀ's rows generalized to the full dual space.

theorem Processing.Lexical.Discriminative.predictionEnergy_eq_zero_iff {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} (hq : ∀ (i : Fin m), 0 < q i) {H : MeaningVec d →ₗ[ℝ] FormVec n} : predictionEnergy data q H = 0 ↔ ∀ (i : Fin m), H (data.meanings i) = 0

Under positive weights the prediction energy is definite: it vanishes iff the predictions vanish on every training meaning.

theorem Processing.Lexical.Discriminative.IsERMSolution.apply_meanings_eq {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 < q i) {G' : MeaningVec d →ₗ[ℝ] FormVec n} (hG : IsERMSolution data q G) (hG' : IsERMSolution data q G') (i : Fin m) : G (data.meanings i) = G' (data.meanings i)

All ERM solutions under positive weights produce the same predicted form for every experienced meaning — fitted values are unique even when the ERM map is not.

theorem Processing.Lexical.Discriminative.IsERMSolution.apply_eq_of_mem_span {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 < q i) {G' : MeaningVec d →ₗ[ℝ] FormVec n} (hG : IsERMSolution data q G) (hG' : IsERMSolution data q G') {s : MeaningVec d} (hs : s ∈ Submodule.span ℝ (Set.range data.meanings)) : G s = G' s

ERM solutions agree at every meaning in the span of the experienced ones. Together with IsERMSolution.exists_apply_ne, novel-item predictions are well-defined exactly on the span of experience — the model generalizes by linear combination of experienced meanings and is unconstrained beyond them.

theorem Processing.Lexical.Discriminative.IsERMSolution.add_of_forall_eq_zero {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hG : IsERMSolution data q G) {H : MeaningVec d →ₗ[ℝ] FormVec n} (hH : ∀ (i : Fin m), H (data.meanings i) = 0) : IsERMSolution data q (G + H)

Adding a map that vanishes on every training meaning preserves ERM: the ERM solutions are closed under the data-annihilating directions (and by IsERMSolution.apply_meanings_eq they form exactly such a coset).

theorem Processing.Lexical.Discriminative.IsERMSolution.exists_apply_ne {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} [NeZero n] (hG : IsERMSolution data q G) {s : MeaningVec d} (hs : s ∉ Submodule.span ℝ (Set.range data.meanings)) : ∃ (G' : MeaningVec d →ₗ[ℝ] FormVec n), IsERMSolution data q G' ∧ G s ≠ G' s

Off the span of experienced meanings, ERM solutions are genuinely underdetermined — any ERM solution can be modified into another with a different prediction at any unexperienced meaning direction, by adding a correction supported on the annihilator of the span.

theorem Processing.Lexical.Discriminative.weightedLoss_sqrtScale {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 ≤ q i) : weightedLoss (data.sqrtScale q) (uniformFrequency m) G = weightedLoss data q G

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

theorem Processing.Lexical.Discriminative.isELSolution_sqrtScale_iff {m n d : ℕ} {data : TrainingExperience m n d} {q : FrequencyVector m} {G : MeaningVec d →ₗ[ℝ] FormVec n} (hq : ∀ (i : Fin m), 0 ≤ q i) : IsELSolution (data.sqrtScale q) G ↔ IsERMSolution data q G

FIL under q is exactly EL on the √q-premultiplied experience — [Hei24]'s FIL-EL equivalence, invertibility-free.

Connection to LinearDiscriminativeLexicon

def Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsTrainedOn {m n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (data : TrainingExperience m n d) (q : FrequencyVector m) : Prop

D is trained on data under weights q if its production map is an ERM solution.

Equations

• D.IsTrainedOn data q = Processing.Lexical.Discriminative.IsERMSolution data q D.production

@[reducible, inline]

abbrev Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsELTrainedOn {m n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (data : TrainingExperience m n d) : Prop

A DLM is EL-trained for given data iff its production map is the type-uniform ERM solution.

Equations

• D.IsELTrainedOn data = D.IsTrainedOn data (Processing.Lexical.Discriminative.uniformFrequency m)

@[reducible, inline]

abbrev Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsFILTrainedOn {m n d : ℕ} (D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)) (data : TrainingExperience m n d) (q : FrequencyVector m) : Prop

A DLM is FIL-trained with a given frequency vector iff its production map is the corresponding ERM solution.

Equations

• D.IsFILTrainedOn data q = D.IsTrainedOn data q

theorem Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsTrainedOn.semSup_eq_of_decodable {m n d : ℕ} {D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)} {data : TrainingExperience m n d} {q : FrequencyVector m} (hD : D.IsTrainedOn data q) (hq : ∀ (i : Fin m), 0 < q i) {j₀ : Fin n} {w : MeaningVec d →ₗ[ℝ] ℝ} (hw : ∀ (i : Fin m), w (data.meanings i) = data.forms i j₀) (i : Fin m) : semSup D (data.meanings i) j₀ = data.forms i j₀

A trained DLM's semantic support at a linearly decodable form coordinate equals the observed form value on every positively-weighted training event; any contrast carried by that coordinate — categorical or graded — transfers to semSup exactly.

theorem Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsTrainedOn.abs_semSup_sub_le {m n d : ℕ} {D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)} {data : TrainingExperience m n d} {q : FrequencyVector m} (hD : D.IsTrainedOn data q) (hq : ∀ (i : Fin m), 0 < q i) {j₀ : Fin n} {w : MeaningVec d →ₗ[ℝ] ℝ} {ε : ℝ} (hw : coordResidual data q (fun (k : Fin m) => w (data.meanings k)) j₀ ≤ ε) (i : Fin m) : |semSup D (data.meanings i) j₀ - data.forms i j₀| ≤ √(ε / q i)

Graded form of semSup_eq_of_decodable: a trained DLM's semantic support at a coordinate decoded within total weighted squared error ε deviates from the observed form value by at most √(ε / q i) — the transfer theorem in the graded form the applications actually use, where decoding is estimated rather than exact ([GB24]; [HCB26]).

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

Two DLMs trained on the same experience and weights have identical semantic support at every experienced meaning (IsERMSolution.apply_meanings_eq); semSup is thus a well-defined property of the training experience, not of the particular ERM solution.

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

semSup is well-defined for novel meanings too, as long as they lie in the span of experienced ones — the model generalizes by linear combination of experienced meanings. Off the span, predictions are underdetermined (IsERMSolution.exists_apply_ne).

theorem Processing.Lexical.Discriminative.LinearDiscriminativeLexicon.IsTrainedOn.semSupWord_eq_of_decodable {m n d : ℕ} {D : LinearDiscriminativeLexicon ℝ (FormVec n) (MeaningVec d)} {data : TrainingExperience m n d} {q : FrequencyVector m} (hD : D.IsTrainedOn data q) (hq : ∀ (i : Fin m), 0 < q i) {js : List (Fin n)} (hw : ∀ j ∈ js, ∃ (w : MeaningVec d →ₗ[ℝ] ℝ), ∀ (i : Fin m), w (data.meanings i) = data.forms i j) (i : Fin m) : semSupWord D (data.meanings i) js = (List.map (fun (j : Fin n) => data.forms i j) js).sum

Semantic Support for Form ([GB24] appendix; [HCB26]) — semSupWord over a word's cue coordinates — equals the sum of the observed form values whenever each coordinate is linearly decodable from the meanings.