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

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.nungon_sr_system_matches : Data.nungon.srSystem = Typology.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 Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.nungon_ss_matches_relations : Fragments.Nungon.MedialVerbs.ssSuffixes.length = Data.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.nungon_dual_syncretism : Fragments.Nungon.MedialVerbs.ds2du.form = Fragments.Nungon.MedialVerbs.ds3du.form

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

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

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

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

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

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

Nungon medial verbs are UD converbs.

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

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

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

Manambu has 9 medial clause markers in total.

theorem Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.manambu_relation_count : Data.manambu.relationsMarked.length = 3

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

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

Manambu has both bridging types (recapitulative and summary).

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

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

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

Korean has 8 conjunctive suffixes.

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.korean_suffix_relation_match : Fragments.Korean.MedialVerbs.allSuffixes.length = Data.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.korean_full_negation : Data.korean.medialMorph.polarity = Typology.CategoryRetention.full

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

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.korean_partial_tense : Data.korean.medialMorph.tense = Typology.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.turkish_no_sr : Data.turkish.srSystem = Typology.SRSystem.none

Turkish has no SR system.

theorem Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.turkish_converb_covers_relations : Fragments.Turkish.MedialVerbs.allConverbs.length ≥ Data.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.turkish_full_negation : Data.turkish.medialMorph.polarity = Typology.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 Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.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

instance Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instDecidableEqChainAgent : DecidableEq ChainAgent

Equations

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

def Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instReprChainAgent.repr : ChainAgent → ℕ → Std.Format

Equations

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

instance Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instReprChainAgent : Repr ChainAgent

Equations

• Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instReprChainAgent = { reprPrec := Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instReprChainAgent.repr }

instance Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instBEqChainAgent : BEq ChainAgent

Equations

• Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instBEqChainAgent = { beq := Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instBEqChainAgent.beq }

def Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instBEqChainAgent.beq : ChainAgent → ChainAgent → Bool

Equations

• Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.instBEqChainAgent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[reducible, inline]

abbrev Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.ChainCtx : Type

Equations

• Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.ChainCtx = Core.Context.KContext Unit Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.ChainAgent Unit ℤ

def Phenomena.ClauseChaining.Studies.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

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

def Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.finalOnly : Core.Context.ContextTower ChainCtx

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

Equations

• Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.finalOnly = Core.Context.ContextTower.root Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.finalCtx

def Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.chain1 : Core.Context.ContextTower ChainCtx

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

Equations

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

def Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.chain2 : Core.Context.ContextTower ChainCtx

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

Equations

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

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.finalOnly_depth : finalOnly.depth = 0

Final-only chain has depth 0.

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.chain1_depth : chain1.depth = 1

1-medial chain has depth 1.

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.chain2_depth : chain2.depth = 2

2-medial chain has depth 2.

theorem Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.final_tense_at_origin_2 : chain2.origin.time = 0

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.medial_has_own_time_1 : chain1.innermost.time = -3

The innermost medial clause has its own event time.

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.medial_has_own_time_2 : chain2.innermost.time = -5

def Phenomena.ClauseChaining.Studies.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

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

def Phenomena.ClauseChaining.Studies.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

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

theorem Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.nungon_tense_absent_means_origin : Data.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 Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.turkish_tense_retained_means_local : Data.turkish.tenseFromFinalVerb = false

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

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

Korean's tenseFromFinalVerb = false matches local access.

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

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

def Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.sameSubjectChain : Core.Context.ContextTower ChainCtx

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

Equations

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

def Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.diffSubjectChain : Core.Context.ContextTower ChainCtx

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

Equations

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

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.ss_agent_match : sameSubjectChain.innermost.agent = sameSubjectChain.origin.agent

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

theorem Phenomena.ClauseChaining.Studies.SarvasyAikhenvald2025.ds_agent_mismatch : diffSubjectChain.innermost.agent ≠ diffSubjectChain.origin.agent

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

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

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

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

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

theorem Phenomena.ClauseChaining.Studies.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 Phenomena.ClauseChaining.Studies.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.