Relational Morphology: the sister-schema engine and its divergences

[JA20]

[JA20]'s Relational Morphology explicates morphological motivation as shared structure recorded by nondirectional relational links, rather than by directed inheritance. This file instantiates the Morphology/Construction/ substrate as that engine and states its three divergences from rival accounts, each verified against the book.

The linked-variable coindices α (phonology) and β (semantics) of the [X-ism]/[X-ist] sister schemas are rendered as a shared coindex space; the English and German verb paradigms use the syncretism (Setoid.ker) and ablaut (SameExcept) substrate. The Same Verb flagship lifts Linkage.realize_eq_of_corr_eq_lexeme: two lexemes sharing a morphosyntactic-form correspondent inflect alike, evading the lexical-index accounts of [Spe13b]. The cycle flagship instantiates Hierarchy.parent_asymm: Objection 10's assassin/assassinate, whose form and meaning planes demand opposite parent orientations, cannot both be edges of one acyclic hierarchy, while a symmetric sister link carries both by construction.

Main results

• behaviorism_pairs, trumpism_pairs — the [X-ism]/[X-ist] sister schema and its open-endedness, as Sister.Pairs on linked coindices
• walk_syncretisms, spricht_morphome — English and German verb syncretisms / the morphomic 2/3-sg-present pattern via syncretismClass
• singSang_contrast, stringStrung_contrast, ablaut_generality — ablaut classes as SameExcept contrasts at the nucleus, under the general schema
• draw_same_verb, ring_wring_distinct — the Same Verb flagship and its homophony negative control
• assassin_cycle, assassin_sister_pairs — the cycle flagship: inheritance forces a 2-cycle where a sister link does not

inductive JackendoffAudring2020.Coindex : Type

The linked-variable coindices of [JA20]'s sister schemas: alpha the phonological link, beta the semantic link.

• alpha : Coindex
• beta : Coindex

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqCoindex : DecidableEq Coindex

Equations

• JackendoffAudring2020.instDecidableEqCoindex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeCoindex : Fintype Coindex

Equations

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

Sister schemas: [X-ism] and [X-ist]

[JA20] §4.8.2, formalizing the second-order schema [Boo10b] observed: a noun in -ism denoting an ideology is paired with a noun in -ist denoting an adherent, correlated on the shared phonological base (coindex α) and the shared ideology (coindex β). The relation is stated once between the schemas and holds of every attested pair, and is open-ended — a new ideology (Trumpism) has its adherents (Trumpists) without hesitation.

inductive JackendoffAudring2020.Sym : Type

Phonological bases and ideology values the -ism/-ist schemas range over.

• behavior : Sym
• commun : Sym
• trump : Sym
• behaviorismSem : Sym
• communismSem : Sym
• trumpismSem : Sym

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqSym : DecidableEq Sym

Equations

• JackendoffAudring2020.instDecidableEqSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeSym : Fintype Sym

Equations

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

inductive JackendoffAudring2020.IsmVar : Type

The two variables of the -ism schema: a phonological base and an ideology.

• base : IsmVar
• ideology : IsmVar

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqIsmVar : DecidableEq IsmVar

Equations

• JackendoffAudring2020.instDecidableEqIsmVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeIsmVar : Fintype IsmVar

Equations

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

inductive JackendoffAudring2020.IstVar : Type

The two variables of the -ist schema.

• base : IstVar
• ideology : IstVar

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqIstVar : DecidableEq IstVar

Equations

• JackendoffAudring2020.instDecidableEqIstVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeIstVar : Fintype IstVar

Equations

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

def JackendoffAudring2020.ismCoindex : IsmVar → Coindex

Equations

• JackendoffAudring2020.ismCoindex JackendoffAudring2020.IsmVar.base = JackendoffAudring2020.Coindex.alpha
• JackendoffAudring2020.ismCoindex JackendoffAudring2020.IsmVar.ideology = JackendoffAudring2020.Coindex.beta

def JackendoffAudring2020.istCoindex : IstVar → Coindex

Equations

• JackendoffAudring2020.istCoindex JackendoffAudring2020.IstVar.base = JackendoffAudring2020.Coindex.alpha
• JackendoffAudring2020.istCoindex JackendoffAudring2020.IstVar.ideology = JackendoffAudring2020.Coindex.beta

def JackendoffAudring2020.ismSchema : Morphology.Construction.Schema IsmVar (Flat Sym)

Equations

• JackendoffAudring2020.ismSchema = { body := fun (x : JackendoffAudring2020.IsmVar) => ⊥, opens := Set.univ }

def JackendoffAudring2020.istSchema : Morphology.Construction.Schema IstVar (Flat Sym)

Equations

• JackendoffAudring2020.istSchema = { body := fun (x : JackendoffAudring2020.IstVar) => ⊥, opens := Set.univ }

def JackendoffAudring2020.ismistSister : Morphology.Construction.Sister IsmVar IstVar (Flat Sym)

The [X-ism]/[X-ist] sister schema: variables sharing a coindex are linked.

Equations

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

def JackendoffAudring2020.behaviorismW : IsmVar → Flat Sym

Equations

• JackendoffAudring2020.behaviorismW JackendoffAudring2020.IsmVar.base = ↑JackendoffAudring2020.Sym.behavior
• JackendoffAudring2020.behaviorismW JackendoffAudring2020.IsmVar.ideology = ↑JackendoffAudring2020.Sym.behaviorismSem

def JackendoffAudring2020.behavioristW : IstVar → Flat Sym

Equations

• JackendoffAudring2020.behavioristW JackendoffAudring2020.IstVar.base = ↑JackendoffAudring2020.Sym.behavior
• JackendoffAudring2020.behavioristW JackendoffAudring2020.IstVar.ideology = ↑JackendoffAudring2020.Sym.behaviorismSem

def JackendoffAudring2020.trumpismW : IsmVar → Flat Sym

Equations

• JackendoffAudring2020.trumpismW JackendoffAudring2020.IsmVar.base = ↑JackendoffAudring2020.Sym.trump
• JackendoffAudring2020.trumpismW JackendoffAudring2020.IsmVar.ideology = ↑JackendoffAudring2020.Sym.trumpismSem

def JackendoffAudring2020.trumpistW : IstVar → Flat Sym

Equations

• JackendoffAudring2020.trumpistW JackendoffAudring2020.IstVar.base = ↑JackendoffAudring2020.Sym.trump
• JackendoffAudring2020.trumpistW JackendoffAudring2020.IstVar.ideology = ↑JackendoffAudring2020.Sym.trumpismSem

theorem JackendoffAudring2020.behaviorism_pairs : ismistSister.Pairs behaviorismW behavioristW

behaviorism/behaviorist is a paired instantiation of the sister schema: both share the base phonology (α) and the ideology (β) — the attested pair (44a).

theorem JackendoffAudring2020.trumpism_pairs : ismistSister.Pairs trumpismW trumpistW

The relation is open-ended: Trumpism/Trumpist pairs by the same schema with no listed precedent (§4.8.2).

English and German verb syncretisms

The English verb repertoire (16) is six cells. For walk, present equals infinitive (bare stem) and past equals past participle (-ed): these are syncretisms ([JA20]: "We would like the grammar to express these syncretisms"), coincidences in the realization map read off syncretismClass (Setoid.ker). The German present-tense 2/3-sg stem ablaut (spricht) is a morphome ([Aro94]): the cells it groups do not form a natural class.

inductive JackendoffAudring2020.VCell : Type

The six English finite/nonfinite verb cells (16).

• pres : VCell
• pres3sg : VCell
• past : VCell
• inf : VCell
• prespt : VCell
• ptcp : VCell

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqVCell : DecidableEq VCell

Equations

• JackendoffAudring2020.instDecidableEqVCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeVCell : Fintype VCell

Equations

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

inductive JackendoffAudring2020.VForm : Type

The phonological reflex of walk in each cell: bare stem, -s, -ed, -ing.

• bare : VForm
• s : VForm
• ed : VForm
• ing : VForm

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqVForm : DecidableEq VForm

Equations

• JackendoffAudring2020.instDecidableEqVForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JackendoffAudring2020.walkForm : VCell → VForm

walk's realization (19): present and infinitive are bare, past and past participle both -ed.

Equations

• JackendoffAudring2020.walkForm JackendoffAudring2020.VCell.pres = JackendoffAudring2020.VForm.bare
• JackendoffAudring2020.walkForm JackendoffAudring2020.VCell.inf = JackendoffAudring2020.VForm.bare
• JackendoffAudring2020.walkForm JackendoffAudring2020.VCell.pres3sg = JackendoffAudring2020.VForm.s
• JackendoffAudring2020.walkForm JackendoffAudring2020.VCell.past = JackendoffAudring2020.VForm.ed
• JackendoffAudring2020.walkForm JackendoffAudring2020.VCell.ptcp = JackendoffAudring2020.VForm.ed
• JackendoffAudring2020.walkForm JackendoffAudring2020.VCell.prespt = JackendoffAudring2020.VForm.ing

theorem JackendoffAudring2020.walk_syncretisms : VCell.inf ∈ Morphology.syncretismClass walkForm VCell.pres ∧ VCell.ptcp ∈ Morphology.syncretismClass walkForm VCell.past ∧ VCell.past ∉ Morphology.syncretismClass walkForm VCell.pres

walk's two syncretisms: present with infinitive, past with past participle; present and past are not syncretic.

inductive JackendoffAudring2020.GCell : Type

The six present-tense person/number cells of a German strong verb.

• s1 : GCell
• s2 : GCell
• s3 : GCell
• p1 : GCell
• p2 : GCell
• p3 : GCell

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqGCell : DecidableEq GCell

Equations

• JackendoffAudring2020.instDecidableEqGCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeGCell : Fintype GCell

Equations

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

inductive JackendoffAudring2020.GVowel : Type

The present-tense stem vowel of sprechen: the special ablauted /ɪ/ in 2/3-sg, the default /ɛ/ elsewhere (43), (45).

• eLax : GVowel
• iLax : GVowel

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqGVowel : DecidableEq GVowel

Equations

• JackendoffAudring2020.instDecidableEqGVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JackendoffAudring2020.sprechenStemVowel : GCell → GVowel

Equations

• JackendoffAudring2020.sprechenStemVowel JackendoffAudring2020.GCell.s2 = JackendoffAudring2020.GVowel.iLax
• JackendoffAudring2020.sprechenStemVowel JackendoffAudring2020.GCell.s3 = JackendoffAudring2020.GVowel.iLax
• JackendoffAudring2020.sprechenStemVowel x✝ = JackendoffAudring2020.GVowel.eLax

theorem JackendoffAudring2020.spricht_morphome : GCell.s3 ∈ Morphology.syncretismClass sprechenStemVowel GCell.s2 ∧ GCell.s1 ∉ Morphology.syncretismClass sprechenStemVowel GCell.s2

The morphomic 2/3-sg-present pattern: 2-sg and 3-sg share the special stem vowel, and 1-sg does not — the cells group as a class with no natural (feature-conjunction) characterization ([Aro94]).

Ablaut as same-except contrast

Table 5.1's ablaut classes are SameExcept contrasts at the syllabic nucleus: a stem and its past tense are phonologically identical except for the nucleus vowel. Over the vowel tier (only the nucleus bears a vowel), the sing/sang pattern (ten verbs) and the string/strung pattern (thirteen) are contrasts; the German singen/sang/gesungen three-sister (eighteen members) is a pair of nucleus contrasts. The general ablaut schema (25) leaves the nucleus an open variable, and the sing/sang subschema (26) instantiates it.

inductive JackendoffAudring2020.Vowel : Type

The nucleus vowels the ablaut classes use: sing /ɪ/, sang /æ/, sung/strung /ʌ/, German past /a/.

• iLax : Vowel
• ae : Vowel
• uh : Vowel
• ah : Vowel

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqVowel : DecidableEq Vowel

Equations

• JackendoffAudring2020.instDecidableEqVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeVowel : Fintype Vowel

Equations

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

inductive JackendoffAudring2020.Pos : Type

Syllable positions: only the nucleus carries a vowel on this tier.

• onset : Pos
• nucleus : Pos
• coda : Pos

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqPos : DecidableEq Pos

Equations

• JackendoffAudring2020.instDecidableEqPos x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypePos : Fintype Pos

Equations

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

def JackendoffAudring2020.melody (v : Vowel) : Pos → Flat Vowel

The vowel melody of a monosyllable: the vowel at the nucleus, ⊥ elsewhere.

Equations

• JackendoffAudring2020.melody v JackendoffAudring2020.Pos.nucleus = ↑v
• JackendoffAudring2020.melody v x✝ = ⊥

theorem JackendoffAudring2020.melody_contrast {v w : Vowel} (h : v ≠ w) : Morphology.Construction.Contrast (melody v) (melody w) {Pos.nucleus}

Two melodies differing only in their nucleus vowel are a nucleus contrast.

theorem JackendoffAudring2020.singSang_contrast : Morphology.Construction.Contrast (melody Vowel.iLax) (melody Vowel.ae) {Pos.nucleus}

sing/sang: identical except at the nucleus (/ɪ/ vs /æ/) — a contrast.

theorem JackendoffAudring2020.stringStrung_contrast : Morphology.Construction.Contrast (melody Vowel.iLax) (melody Vowel.uh) {Pos.nucleus}

string/strung: identical except at the nucleus (/ɪ/ vs /ʌ/).

theorem JackendoffAudring2020.singen_three_sister : Morphology.Construction.Contrast (melody Vowel.iLax) (melody Vowel.ah) {Pos.nucleus} ∧ Morphology.Construction.Contrast (melody Vowel.ah) (melody Vowel.uh) {Pos.nucleus}

German singen/sang/gesungen: the three sisters differ pairwise only at the nucleus (/ɪ/, /a/, the back-vowel /ʌ/).

def JackendoffAudring2020.ablautSchema : Morphology.Construction.Schema Pos (Flat Vowel)

The general ablaut schema (25): the nucleus is an open variable, all positions otherwise unconstrained.

Equations

• JackendoffAudring2020.ablautSchema = { body := fun (x : JackendoffAudring2020.Pos) => ⊥, opens := {JackendoffAudring2020.Pos.nucleus} }

theorem JackendoffAudring2020.ablaut_generality : ablautSchema.Instantiates (melody Vowel.iLax)

The sing/sang subschema (26) instantiates the general ablaut schema (25): the general schema's open nucleus is filled by /ɪ/.

The Same Verb flagship

[JA20] §5.6: many verbs share an irregular paradigm across distinct meanings — draw a picture and draw praise both have past drew — where lexical-index accounts ([Spe13b]) individuate every item. RM shares a single morphosyntactic-form correspondent (the pivot; phonology is derived through the shared morphosyntax↔phonology link), and one lift covers both the containment case (take/took part) and the sister case (the two draws differing only in semantics). J&A flag "three (perhaps minor) issues" with the index account (idioms, profligacy, mentalistic construal), not a knockdown objection. The negative control is homophony without shared paradigm: ring/wring/ringed are distinct verbs whose correspondents differ.

inductive JackendoffAudring2020.DrawLex : Type

The draw readings and the homophonous ring/wring.

• drawPicture : DrawLex
• drawElicit : DrawLex
• ring : DrawLex
• wring : DrawLex

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqDrawLex : DecidableEq DrawLex

Equations

• JackendoffAudring2020.instDecidableEqDrawLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeDrawLex : Fintype DrawLex

Equations

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

inductive JackendoffAudring2020.DrawStem : Type

The form correspondents: the two draws share one, ring and wring differ.

• drawZ : DrawStem
• ringZ : DrawStem
• wringZ : DrawStem

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqDrawStem : DecidableEq DrawStem

Equations

• JackendoffAudring2020.instDecidableEqDrawStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeDrawStem : Fintype DrawStem

Equations

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

inductive JackendoffAudring2020.Tense : Type

• pres : Tense
• past : Tense

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqTense : DecidableEq Tense

Equations

• JackendoffAudring2020.instDecidableEqTense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeTense : Fintype Tense

Equations

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

def JackendoffAudring2020.drawLinkage : Morphology.Linkage DrawLex DrawStem Tense

The paradigm linkage: both draw readings select the same stem, so they share every correspondent; ring and wring select distinct stems.

Equations

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

theorem JackendoffAudring2020.draw_same_verb {W : Type u_1} [DecidableEq W] (rf : DrawStem → Tense → W) (σ : Tense) : drawLinkage.realize rf DrawLex.drawPicture σ = drawLinkage.realize rf DrawLex.drawElicit σ

Same Verb: the two draw readings, sharing a form correspondent, realize identically at every cell — drew is forced, whatever their distinct semantics. Instantiates Linkage.realize_eq_of_corr_eq_lexeme.

theorem JackendoffAudring2020.ring_wring_distinct : drawLinkage.corr DrawLex.ring Tense.past ≠ drawLinkage.corr DrawLex.wring Tense.past

The negative control: ring and wring are homophonous but have distinct correspondents, so nothing forces a shared past — rang vs wrung.

The cycle flagship: inheritance vs relational linking

[JA20]'s Objection 10 (§3.4.4): in pairs like assassin/assassinate, the form plane builds the second on the first (assassinate from assassin), while the meaning plane builds the first on the second (an assassin is one who assassinates). "assassin is both 'above' and 'below' assassinate." Demanding a single directed inheritance relation realize both orientations forces a 2-cycle, refuted by Hierarchy.parent_asymm (the well-foundedness rendering is ours; the above-and-below paradox is J&A's). The symmetric sister link carries both plane-links by construction, nondirectionally — the divergence runs the other way from the default-override win of [Boo10b]'s werkbaar.

inductive JackendoffAudring2020.AsPair : Type

The mixed-direction pair.

• assassin : AsPair
• assassinate : AsPair

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqAsPair : DecidableEq AsPair

Equations

• JackendoffAudring2020.instDecidableEqAsPair x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeAsPair : Fintype AsPair

Equations

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

theorem JackendoffAudring2020.assassin_cycle (h : Morphology.Construction.Hierarchy AsPair) (hform : h.parent AsPair.assassinate = some AsPair.assassin) (hmean : h.parent AsPair.assassin = some AsPair.assassinate) : False

Cycle: no acyclic hierarchy realizes both orientation demands. The form plane demands assassinate's parent be assassin; the meaning plane demands assassin's parent be assassinate; together they are a 2-cycle.

inductive JackendoffAudring2020.AsVar : Type

The two variables of a lexical entry that a sister link relates: phonological base (α) and semantics (β).

• phon : AsVar
• sem : AsVar

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqAsVar : DecidableEq AsVar

Equations

• JackendoffAudring2020.instDecidableEqAsVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeAsVar : Fintype AsVar

Equations

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

def JackendoffAudring2020.asCoindex : AsVar → Coindex

Equations

• JackendoffAudring2020.asCoindex JackendoffAudring2020.AsVar.phon = JackendoffAudring2020.Coindex.alpha
• JackendoffAudring2020.asCoindex JackendoffAudring2020.AsVar.sem = JackendoffAudring2020.Coindex.beta

inductive JackendoffAudring2020.AsAtom : Type

The shared material of the assassin/assassinate entries (41).

• asasin : AsAtom
• murderSem : AsAtom

@[implicit_reducible]

instance JackendoffAudring2020.instDecidableEqAsAtom : DecidableEq AsAtom

Equations

• JackendoffAudring2020.instDecidableEqAsAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JackendoffAudring2020.instFintypeAsAtom : Fintype AsAtom

Equations

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

def JackendoffAudring2020.asSchema : Morphology.Construction.Schema AsVar (Flat AsAtom)

Equations

• JackendoffAudring2020.asSchema = { body := fun (x : JackendoffAudring2020.AsVar) => ⊥, opens := Set.univ }

def JackendoffAudring2020.assassinSister : Morphology.Construction.Sister AsVar AsVar (Flat AsAtom)

The symmetric sister link between assassin and assassinate: they share the phonological base (α) and part of the semantics (β), neither derived from the other.

Equations

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

def JackendoffAudring2020.assassinW : AsVar → Flat AsAtom

Equations

• JackendoffAudring2020.assassinW JackendoffAudring2020.AsVar.phon = ↑JackendoffAudring2020.AsAtom.asasin
• JackendoffAudring2020.assassinW JackendoffAudring2020.AsVar.sem = ↑JackendoffAudring2020.AsAtom.murderSem

def JackendoffAudring2020.assassinateW : AsVar → Flat AsAtom

Equations

• JackendoffAudring2020.assassinateW JackendoffAudring2020.AsVar.phon = ↑JackendoffAudring2020.AsAtom.asasin
• JackendoffAudring2020.assassinateW JackendoffAudring2020.AsVar.sem = ↑JackendoffAudring2020.AsAtom.murderSem

theorem JackendoffAudring2020.assassin_sister_pairs : assassinSister.Pairs assassinW assassinateW

The sister link satisfies both plane-demands at once — the shared base and shared semantics — where the directed hierarchy could not.

theorem JackendoffAudring2020.assassin_sister_symm : assassinSister.swap.Pairs assassinateW assassinW

Nondirectionality: the sister relation reads the same transposed, so neither member is "the base".

Storage versus computation, and scope (prose)

Storage vs computation. [JA20] treat a paradigm as stored schemas that operate nondirectionally, so no form is uniformly "derived" — a lexical-strength gradient plays the role a rule/computation weight plays in probabilistic grammars ([OD15]). No Lean content follows without a concrete measure, so this stays prose.

Scope. The rival-framings above are [JA20]'s own claims, stated as theirs: that inheritance cannot state horizontal links is contested in the DATR literature. Word.Tree's ordered constructors and RM's order-free morphosyntax (§4.7) are latent rivals — a documented stance difference, changing nothing. RM independently vindicates the no-zero-morphs analysis (§4.3 double-coindexation): the past tense and infinitive of walk add no phonological content, coindexed to the base rather than to a zero affix — a convergence noted here, not in Morph.lean.