Form and meaning coding for the DLM

[HCB26]

The interfaces by which linguistic objects feed the discriminative lexicon ([HCB26] ch. 4-5). A Linearizable type yields a symbol string; its cues are the k-factors of the boundary-augmented string — the same windowing as subregular locality (Subregular.SLGrammar) — and its form vector is the binary cue indicator (Box 4.2: the C matrix holds only 1s and 0s, not counts; the count refinement is where strict locality's unit margin lives, Subregular.SLGrammar). A SemanticPrimitives type yields a multiset of atomic semantic primitives — a lexeme plus inflectional-function tags (the book's term, ch. 5) — and conceptualize builds its meaning vector as the sum of primitive embeddings: the book's additive decomposition (eq. 5.3) and its verb for the operation (§16.3).

conceptualize_analogy is the general form of proportional analogy: a linear map respects every multiset-level relation among primitive decompositions. The stem-exponent fourth proportional of Studies/HeitmeierChuangBaayen2026 is the two-primitive case.

Form side

class Processing.Lexical.Discriminative.Linearizable (W : Type u_1) (Sym : outParam (Type u_2)) : Type (max u_1 u_2)

A form type that linearizes to a symbol string — the domain of the DLM's cue coding.

• symbols : W → List Sym

@[implicit_reducible]

instance Processing.Lexical.Discriminative.instLinearizableList {α : Type u_1} : Linearizable (List α) α

Equations

• Processing.Lexical.Discriminative.instLinearizableList = { symbols := id }

def Processing.Lexical.Discriminative.cues {W : Type u_1} {Sym : Type u_2} [Linearizable W Sym] (k : ℕ) (w : W) : List (Subregular.Augmented Sym)

The k-gram cues of a form: k-factors of the boundary-augmented symbol string.

Equations

• Processing.Lexical.Discriminative.cues k w = List.kFactors k (Subregular.boundary k (Processing.Lexical.Discriminative.Linearizable.symbols w))

def Processing.Lexical.Discriminative.cueVector {W : Type u_1} {Sym : Type u_2} [Linearizable W Sym] [DecidableEq Sym] (k : ℕ) {N : ℕ} (inv : Fin N → Subregular.Augmented Sym) (w : W) : FormVec N

The binary cue-indicator vector over a fixed cue inventory.

Equations

• Processing.Lexical.Discriminative.cueVector k inv w j = if inv j ∈ Processing.Lexical.Discriminative.cues k w then 1 else 0

def Processing.Lexical.Discriminative.Discriminable {W : Type u_1} {Sym : Type u_2} [Linearizable W Sym] (k : ℕ) (lexicon : Set W) : Prop

A lexicon is discriminable at width k when cue coding separates its forms; failures are homographs ([HCB26] ch. 7).

Equations

• Processing.Lexical.Discriminative.Discriminable k lexicon = Set.InjOn (Processing.Lexical.Discriminative.cues k) lexicon

Meaning side

class Processing.Lexical.Discriminative.SemanticPrimitives (M : Type u_3) (Prim : outParam (Type u_4)) : Type (max u_3 u_4)

A meaning type with atomic semantic primitives — a lexeme and inflectional-function tags.

• primitives : M → Multiset Prim

def Processing.Lexical.Discriminative.conceptualize {M : Type u_3} {Prim : Type u_4} [SemanticPrimitives M Prim] {d : ℕ} (emb : Prim → MeaningVec d) (m : M) : MeaningVec d

Conceptualization: the meaning vector of an object is the sum of its primitives' vectors.

Equations

• Processing.Lexical.Discriminative.conceptualize emb m = (Multiset.map emb (Processing.Lexical.Discriminative.primitives m)).sum

theorem Processing.Lexical.Discriminative.conceptualize_add_of_primitives_add {M : Type u_3} {Prim : Type u_4} [SemanticPrimitives M Prim] {d : ℕ} (emb : Prim → MeaningVec d) {m₁ m₂ m₃ m₄ : M} (h : primitives m₁ + primitives m₂ = primitives m₃ + primitives m₄) : conceptualize emb m₁ + conceptualize emb m₂ = conceptualize emb m₃ + conceptualize emb m₄

theorem Processing.Lexical.Discriminative.conceptualize_analogy {M : Type u_3} {Prim : Type u_4} [SemanticPrimitives M Prim] {d n : ℕ} (emb : Prim → MeaningVec d) (G : MeaningVec d →ₗ[ℝ] FormVec n) {m₁ m₂ m₃ m₄ : M} (h : primitives m₁ + primitives m₂ = primitives m₃ + primitives m₄) : G (conceptualize emb m₁) + G (conceptualize emb m₂) = G (conceptualize emb m₃) + G (conceptualize emb m₄)

Generic proportional analogy: any linear map respects every multiset-level relation among primitive decompositions. The stem-exponent fourth proportional is the case {lex, PL} + {lex', SG} = {lex, SG} + {lex', PL}.