Clause Chaining

@cite{sarvasy-aikhenvald-2025} @cite{foley-r-d-van-valin-1984}

Part I: Fragment Verification

Theorems connecting the clause chaining fragment data (medial verb inventories) to the typological parameters in Data.lean. Each theorem verifies that the fragment's morphological inventory is consistent with the language's clause chaining parameter bundle.

Dimensions

1. SR inventory ↔ SR system: languages with SR morphology have SS and DS markers in their fragment; languages without SR have no SR-indexed markers
2. Relation inventory ↔ relations marked: the number of distinct semantic relations in the fragment matches the parameter bundle's list
3. Agreement pattern ↔ medial morphology: DS-triggered agreement is consistent with the medial morph profile
4. Converb count ↔ relation richness: non-SR languages have more converbal suffixes, consistent with the generalization that SR absorbs semantic work

Part II: ContextTower Derivation

End-to-end derivation chain connecting the ContextTower infrastructure to clause chaining phenomena. The core insight: in a medial-final chain, the final verb establishes the root context and each medial clause pushes a .clauseChain shift. TAM values absent on medial verbs are inherited from the origin (the final verb's context).

Results

1. Tower depth = chain length: N medial clauses → tower depth N
2. TAM scope = origin access: the final verb's tense/mood at .origin scopes over medial clauses that lack their own tense/mood
3. Tense inheritance: languages with tenseFromFinalVerb = true (Nungon) read tense from origin; languages with medial tense (Turkish) read locally
4. SR as agent comparison: SS = .agent same across adjacent tower levels; DS = .agent differs

def Phenomena.ClauseChaining.nungon : Typology.ClauseChaining.ClauseChainingParams

Nungon (Trans-New Guinea, Finisterre-Huon; @cite{sarvasy-2017}, 2025 Ch. 7).

The best-described clause chaining language. Obligatory SR with temporal encoding: four distinct medial forms (SS-SEQ, SS-SIM, DS-SEQ, DS-SIM). Medial verbs are maximally reduced (bare stem + SR suffix). The final verb alone carries tense, agreement, and full mood. Non-canonical stand-alone medial clauses are attested.

Equations

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

def Phenomena.ClauseChaining.manambu : Typology.ClauseChaining.ClauseChainingParams

Manambu (Ndu family, East Sepik; @cite{aikhenvald-2008}, 2025 Ch. 6).

Equations

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

def Phenomena.ClauseChaining.kuWaru : Typology.ClauseChaining.ClauseChainingParams

Ku Waru (Trans-New Guinea, Chimbu-Wahgi; @cite{merlan-rumsey-1991}).

Equations

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

def Phenomena.ClauseChaining.korean : Typology.ClauseChaining.ClauseChainingParams

Korean (Koreanic; @cite{sohn-1999}).

Equations

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

def Phenomena.ClauseChaining.turkish : Typology.ClauseChaining.ClauseChainingParams

Turkish (Turkic; @cite{goksel-kerslake-2005}).

Equations

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

def Phenomena.ClauseChaining.korowai : Typology.ClauseChaining.ClauseChainingParams

Korowai (Trans-New Guinea, Greater Awyu; @cite{de-vries-2025} Ch. 5).

Equations

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

def Phenomena.ClauseChaining.allLanguages : List Typology.ClauseChaining.ClauseChainingParams

All language data entries.

Equations

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

theorem Phenomena.ClauseChaining.nungon_has_sr : nungon.hasSR = true

theorem Phenomena.ClauseChaining.manambu_has_sr : manambu.hasSR = true

theorem Phenomena.ClauseChaining.kuWaru_has_sr : kuWaru.hasSR = true

theorem Phenomena.ClauseChaining.korean_no_sr : korean.hasSR = false

theorem Phenomena.ClauseChaining.turkish_no_sr : turkish.hasSR = false

theorem Phenomena.ClauseChaining.korowai_has_sr : korowai.hasSR = true

theorem Phenomena.ClauseChaining.nungon_tense_from_final : nungon.tenseFromFinalVerb = true

theorem Phenomena.ClauseChaining.manambu_tense_not_from_final : manambu.tenseFromFinalVerb = false

theorem Phenomena.ClauseChaining.korean_tense_not_from_final : korean.tenseFromFinalVerb = false

theorem Phenomena.ClauseChaining.nungon_has_bridging : nungon.hasBridging = true

theorem Phenomena.ClauseChaining.korean_no_bridging : korean.hasBridging = false

theorem Phenomena.ClauseChaining.kuWaru_has_bridging : kuWaru.hasBridging = true

theorem Phenomena.ClauseChaining.nungon_temporal_via_sr : nungon.temporalViaSR = true

theorem Phenomena.ClauseChaining.manambu_not_temporal_via_sr : manambu.temporalViaSR = false

theorem Phenomena.ClauseChaining.nungon_medial_is_converb : nungon.medialVerbForm = UD.VerbForm.Conv

theorem Phenomena.ClauseChaining.korean_medial_is_converb : korean.medialVerbForm = UD.VerbForm.Conv

theorem Phenomena.ClauseChaining.turkish_medial_is_converb : turkish.medialVerbForm = UD.VerbForm.Conv

theorem Phenomena.ClauseChaining.all_medial_final : (allLanguages.all fun (x : Typology.ClauseChaining.ClauseChainingParams) => x.direction == Typology.ClauseChaining.ChainDirection.medialFinal) = true

All sampled languages are medial-final.

theorem Phenomena.ClauseChaining.sr_languages_have_target : (allLanguages.all fun (p : Typology.ClauseChaining.ClauseChainingParams) => !p.hasSR || p.srTarget.isSome) = true

Every language with SR tracks at least subject continuity.

theorem Phenomena.ClauseChaining.sr_languages_ss_unmarked : (allLanguages.all fun (p : Typology.ClauseChaining.ClauseChainingParams) => !p.hasSR || p.srMarkedness == some Typology.ClauseChaining.SRMarkedness.ssUnmarked) = true

In every SR language in the sample, SS is the unmarked member.

theorem Phenomena.ClauseChaining.noSR_richer_relations : (allLanguages.all fun (p : Typology.ClauseChaining.ClauseChainingParams) => p.hasSR || decide (p.relationsMarked.length ≥ 7)) = true

Languages without SR mark more interclausal semantic relations (7+ relation types). SR languages encode fewer relation types because the SR morpheme absorbs sequential/simultaneous distinctions.

theorem SarvasyAikhenvald2025.nungon_sr_system_matches : Phenomena.ClauseChaining.nungon.srSystem = Typology.ClauseChaining.SRSystem.ssDsTemporal

Nungon has the ssDsTemporal SR system: the fragment provides both SS suffixes (invariant, 2 forms for SEQ/SIM) and a full DS person/number paradigm. The four-way system (SS-SEQ, SS-SIM, DS-SEQ, DS-SIM) matches SRSystem.ssDsTemporal.

theorem SarvasyAikhenvald2025.nungon_ds_paradigm_complete : Fragments.Nungon.MedialVerbs.dsParadigm.length = 9

Nungon DS paradigm has 9 cells (3 persons x 3 numbers). DS forms carry person/number agreement — consistent with the agreement field being .absent on medial verbs in general (SS forms lack agreement; DS forms are the exception that proves the rule).

theorem SarvasyAikhenvald2025.nungon_ss_matches_relations : Fragments.Nungon.MedialVerbs.ssSuffixes.length = Phenomena.ClauseChaining.nungon.relationsMarked.length

Nungon SS suffixes are exactly 2: sequential and simultaneous. This matches the relationsMarked = [.sequential,.simultaneous] in the parameter bundle — the two temporal relations are the only semantics encoded on SS medial verbs.

theorem SarvasyAikhenvald2025.nungon_dual_syncretism : Fragments.Nungon.MedialVerbs.ds2du.form = Fragments.Nungon.MedialVerbs.ds3du.form

Nungon has dual number syncretism: 2du = 3du.

theorem SarvasyAikhenvald2025.nungon_plural_syncretism : Fragments.Nungon.MedialVerbs.ds2pl.form = Fragments.Nungon.MedialVerbs.ds3pl.form

Nungon has plural number syncretism: 2pl = 3pl.

theorem SarvasyAikhenvald2025.nungon_tense_scope : Phenomena.ClauseChaining.nungon.tenseFromFinalVerb = true

Nungon tense is absent on medial verbs — inherited from the final verb.

theorem SarvasyAikhenvald2025.nungon_medial_converb : Phenomena.ClauseChaining.nungon.medialVerbForm = UD.VerbForm.Conv

Nungon medial verbs are UD converbs.

theorem SarvasyAikhenvald2025.manambu_sr_system_matches : Phenomena.ClauseChaining.manambu.srSystem = Typology.ClauseChaining.SRSystem.ssDs

Manambu has a binary SS/DS system (without temporal encoding). The fragment inventory partitions into SS, DS, and neutral markers.

theorem SarvasyAikhenvald2025.manambu_inventory_size : Fragments.Manambu.MedialVerbs.allMarkers.length = 9

Manambu has 9 medial clause markers in total.

theorem SarvasyAikhenvald2025.manambu_sr_partition : Fragments.Manambu.MedialVerbs.ssMarkers.length + Fragments.Manambu.MedialVerbs.dsMarkers.length + Fragments.Manambu.MedialVerbs.neutralMarkers.length = Fragments.Manambu.MedialVerbs.allMarkers.length

Manambu's 9 markers partition into 5 SS + 2 DS + 2 neutral.

theorem SarvasyAikhenvald2025.manambu_agreement_on_ds_only : (Fragments.Manambu.MedialVerbs.dsMarkers.all fun (x : Fragments.Manambu.MedialVerbs.MarkerEntry) => x.hasSubjectMarking) = true ∧ (Fragments.Manambu.MedialVerbs.ssMarkers.all fun (x : Fragments.Manambu.MedialVerbs.MarkerEntry) => !x.hasSubjectMarking) = true

Every Manambu DS marker triggers subject agreement; no SS marker does. This mirrors the Nungon pattern: agreement is a property of DS marking, not of medial verbs in general.

theorem SarvasyAikhenvald2025.manambu_relation_count : Phenomena.ClauseChaining.manambu.relationsMarked.length = 3

Manambu marks 3 interclausal relations (sequential, simultaneous, causal), matching the parameter bundle.

theorem SarvasyAikhenvald2025.manambu_both_bridging : Phenomena.ClauseChaining.manambu.hasBridging = true

Manambu has both bridging types (recapitulative and summary).

theorem SarvasyAikhenvald2025.korean_no_sr : Phenomena.ClauseChaining.korean.srSystem = Typology.ClauseChaining.SRSystem.none

Korean has no SR system: conjunctive suffixes encode semantic relations directly without tracking subject continuity.

theorem SarvasyAikhenvald2025.korean_suffix_inventory : Fragments.Korean.MedialVerbs.allSuffixes.length = 8

Korean has 8 conjunctive suffixes.

theorem SarvasyAikhenvald2025.korean_suffix_relation_match : Fragments.Korean.MedialVerbs.allSuffixes.length = Phenomena.ClauseChaining.korean.relationsMarked.length

Korean marks 8 interclausal relations in its parameter bundle. The suffix count matches the relation count: each suffix maps to (at least) one relation type.

theorem SarvasyAikhenvald2025.korean_full_negation : Phenomena.ClauseChaining.korean.medialMorph.polarity = Typology.ClauseChaining.CategoryRetention.full

Korean allows full independent negation on medial clauses — consistent with all 8 suffixes allowing negation.

theorem SarvasyAikhenvald2025.korean_partial_tense : Phenomena.ClauseChaining.korean.medialMorph.tense = Typology.ClauseChaining.CategoryRetention.restricted ∧ Fragments.Korean.MedialVerbs.tensedSuffixes.length = 3

Korean medial verbs partially retain tense. The fragment confirms this: 3 of 8 suffixes allow tense marking on the medial verb.

theorem SarvasyAikhenvald2025.turkish_no_sr : Phenomena.ClauseChaining.turkish.srSystem = Typology.ClauseChaining.SRSystem.none

Turkish has no SR system.

theorem SarvasyAikhenvald2025.turkish_converb_inventory : Fragments.Turkish.MedialVerbs.allConverbs.length = 8

Turkish has 8 converbal suffixes (-(y)ip, -(y)erek, -(y)ince, -ken, -dikce, -meden, -AlI, -casina).

theorem SarvasyAikhenvald2025.turkish_converb_covers_relations : Fragments.Turkish.MedialVerbs.allConverbs.length ≥ Phenomena.ClauseChaining.turkish.relationsMarked.length

Turkish converbs outnumber relations: multiple converbs can encode the same semantic relation (e.g., both -erek and -çasına encode manner; both -erek and -ken encode simultaneous).

theorem SarvasyAikhenvald2025.turkish_full_negation : Phenomena.ClauseChaining.turkish.medialMorph.polarity = Typology.ClauseChaining.CategoryRetention.full

Turkish allows full independent negation on medial clauses — every affirmative converb has a negative counterpart, plus there is one inherently negative converb (-meden).

theorem SarvasyAikhenvald2025.turkish_polarity_complete : Fragments.Turkish.MedialVerbs.affirmativeConverbs.length + Fragments.Turkish.MedialVerbs.negativeConverbs.length = Fragments.Turkish.MedialVerbs.allConverbs.length

7 affirmative + 1 inherently negative = 8 total.

theorem SarvasyAikhenvald2025.noSR_more_dedicated_markers : Fragments.Korean.MedialVerbs.allSuffixes.length > Fragments.Nungon.MedialVerbs.ssSuffixes.length ∧ Fragments.Turkish.MedialVerbs.allConverbs.length > Fragments.Nungon.MedialVerbs.ssSuffixes.length

Non-SR languages have richer converbal inventories than SR languages' non-SR-encoded relations. Korean (8 suffixes for 8 relations) and Turkish (8 converbs for 7 relations) each have more dedicated markers than Nungon (2 SS forms for 2 relations) or Manambu (9 markers, but only 3 dedicated relations — the rest are SR-conditioned).

theorem SarvasyAikhenvald2025.ds_agreement_universal : (Fragments.Manambu.MedialVerbs.dsMarkers.all fun (x : Fragments.Manambu.MedialVerbs.MarkerEntry) => x.hasSubjectMarking) = true ∧ (Fragments.Manambu.MedialVerbs.ssMarkers.all fun (x : Fragments.Manambu.MedialVerbs.MarkerEntry) => !x.hasSubjectMarking) = true

Agreement asymmetry is cross-linguistically stable: in both Nungon and Manambu, subject agreement appears only on DS medial verbs, never on SS. This structural fact — that SS doesn't need to identify its subject because it's shared with the following clause — is the functional motivation for the SS/DS asymmetry.

inductive SarvasyAikhenvald2025.ChainAgent : Type

A minimal clause chain context: world (event structure), agent (subject), position (clause index), and time (event time).

• subjectA : ChainAgent
• subjectB : ChainAgent
• subjectC : ChainAgent

@[implicit_reducible]

instance SarvasyAikhenvald2025.instDecidableEqChainAgent : DecidableEq ChainAgent

Equations

• SarvasyAikhenvald2025.instDecidableEqChainAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SarvasyAikhenvald2025.instReprChainAgent.repr : ChainAgent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance SarvasyAikhenvald2025.instReprChainAgent : Repr ChainAgent

Equations

• SarvasyAikhenvald2025.instReprChainAgent = { reprPrec := SarvasyAikhenvald2025.instReprChainAgent.repr }

@[reducible, inline]

abbrev SarvasyAikhenvald2025.ChainCtx : Type

Equations

• SarvasyAikhenvald2025.ChainCtx = Core.Context.KContext Unit SarvasyAikhenvald2025.ChainAgent Unit ℤ

def SarvasyAikhenvald2025.finalCtx : ChainCtx

The final verb's context: subject A speaking at time 0. This is the "root" of the chain — the final verb's TAM values.

Equations

• SarvasyAikhenvald2025.finalCtx = { agent := SarvasyAikhenvald2025.ChainAgent.subjectA, addressee := SarvasyAikhenvald2025.ChainAgent.subjectA, world := (), time := 0, position := () }

def SarvasyAikhenvald2025.chainShift (newAgent : ChainAgent) (eventTime : ℤ) : Core.Context.ContextShift ChainCtx

A clauseChain shift: changes agent and time for a medial clause. The medial clause has its own subject and event time.

Equations

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

def SarvasyAikhenvald2025.finalOnly : Core.Context.ContextTower ChainCtx

Root tower: just the final verb, no medial clauses.

Equations

• SarvasyAikhenvald2025.finalOnly = Core.Context.ContextTower.root SarvasyAikhenvald2025.finalCtx

def SarvasyAikhenvald2025.chain1 : Core.Context.ContextTower ChainCtx

A 1-medial chain: one medial clause (subject B, time -3) + final.

Equations

• SarvasyAikhenvald2025.chain1 = SarvasyAikhenvald2025.finalOnly.push (SarvasyAikhenvald2025.chainShift SarvasyAikhenvald2025.ChainAgent.subjectB (-3))

def SarvasyAikhenvald2025.chain2 : Core.Context.ContextTower ChainCtx

A 2-medial chain: two medial clauses + final.

Equations

• SarvasyAikhenvald2025.chain2 = SarvasyAikhenvald2025.chain1.push (SarvasyAikhenvald2025.chainShift SarvasyAikhenvald2025.ChainAgent.subjectC (-5))

theorem SarvasyAikhenvald2025.finalOnly_depth : finalOnly.depth = 0

Final-only chain has depth 0.

theorem SarvasyAikhenvald2025.chain1_depth : chain1.depth = 1

1-medial chain has depth 1.

theorem SarvasyAikhenvald2025.chain2_depth : chain2.depth = 2

2-medial chain has depth 2.

theorem SarvasyAikhenvald2025.final_tense_at_origin_1 : chain1.origin.time = 0

The final verb's tense is always accessible at the origin, regardless of how many medial clauses are pushed. This is why the final verb's TAM "scopes over" the chain.

theorem SarvasyAikhenvald2025.final_tense_at_origin_2 : chain2.origin.time = 0

theorem SarvasyAikhenvald2025.medial_has_own_time_1 : chain1.innermost.time = -3

The innermost medial clause has its own event time.

theorem SarvasyAikhenvald2025.medial_has_own_time_2 : chain2.innermost.time = -5

def SarvasyAikhenvald2025.originTenseAccess : Core.Context.AccessPattern ChainCtx ℤ

Origin access pattern: reads tense from the final verb. This models languages like Nungon where medial verbs lack tense entirely (tenseFromFinalVerb = true). The medial verb inherits tense from the final verb's context.

Equations

• SarvasyAikhenvald2025.originTenseAccess = { depth := Core.Context.DepthSpec.origin, project := Core.Context.KContext.time }

def SarvasyAikhenvald2025.localTenseAccess : Core.Context.AccessPattern ChainCtx ℤ

Local access pattern: reads tense from the medial verb's own context. This models languages like Turkish where medial verbs retain some tense distinctions.

Equations

• SarvasyAikhenvald2025.localTenseAccess = { depth := Core.Context.DepthSpec.local, project := Core.Context.KContext.time }

theorem SarvasyAikhenvald2025.nungon_style_reads_final_tense : originTenseAccess.resolve chain1 = 0

In a Nungon-style chain (tenseFromFinalVerb = true), medial verb reads final verb's tense (0) via origin access.

theorem SarvasyAikhenvald2025.turkish_style_reads_local_tense : localTenseAccess.resolve chain1 = -3

In a Turkish-style chain, medial verb reads its own event time (-3) via local access.

theorem SarvasyAikhenvald2025.tense_scope_stable : originTenseAccess.resolve chain1 = originTenseAccess.resolve chain2

Origin tense access is stable: adding more medial clauses doesn't change the final verb's tense. This is the scope property: the final verb's TAM values are invariant under chain extension.

theorem SarvasyAikhenvald2025.nungon_tense_absent_means_origin : Phenomena.ClauseChaining.nungon.tenseFromFinalVerb = true

Nungon's tenseFromFinalVerb = true is consistent with origin access: the medial verb's tense dimension is absent, so it reads from origin.

theorem SarvasyAikhenvald2025.turkish_tense_retained_means_local : Phenomena.ClauseChaining.turkish.tenseFromFinalVerb = false

Turkish's tenseFromFinalVerb = false is consistent with local access: the medial verb has restricted tense, so it reads locally.

theorem SarvasyAikhenvald2025.korean_tense_retained_means_local : Phenomena.ClauseChaining.korean.tenseFromFinalVerb = false

Korean's tenseFromFinalVerb = false matches local access.

theorem SarvasyAikhenvald2025.kuWaru_tense_absent_means_origin : Phenomena.ClauseChaining.kuWaru.tenseFromFinalVerb = true

Ku Waru's tenseFromFinalVerb = true matches origin access (like Nungon).

def SarvasyAikhenvald2025.sameSubjectChain : Core.Context.ContextTower ChainCtx

Same-subject (SS): adjacent medial clause has the same agent.

Equations

• SarvasyAikhenvald2025.sameSubjectChain = SarvasyAikhenvald2025.finalOnly.push (SarvasyAikhenvald2025.chainShift SarvasyAikhenvald2025.ChainAgent.subjectA (-3))

def SarvasyAikhenvald2025.diffSubjectChain : Core.Context.ContextTower ChainCtx

Different-subject (DS): adjacent medial clause has a different agent.

Equations

• SarvasyAikhenvald2025.diffSubjectChain = SarvasyAikhenvald2025.finalOnly.push (SarvasyAikhenvald2025.chainShift SarvasyAikhenvald2025.ChainAgent.subjectB (-3))

theorem SarvasyAikhenvald2025.ss_agent_match : sameSubjectChain.innermost.agent = sameSubjectChain.origin.agent

SS: the medial clause's agent equals the final verb's agent.

theorem SarvasyAikhenvald2025.ds_agent_mismatch : diffSubjectChain.innermost.agent ≠ diffSubjectChain.origin.agent

DS: the medial clause's agent differs from the final verb's agent.

theorem SarvasyAikhenvald2025.sr_languages_use_tower_agent_tracking : ([Phenomena.ClauseChaining.nungon, Phenomena.ClauseChaining.manambu, Phenomena.ClauseChaining.kuWaru, Phenomena.ClauseChaining.korowai].all fun (x : Typology.ClauseChaining.ClauseChainingParams) => x.hasSR) = true

SR-bearing languages in the sample all have SR systems.

theorem SarvasyAikhenvald2025.nonsr_languages_no_agent_tracking : ([Phenomena.ClauseChaining.korean, Phenomena.ClauseChaining.turkish].all fun (p : Typology.ClauseChaining.ClauseChainingParams) => !p.hasSR) = true

Non-SR languages don't track agent continuity morphologically.

theorem SarvasyAikhenvald2025.chain_shift_label : (chainShift ChainAgent.subjectB (-3)).label = Core.Context.ShiftLabel.clauseChain

The chain shift carries the .clauseChain label, connecting it to the ShiftLabel taxonomy in Tower.lean.

theorem SarvasyAikhenvald2025.chain_is_not_attitude : (chainShift ChainAgent.subjectB (-3)).label ≠ Core.Context.ShiftLabel.attitude

Chain shifts are distinct from attitude shifts (subordination). This reflects the cosubordination ≠ subordination distinction: clause chaining uses a different shift label than attitude embedding.