Paradigm linkage: content paradigms, form paradigms, and correspondence

Inflectional morphology relates three levels of representation ([Stu12]; the book-length apparatus is [Stu16]): a lexeme's content paradigm of cells ⟨L, σ⟩ pairing a lexeme with a syntacticosemantic property set, a stem's form paradigm of cells ⟨Z, τ⟩ pairing a stem with a property set it inflects for, and the realized paradigm of word forms. A content cell is realized by being linked to its form correspondents, whose realizations it shares. The correspondence is a finite relation in factored presentation: a stem selection stems : L → P → Finset Z and a lexeme-sensitive property mapping pm : L → P → P. Canonically the relation is the graph of ⟨l, σ⟩ ↦ ⟨root l, σ⟩ ([stump-2006]'s universal default rule of paradigm linkage).

Canonical linkage is the typological extreme against which deviations are calibrated — [Cor07]'s canonical-typology method, with the axes read off the correspondence relation's standard properties. IsTotal: every content cell has a form correspondent. IsUnivalent: at most one. IsStemInvariant: one stem serves all of a lexeme's cells. IsInjective: no two content cells share a correspondent. IsPropertyPreserving: a correspondent carries the content cell's own property set. Each named noncanonical phenomenon negates one axis: defectiveness totality ([Stu12] §3.1), overabundance univalence ([Tho11]'s cell-mates), suppletion stem invariance (§3.4), syncretism injectivity (§3.2), and deponency and functor-argument reversal property preservation (§3.3).

Stem invariance is one instance of a projection-indexed family: InvariantAlong p asks the composite p ∘ stems to be constant per lexeme. Instantiated at a consumer-supplied inflection-class projection cls : Z → K it yields heteroclisis — form correspondents drawn from form paradigms of two or more inflection classes ([stump-2006]). Because constancy transfers along any projection (InvariantAlong.comp), heteroclisis entails stem non-invariance (IsHeteroclite.isSuppletive): heteroclisis is "a kind of stem alternation" even when the stems are phonologically identical, [stump-2006]'s reading of Czech PRAMEN, whose two stems differ in class but not in form.

Main declarations

• Linkage L Z P — the correspondence in factored presentation: finite stem selection and lexeme-sensitive property mapping
• Linkage.corr, Linkage.realize — the form-correspondent set of a content cell and the realized paradigm over it
• Linkage.IsTotal, IsUnivalent, IsStemInvariant, IsInjective, IsPropertyPreserving — the axes of canonical linkage; IsCanonical bundles them; InvariantAlong is the projection-indexed generalization of stem invariance
• Linkage.IsDefective, IsOverabundant, IsSuppletive, IsHeteroclite, IsSyncretic, IsUnfaithful — the six deviations, each an axis failure (isDefective_iff_not_isTotal, isOverabundant_iff_not_isUnivalent, isSyncretic_iff_not_isInjective, …)
• Linkage.IsHeteroclite.isSuppletive — heteroclisis entails stem non-invariance
• Linkage.HasCellMates — distinct realized forms at one cell; entails IsOverabundant
• Linkage.IsVirtual — a form cell no content cell corresponds to
• Linkage.canonical / canonical_isCanonical — the total, lexeme-blind, one-stem linkage, canonical on all axes
• Linkage.realize_eq_of_corr_eq, realize_eq_of_corr_eq_lexeme — shared correspondents force shared realizations, within and across lexemes

structure Morphology.Linkage (L : Type u_1) (Z : Type u_2) (P : Type u_3) : Type (max (max u_1 u_2) u_3)

A paradigm linkage ([Stu12]) from the vantage of a single lexeme: the two components of the form-correspondence relation. stems selects the finite set of stems realizing a content cell — empty at a gap in the stem specification, more than one at an overabundant cell; pm carries a content cell's property set to its form correspondents', and may consult the lexeme. Canonically stems is singleton-valued and constant in the property set and pm is the identity.

• stems : L → P → Finset Z

  The stems realizing a content cell ⟨l, σ⟩: empty where the stem specification has a gap, non-singleton where the cell is overabundant.

• pm : L → P → P

  The property mapping carrying a content cell's property set to its form correspondents', consulting the lexeme for functor-argument reversal.

def Morphology.Linkage.corr {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (l : L) (σ : P) : Finset (Z × P)

The form correspondents of a content cell ⟨l, σ⟩: each selected stem paired with the mapped property set — empty where the stem specification has a gap.

Equations

• ℓ.corr l σ = ℓ.stems l σ ×ˢ {ℓ.pm l σ}

@[simp]

theorem Morphology.Linkage.mem_corr {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) {l : L} {σ : P} {zτ : Z × P} : zτ ∈ ℓ.corr l σ ↔ zτ.1 ∈ ℓ.stems l σ ∧ zτ.2 = ℓ.pm l σ

@[simp]

theorem Morphology.Linkage.corr_nonempty {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (l : L) (σ : P) : (ℓ.corr l σ).Nonempty ↔ (ℓ.stems l σ).Nonempty

@[simp]

theorem Morphology.Linkage.card_corr {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (l : L) (σ : P) : (ℓ.corr l σ).card = (ℓ.stems l σ).card

def Morphology.Linkage.realize {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] (realizeForm : Z → P → W) (l : L) (σ : P) : Finset (W × P)

The realized paradigm on content cells: a content cell realizes as its form correspondents do. realizeForm supplies the form-cell realization; the result is empty exactly where the correspondent set is.

Equations

• ℓ.realize realizeForm l σ = Finset.image (fun (z : Z) => realizeForm z (ℓ.pm l σ)) (ℓ.stems l σ) ×ˢ {ℓ.pm l σ}

@[simp]

theorem Morphology.Linkage.mem_realize {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] {realizeForm : Z → P → W} {l : L} {σ : P} {wτ : W × P} : wτ ∈ ℓ.realize realizeForm l σ ↔ ∃ z ∈ ℓ.stems l σ, wτ = (realizeForm z (ℓ.pm l σ), ℓ.pm l σ)

The axes of canonical linkage

def Morphology.Linkage.IsTotal {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Totality: every content cell has a form correspondent. Defectiveness is the failure.

Equations

• ℓ.IsTotal = ∀ (l : L) (σ : P), (ℓ.stems l σ).Nonempty

def Morphology.Linkage.IsUnivalent {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Univalence: every content cell has at most one form correspondent. Overabundance is the failure.

Equations

• ℓ.IsUnivalent = ∀ (l : L) (σ : P), (ℓ.stems l σ).card ≤ 1

def Morphology.Linkage.InvariantAlong {L : Type u_1} {Z : Type u_2} {P : Type u_3} {X : Type u_5} (ℓ : Linkage L Z P) (p : Z → X) : Prop

Invariance along a projection: the composite p ∘ stems is constant on each lexeme's paradigm. At p := id this is stem invariance; at an inflection-class projection it is the axis heteroclisis negates. Undefined cells impose no constraint.

Equations

• ℓ.InvariantAlong p = ∀ (l : L) ⦃σ₁ σ₂ : P⦄ ⦃z₁ z₂ : Z⦄, z₁ ∈ ℓ.stems l σ₁ → z₂ ∈ ℓ.stems l σ₂ → p z₁ = p z₂

def Morphology.Linkage.IsStemInvariant {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Stem invariance: one stem serves all of a lexeme's cells, so its correspondents come from a single form paradigm. Stem suppletion is the failure.

Equations

• ℓ.IsStemInvariant = ℓ.InvariantAlong id

def Morphology.Linkage.IsInjective {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Injectivity: no two content cells of a lexeme share a form correspondent. Syncretism is the failure.

Equations

• ℓ.IsInjective = ∀ (l : L) ⦃σ₁ σ₂ : P⦄, σ₁ ≠ σ₂ → Disjoint (ℓ.corr l σ₁) (ℓ.corr l σ₂)

def Morphology.Linkage.IsPropertyPreserving {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Property preservation: a form correspondent carries the content cell's own property set. Deponency, functor-argument reversal, and directional syncretism are failures.

Equations

• ℓ.IsPropertyPreserving = ∀ (l : L) (σ : P), ℓ.pm l σ = σ

structure Morphology.Linkage.IsCanonical {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Canonical paradigm linkage ([Stu12], axes per [Cor07]'s canonical-typology method): all five axes at once.

• total : ℓ.IsTotal
• univalent : ℓ.IsUnivalent
• stemInvariant : ℓ.IsStemInvariant
• injective : ℓ.IsInjective
• propertyPreserving : ℓ.IsPropertyPreserving

theorem Morphology.Linkage.InvariantAlong.comp {L : Type u_1} {Z : Type u_2} {P : Type u_3} {X : Type u_5} {Y : Type u_6} {ℓ : Linkage L Z P} {p : Z → X} (h : ℓ.InvariantAlong p) (q : X → Y) : ℓ.InvariantAlong (q ∘ p)

Constancy transfers along any further projection.

theorem Morphology.Linkage.IsStemInvariant.invariantAlong {L : Type u_1} {Z : Type u_2} {P : Type u_3} {X : Type u_5} {ℓ : Linkage L Z P} (h : ℓ.IsStemInvariant) (p : Z → X) : ℓ.InvariantAlong p

A stem-invariant linkage is invariant along every projection.

Deviations from canonical linkage

Each noncanonical phenomenon negates one axis.

def Morphology.Linkage.IsDefective {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Defectiveness: some content cell lacks a form correspondent ([Stu12] §3.1). Negates totality.

Equations

• ℓ.IsDefective = ∃ (l : L) (σ : P), ℓ.stems l σ = ∅

def Morphology.Linkage.IsOverabundant {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Overabundance: some content cell has two or more form correspondents — [Tho11]'s cell-mates, at the level of the correspondence. Negates univalence.

Equations

• ℓ.IsOverabundant = ∃ (l : L) (σ : P), 2 ≤ (ℓ.stems l σ).card

def Morphology.Linkage.IsSuppletive {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Suppletion: a lexeme's correspondents draw on more than one stem ([Stu12] §3.4). Negates stem invariance.

Equations

• ℓ.IsSuppletive = ¬ℓ.IsStemInvariant

def Morphology.Linkage.IsHeteroclite {L : Type u_1} {Z : Type u_2} {P : Type u_3} {K : Type u_7} (ℓ : Linkage L Z P) (cls : Z → K) : Prop

Heteroclisis: a lexeme's correspondents draw on form paradigms of two or more inflection classes ([stump-2006]), the classes given by a projection cls : Z → K. Negates invariance along cls.

Equations

• ℓ.IsHeteroclite cls = ¬ℓ.InvariantAlong cls

def Morphology.Linkage.IsSyncretic {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Syncretism: two distinct content cells share a form correspondent ([Stu12] §3.2). Negates injectivity.

Equations

• ℓ.IsSyncretic = ∃ (l : L) (σ₁ : P) (σ₂ : P), σ₁ ≠ σ₂ ∧ ¬Disjoint (ℓ.corr l σ₁) (ℓ.corr l σ₂)

def Morphology.Linkage.IsUnfaithful {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Prop

Unfaithfulness: some content cell's form correspondents carry a different property set — deponency and functor-argument reversal ([Stu12] §3.3). Negates property preservation.

Equations

• ℓ.IsUnfaithful = ∃ (l : L) (σ : P), ℓ.pm l σ ≠ σ

theorem Morphology.Linkage.isDefective_iff_not_isTotal {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : ℓ.IsDefective ↔ ¬ℓ.IsTotal

Defectiveness is exactly the failure of totality.

theorem Morphology.Linkage.isOverabundant_iff_not_isUnivalent {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : ℓ.IsOverabundant ↔ ¬ℓ.IsUnivalent

Overabundance is exactly the failure of univalence.

theorem Morphology.Linkage.isSyncretic_iff_not_isInjective {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : ℓ.IsSyncretic ↔ ¬ℓ.IsInjective

Syncretism is exactly the failure of injectivity.

theorem Morphology.Linkage.isUnfaithful_iff_not_isPropertyPreserving {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : ℓ.IsUnfaithful ↔ ¬ℓ.IsPropertyPreserving

Unfaithfulness is exactly the failure of property preservation.

theorem Morphology.Linkage.IsHeteroclite.isSuppletive {L : Type u_1} {Z : Type u_2} {P : Type u_3} {K : Type u_7} (ℓ : Linkage L Z P) {cls : Z → K} (h : ℓ.IsHeteroclite cls) : ℓ.IsSuppletive

Heteroclisis entails stem non-invariance: drawing on two inflection classes is drawing on two stems, [stump-2006]'s "a kind of stem alternation" — even when the stems are phonologically identical, as in Czech PRAMEN.

theorem Morphology.Linkage.IsCanonical.not_isDefective {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (h : ℓ.IsCanonical) : ¬ℓ.IsDefective

theorem Morphology.Linkage.IsCanonical.not_isOverabundant {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (h : ℓ.IsCanonical) : ¬ℓ.IsOverabundant

theorem Morphology.Linkage.IsCanonical.not_isSuppletive {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (h : ℓ.IsCanonical) : ¬ℓ.IsSuppletive

theorem Morphology.Linkage.IsCanonical.not_isHeteroclite {L : Type u_1} {Z : Type u_2} {P : Type u_3} {K : Type u_7} (ℓ : Linkage L Z P) (h : ℓ.IsCanonical) (cls : Z → K) : ¬ℓ.IsHeteroclite cls

theorem Morphology.Linkage.IsCanonical.not_isSyncretic {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (h : ℓ.IsCanonical) : ¬ℓ.IsSyncretic

theorem Morphology.Linkage.IsCanonical.not_isUnfaithful {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (h : ℓ.IsCanonical) : ¬ℓ.IsUnfaithful

def Morphology.Linkage.IsVirtual {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (zτ : Z × P) : Prop

A virtual cell: a form cell no content cell corresponds to ([Stu12] §4). Realization rules still define a value there, which language change can release by suppressing a linkage override.

Equations

• ℓ.IsVirtual zτ = ∀ (l : L) (σ : P), zτ ∉ ℓ.corr l σ

Decidability

Instances by inferInstanceAs on the definitional unfolding, so decide reduces in the kernel.

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsTotal {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] : Decidable ℓ.IsTotal

Equations

• ℓ.instDecidableIsTotal = Morphology.Linkage.instDecidableIsTotal._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsUnivalent {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] : Decidable ℓ.IsUnivalent

Equations

• ℓ.instDecidableIsUnivalent = Morphology.Linkage.instDecidableIsUnivalent._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableInvariantAlongOfDecidableEq {L : Type u_1} {Z : Type u_2} {P : Type u_3} {X : Type u_5} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [Fintype Z] [DecidableEq Z] {p : Z → X} [DecidableEq X] : Decidable (ℓ.InvariantAlong p)

Equations

• ℓ.instDecidableInvariantAlongOfDecidableEq = Morphology.Linkage.instDecidableInvariantAlongOfDecidableEq._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsStemInvariant {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [Fintype Z] [DecidableEq Z] : Decidable ℓ.IsStemInvariant

Equations

• ℓ.instDecidableIsStemInvariant = Morphology.Linkage.instDecidableIsStemInvariant._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsInjective {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [DecidableEq Z] [DecidableEq P] : Decidable ℓ.IsInjective

Equations

• ℓ.instDecidableIsInjective = Morphology.Linkage.instDecidableIsInjective._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsPropertyPreserving {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [DecidableEq P] : Decidable ℓ.IsPropertyPreserving

Equations

• ℓ.instDecidableIsPropertyPreserving = Morphology.Linkage.instDecidableIsPropertyPreserving._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsDefective {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [DecidableEq Z] : Decidable ℓ.IsDefective

Equations

• ℓ.instDecidableIsDefective = Morphology.Linkage.instDecidableIsDefective._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsOverabundant {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] : Decidable ℓ.IsOverabundant

Equations

• ℓ.instDecidableIsOverabundant = Morphology.Linkage.instDecidableIsOverabundant._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsSuppletive {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [Fintype Z] [DecidableEq Z] : Decidable ℓ.IsSuppletive

Equations

• ℓ.instDecidableIsSuppletive = Morphology.Linkage.instDecidableIsSuppletive._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsHeterocliteOfDecidableEq {L : Type u_1} {Z : Type u_2} {P : Type u_3} {K : Type u_7} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [Fintype Z] [DecidableEq Z] {cls : Z → K} [DecidableEq K] : Decidable (ℓ.IsHeteroclite cls)

Equations

• ℓ.instDecidableIsHeterocliteOfDecidableEq = Morphology.Linkage.instDecidableIsHeterocliteOfDecidableEq._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsSyncretic {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [DecidableEq Z] [DecidableEq P] : Decidable ℓ.IsSyncretic

Equations

• ℓ.instDecidableIsSyncretic = Morphology.Linkage.instDecidableIsSyncretic._aux_1 ℓ

@[implicit_reducible]

instance Morphology.Linkage.instDecidableIsUnfaithful {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) [Fintype L] [Fintype P] [DecidableEq P] : Decidable ℓ.IsUnfaithful

Equations

• ℓ.instDecidableIsUnfaithful = Morphology.Linkage.instDecidableIsUnfaithful._aux_1 ℓ

Realization

theorem Morphology.Linkage.realize_eq_of_corr_eq {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] (realizeForm : Z → P → W) {l : L} {σ₁ σ₂ : P} (h : ℓ.corr l σ₁ = ℓ.corr l σ₂) : ℓ.realize realizeForm l σ₁ = ℓ.realize realizeForm l σ₂

Equal correspondent sets force equal realizations ([Stu12] §3.2): the mechanism of syncretism.

theorem Morphology.Linkage.realize_eq_of_corr_eq_lexeme {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] (realizeForm : Z → P → W) {l₁ l₂ : L} {σ : P} (h : ℓ.corr l₁ σ = ℓ.corr l₂ σ) : ℓ.realize realizeForm l₁ σ = ℓ.realize realizeForm l₂ σ

Correspondent sets shared across two lexemes force shared realizations: the cross-lexeme companion of realize_eq_of_corr_eq. This is the mechanism behind [JA20]'s Same Verb solution — homophones with a shared morphosyntactic-form pivot inflect alike, however their distinct semantics.

theorem Morphology.Linkage.not_disjoint_realize_of_not_disjoint_corr {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] (realizeForm : Z → P → W) {l : L} {σ₁ σ₂ : P} (h : ¬Disjoint (ℓ.corr l σ₁) (ℓ.corr l σ₂)) : ¬Disjoint (ℓ.realize realizeForm l σ₁) (ℓ.realize realizeForm l σ₂)

A shared form correspondent already forces a shared realized form, even when the full correspondent sets differ: the multi-valued syncretism mechanism.

def Morphology.Linkage.HasCellMates {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] (realizeForm : Z → P → W) : Prop

Cell-mates ([Tho11]): some content cell realizes as two or more distinct word forms.

Equations

• ℓ.HasCellMates realizeForm = ∃ (l : L) (σ : P), 2 ≤ (ℓ.realize realizeForm l σ).card

theorem Morphology.Linkage.card_realize_le_card_stems {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] (realizeForm : Z → P → W) (l : L) (σ : P) : (ℓ.realize realizeForm l σ).card ≤ (ℓ.stems l σ).card

Realization cannot outnumber the stems that feed it.

theorem Morphology.Linkage.HasCellMates.isOverabundant {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} (ℓ : Linkage L Z P) [DecidableEq W] (realizeForm : Z → P → W) (h : ℓ.HasCellMates realizeForm) : ℓ.IsOverabundant

Cell-mates certify overabundance: distinct realized forms at one cell need distinct form correspondents there. The converse fails — distinct correspondents may realize alike.

The canonical linkage

def Morphology.Linkage.canonical {L : Type u_1} {Z : Type u_2} {P : Type u_3} (st : L → Z) : Linkage L Z P

The canonical one-stem linkage: a total, univalent, lexeme-blind stem selection with the identity property mapping — the graph of [stump-2006]'s universal default rule of paradigm linkage.

Equations

• Morphology.Linkage.canonical st = { stems := fun (l : L) (x : P) => {st l}, pm := fun (x : L) (σ : P) => σ }

@[simp]

theorem Morphology.Linkage.canonical_stems {L : Type u_1} {Z : Type u_2} {P : Type u_3} (st : L → Z) (l : L) (σ : P) : (canonical st).stems l σ = {st l}

@[simp]

theorem Morphology.Linkage.canonical_pm {L : Type u_1} {Z : Type u_2} {P : Type u_3} (st : L → Z) (l : L) (σ : P) : (canonical st).pm l σ = σ

@[simp]

theorem Morphology.Linkage.canonical_corr {L : Type u_1} {Z : Type u_2} {P : Type u_3} (st : L → Z) (l : L) (σ : P) : (canonical st).corr l σ = {(st l, σ)}

@[simp]

theorem Morphology.Linkage.canonical_realize {L : Type u_1} {Z : Type u_2} {P : Type u_3} {W : Type u_4} [DecidableEq W] (st : L → Z) (realizeForm : Z → P → W) (l : L) (σ : P) : (canonical st).realize realizeForm l σ = {(realizeForm (st l) σ, σ)}

theorem Morphology.Linkage.canonical_isCanonical {L : Type u_1} {Z : Type u_2} {P : Type u_3} (st : L → Z) : (canonical st).IsCanonical

The canonical linkage is canonical on all five axes.

The realization view

def Morphology.Linkage.toRealization {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : Realization L P Z

The stem selection as a realization: lexemes as indices, property sets as contexts, stems as forms. A lossless embedding — the linkage adds only the property mapping pm on top of it.

Equations

• ℓ.toRealization = { realize := ℓ.stems }

@[simp]

theorem Morphology.Linkage.toRealization_realize {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) (l : L) (σ : P) : ℓ.toRealization.realize l σ = ℓ.stems l σ

theorem Morphology.Linkage.toRealization_isUnivalent_iff {L : Type u_1} {Z : Type u_2} {P : Type u_3} (ℓ : Linkage L Z P) : ℓ.toRealization.IsUnivalent ↔ ℓ.IsUnivalent

The linkage and its realization agree on univalence.