Sakha Two-Modality Case Assignment @cite{baker-vinokurova-2010}

@cite{baker-vinokurova-2010} argue that Sakha (Turkic) requires both of the case-assignment mechanisms that linguistic theory has on offer: configurational dependent case (Marantz; @cite{marantz-1991}) for ACC and DAT, and Agree with a functional head (Chomsky; @cite{chomsky-2000}) for NOM and GEN. The two modalities are not in competition — they coexist in a single grammar:

• DAT rule (paper (4a)/(85)): if NP1 c-commands NP2 in the same VP-phase and NP2 is unmarked, value NP1 as DAT.
• ACC rule (paper (4b)/(85)): if NP1 c-commands NP2 in any phase and NP1 is unmarked, value NP2 as ACC. (4a) bleeds (4b) on the VP cycle by Elsewhere ordering.
• NOM rule (paper (5)/(86)): finite T Agrees with the highest unvalued NP visible on the CP cycle and values it NOM.
• GEN rule (paper (5)/(86)): D Agrees with the possessor inside DP and values it GEN. (DP-internal; not modeled by the clausal algorithm here, but parameterized via genMode := .agreeD.)

The library's CaseSystemConfig (in DependentCase.lean) is parameterized so each of the four structural cases gets an independent mechanism slot. Sakha is the configuration where ACC and DAT are dependent while NOM and GEN are Agree-based — exactly the @cite{baker-vinokurova-2010} grammar.

Phase visibility and DOM

NPs carry both a basePhase (where they were merged) and a shifted flag (did they move to a higher phase before evaluation). This captures the Phase Impenetrability Condition: an unshifted NP inside VP is invisible on the CP cycle, so it cannot be a competitor for the ACC rule on that cycle.

Differential Object Marking falls out: specific objects shift to the edge of VP (or beyond) and become visible on the CP cycle, where they form a competitor pair with the subject and receive ACC. Nonspecific objects stay inside VP, are invisible to T, and surface unmarked.

This file states the central derivations for monotransitives, ditransitives, unaccusatives, and DOM. ECM and DP-level GEN are acknowledged but not formalized; the clausal algorithm covers them in principle but the present PhasedNP representation does not yet distinguish embedded vs matrix domains.

def Phenomena.Case.Studies.BakerVinokurova2010.sakhaConfig : Syntax.Case.CaseSystemConfig

Sakha's case system: accusative alignment with the @cite{baker-vinokurova-2010} two-modality split. ACC and DAT are dependent (Marantz); NOM and GEN are Agree-based (Chomsky).

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.sakha_acc_dependent : sakhaConfig.accMode = Syntax.Case.AccAssignment.dependent

theorem Phenomena.Case.Studies.BakerVinokurova2010.sakha_dat_dependent : sakhaConfig.datMode = Syntax.Case.DatAssignment.dependent

theorem Phenomena.Case.Studies.BakerVinokurova2010.sakha_nom_agree : sakhaConfig.nomMode = Syntax.Case.NomAssignment.agreeT

theorem Phenomena.Case.Studies.BakerVinokurova2010.sakha_gen_agree : sakhaConfig.genMode = Syntax.Case.GenAssignment.agreeD

theorem Phenomena.Case.Studies.BakerVinokurova2010.two_modalities_present : (sakhaConfig.accMode = Syntax.Case.AccAssignment.dependent ∨ sakhaConfig.datMode = Syntax.Case.DatAssignment.dependent) ∧ (sakhaConfig.nomMode = Syntax.Case.NomAssignment.agreeT ∨ sakhaConfig.genMode = Syntax.Case.GenAssignment.agreeD)

The two-modality thesis stated as a structural property of the config: at least one case is configurational, at least one is Agree-based. Mongolian shares the configurational ACC but uses a nonstructural DAT, so Sakha is the strictest exemplar.

def Phenomena.Case.Studies.BakerVinokurova2010.subj (label : String) : Syntax.Case.PhasedNP

A subject NP merged at the vP edge / SpecTP — visible on the CP cycle.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.subj label = { label := label, lexicalCase := none, basePhase := Syntax.Case.CasePhase.cp }

def Phenomena.Case.Studies.BakerVinokurova2010.shiftedVP (label : String) : Syntax.Case.PhasedNP

A VP-internal NP that has shifted (specific object, raised theme).

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.shiftedVP label = { label := label, lexicalCase := none, basePhase := Syntax.Case.CasePhase.vp, shifted := true }

def Phenomena.Case.Studies.BakerVinokurova2010.lowVP (label : String) : Syntax.Case.PhasedNP

A VP-internal NP that has not shifted (nonspecific object).

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.lowVP label = { label := label, lexicalCase := none, basePhase := Syntax.Case.CasePhase.vp }

def Phenomena.Case.Studies.BakerVinokurova2010.transSpecific : List Syntax.Case.PhasedNP

"Masha cake-ACC ate" with a specific object: the object shifts, competes with the subject on the CP cycle, and is valued ACC.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.transSpecific = [Phenomena.Case.Studies.BakerVinokurova2010.subj "subj", Phenomena.Case.Studies.BakerVinokurova2010.shiftedVP "obj"]

def Phenomena.Case.Studies.BakerVinokurova2010.transSpecificResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.trans_specific_obj_acc : Syntax.Case.getCaseOf "obj" transSpecificResult = some UD.Case.acc

Specific object surfaces with ACC, by the (4b)/(86) ACC rule on the CP cycle.

theorem Phenomena.Case.Studies.BakerVinokurova2010.trans_specific_obj_dependent : Syntax.Case.getSourceOf "obj" transSpecificResult = some Syntax.Case.CaseSource.dependent

The ACC on the specific object is dependent case, not lexical or Agree-based — verifying the Marantz modality is doing the work.

theorem Phenomena.Case.Studies.BakerVinokurova2010.trans_specific_subj_nom : Syntax.Case.getCaseOf "subj" transSpecificResult = some UD.Case.nom

Subject is valued NOM by T-Agree (paper (5)/(86)).

theorem Phenomena.Case.Studies.BakerVinokurova2010.trans_specific_subj_agree : Syntax.Case.getSourceOf "subj" transSpecificResult = some Syntax.Case.CaseSource.agree

The NOM on the subject is the Chomskyan Agree modality, not the Marantzian unmarked default — the central contrast with Mongolian and the structural payoff of nomMode := .agreeT.

def Phenomena.Case.Studies.BakerVinokurova2010.transNonspecific : List Syntax.Case.PhasedNP

"Masha cake ate" with a nonspecific object: the object stays in VP and is invisible to T on the CP cycle, so the ACC rule never fires (no competitor pair). The object surfaces unmarked.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.transNonspecific = [Phenomena.Case.Studies.BakerVinokurova2010.subj "subj", Phenomena.Case.Studies.BakerVinokurova2010.lowVP "obj"]

def Phenomena.Case.Studies.BakerVinokurova2010.transNonspecificResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.trans_nonspecific_obj_unmarked : Syntax.Case.getSourceOf "obj" transNonspecificResult = some Syntax.Case.CaseSource.unmarked

Nonspecific object: no ACC, surfaces unmarked. PIC-driven DOM.

theorem Phenomena.Case.Studies.BakerVinokurova2010.trans_nonspecific_subj_nom : Syntax.Case.getCaseOf "subj" transNonspecificResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "subj" transNonspecificResult = some Syntax.Case.CaseSource.agree

Subject still gets NOM by T-Agree — the Agree probe always finds the highest CP-visible unvalued NP, which is the subject in both DOM variants.

theorem Phenomena.Case.Studies.BakerVinokurova2010.dom_alternation_in_object : Syntax.Case.getCaseOf "obj" transSpecificResult ≠ Syntax.Case.getCaseOf "obj" transNonspecificResult

The DOM alternation: object case differs purely by whether the object has shifted out of VP, with no change to the subject. The grammar does not stipulate "specificity → ACC"; it is derived from phase visibility + the (4b) ACC rule.

theorem Phenomena.Case.Studies.BakerVinokurova2010.dom_subject_invariant : Syntax.Case.getCaseOf "subj" transSpecificResult = Syntax.Case.getCaseOf "subj" transNonspecificResult

The subject case is invariant across the DOM contrast — the same NOM-by-Agree applies whether the object is specific or not.

def Phenomena.Case.Studies.BakerVinokurova2010.ditransitive : List Syntax.Case.PhasedNP

Ditransitive with a specific theme. Three NPs: subj (CP), goal (VP), theme (VP, shifted). The DAT rule fires on the VP cycle for the goal (highest of two unmarked VP-internals), bleeding ACC at that cycle by Elsewhere. The theme then competes with the subject on the CP cycle and is valued ACC.

Equations

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

def Phenomena.Case.Studies.BakerVinokurova2010.ditransitiveResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.ditrans_goal_dat : Syntax.Case.getCaseOf "goal" ditransitiveResult = some UD.Case.dat ∧ Syntax.Case.getSourceOf "goal" ditransitiveResult = some Syntax.Case.CaseSource.dependent

Goal NP receives DAT by the (4a)/(85) DAT rule on the VP cycle.

theorem Phenomena.Case.Studies.BakerVinokurova2010.ditrans_theme_acc : Syntax.Case.getCaseOf "theme" ditransitiveResult = some UD.Case.acc ∧ Syntax.Case.getSourceOf "theme" ditransitiveResult = some Syntax.Case.CaseSource.dependent

Specific theme receives ACC on the CP cycle (after the goal has been valued DAT and removed from competition).

theorem Phenomena.Case.Studies.BakerVinokurova2010.ditrans_subj_nom : Syntax.Case.getCaseOf "subj" ditransitiveResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "subj" ditransitiveResult = some Syntax.Case.CaseSource.agree

Subject receives NOM by T-Agree.

theorem Phenomena.Case.Studies.BakerVinokurova2010.ditrans_full_pattern : Syntax.Case.getCaseOf "subj" ditransitiveResult = some UD.Case.nom ∧ Syntax.Case.getCaseOf "goal" ditransitiveResult = some UD.Case.dat ∧ Syntax.Case.getCaseOf "theme" ditransitiveResult = some UD.Case.acc

The full NOM/DAT/ACC ditransitive pattern derived in one step from assignCasesPhased: this is the central empirical signature of @cite{baker-vinokurova-2010}'s analysis, and it follows from the interaction of the two modalities, not from a stipulated case-assignment template.

theorem Phenomena.Case.Studies.BakerVinokurova2010.dat_bleeds_acc_on_vp_cycle : (List.filter (fun (x : Syntax.Case.CasedNP) => x.case == UD.Case.acc) ditransitiveResult).length = 1 ∧ (List.filter (fun (x : Syntax.Case.CasedNP) => x.case == UD.Case.dat) ditransitiveResult).length = 1

Elsewhere ordering: in the ditransitive, only ONE NP gets ACC despite there being two VP-internal NPs. The (4a) DAT rule bleeds (4b) at the VP cycle.

This is the per-datum verification. The structural reason — that applyAccRule cannot overwrite any marked NP, regardless of the input — is applyAccRule_preserves_marked_at in DependentCase.lean, and the full pipeline analogue is dat_persists_through_assignCasesPhased.

def Phenomena.Case.Studies.BakerVinokurova2010.unaccusative : List Syntax.Case.PhasedNP

Unaccusative: theme raises to SpecTP (modeled with basePhase := .cp). With a single visible NP on the CP cycle, no ACC competitor exists; T-Agree values the theme NOM.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.unaccusative = [Phenomena.Case.Studies.BakerVinokurova2010.subj "theme"]

def Phenomena.Case.Studies.BakerVinokurova2010.unaccResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.unacc_theme_nom : Syntax.Case.getCaseOf "theme" unaccResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "theme" unaccResult = some Syntax.Case.CaseSource.agree

theorem Phenomena.Case.Studies.BakerVinokurova2010.unacc_no_acc : (unaccResult.all fun (x : Syntax.Case.CasedNP) => decide (x.case ≠ UD.Case.acc)) = true

No NP receives ACC in the unaccusative — the dependent ACC rule requires two unmarked competitors and there is only one NP.

These derivations exhibit both modalities firing within a single sentence: dependent case for one NP, Agree for another. This is what forces a hybrid grammar — neither pure Marantz nor pure Chomsky covers the full Sakha pattern.

theorem Phenomena.Case.Studies.BakerVinokurova2010.trans_specific_uses_both_modalities : Syntax.Case.getSourceOf "subj" transSpecificResult = some Syntax.Case.CaseSource.agree ∧ Syntax.Case.getSourceOf "obj" transSpecificResult = some Syntax.Case.CaseSource.dependent

In the specific-object monotransitive, subject and object receive case from different mechanisms: NOM by Agree, ACC by dependent case.

theorem Phenomena.Case.Studies.BakerVinokurova2010.ditrans_three_sources : Syntax.Case.getSourceOf "subj" ditransitiveResult = some Syntax.Case.CaseSource.agree ∧ Syntax.Case.getSourceOf "goal" ditransitiveResult = some Syntax.Case.CaseSource.dependent ∧ Syntax.Case.getSourceOf "theme" ditransitiveResult = some Syntax.Case.CaseSource.dependent

In the ditransitive, all three modal sources are attested: Agree (subject NOM), and two dependent cases (goal DAT, theme ACC). The .lexical and .unmarked sources are absent from this derivation — they would arise for quirky-DAT subjects and for nonspecific themes respectively.

@cite{gong-2022} adopts the Sakha framework for Mongolian but swaps datMode from .dependent to .nonstructural: Mongolian DAT is inherent. Holding ACC, NOM, GEN modes constant and varying only DAT, the algorithm correctly predicts that Mongolian ditransitives have no DAT-from-the-algorithm — DAT must come pre-loaded as lexicalCase.

def Phenomena.Case.Studies.BakerVinokurova2010.mongolianLikeConfig : Syntax.Case.CaseSystemConfig

The Mongolian config differs from Sakha only in datMode.

Equations

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

def Phenomena.Case.Studies.BakerVinokurova2010.ditransMongolian : List Syntax.Case.CasedNP

Same ditransitive input, Mongolian config: the goal is no longer valued DAT by the algorithm — it becomes an unmarked VP-internal NP, which then competes with the theme on the VP cycle for ACC.

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.mongolian_no_algorithmic_dat : (ditransMongolian.all fun (x : Syntax.Case.CasedNP) => decide (x.case ≠ UD.Case.dat)) = true

Without dependent DAT, no NP gets DAT from the algorithm. The DAT on Mongolian goals must be supplied as inherent/lexical case at the lexicon level — exactly @cite{gong-2022}'s claim.

theorem Phenomena.Case.Studies.BakerVinokurova2010.sakha_mongolian_diff_in_dat : Syntax.Case.getCaseOf "goal" ditransitiveResult ≠ Syntax.Case.getCaseOf "goal" ditransMongolian

The Sakha vs. Mongolian contrast localizes to a single config parameter — datMode — exactly as predicted by the parameterized CaseSystemConfig design.

A structural payoff of distinguishing .agree from .unmarked: the same surface case (NOM) can have two distinct sources, and the source matters for downstream computations (visibility to higher probes, raising-to-object, etc.). Sakha NOM is always .agree; a default-NOM language (pure Marantz) would have it as .unmarked.

theorem Phenomena.Case.Studies.BakerVinokurova2010.all_nom_is_agree_in_sakha : (transSpecificResult.all fun (cn : Syntax.Case.CasedNP) => decide (cn.case ≠ UD.Case.nom ∨ cn.source = Syntax.Case.CaseSource.agree)) = true ∧ (ditransitiveResult.all fun (cn : Syntax.Case.CasedNP) => decide (cn.case ≠ UD.Case.nom ∨ cn.source = Syntax.Case.CaseSource.agree)) = true ∧ (unaccResult.all fun (cn : Syntax.Case.CasedNP) => decide (cn.case ≠ UD.Case.nom ∨ cn.source = Syntax.Case.CaseSource.agree)) = true

Every NOM in Sakha derivations comes from T-Agree, never from the unmarked default. This holds across all derivations in this file by construction (because nomMode := .agreeT), and is the structural fingerprint of the Chomsky modality.

@cite{baker-vinokurova-2010} (23)–(24): morphological causatives in Sakha exhibit a striking cascade. The causee surfaces with ACC if the base verb is intransitive (one argumental NP in max VP, no DAT competitor) but with DAT if the base verb is transitive (two argumental NPs in max VP, (4a) fires marking the causee as DAT).

This is the cleanest test of the dependent-case modality: adding an NP (the lower theme) changes the case on a different NP (the causee), which is impossible under any version of head-driven Agree case. The algorithmic Mechanism — (4a) bleeding (4b) on the VP cycle — predicts the cascade without any additional stipulation.

def Phenomena.Case.Studies.BakerVinokurova2010.causativeOfIntransitive : List Syntax.Case.PhasedNP

(23a) "Sardaana made Aisen cry" — base verb 'cry' is intransitive. Max VP contains only the causee (Aisen). With only one argumental NP visible on the VP cycle, neither (4a) nor (4b) fires. The causee shifts to the CP phase, becomes a competitor for the causer (Sardaana), and is valued ACC by (4b) on the CP cycle.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.causativeOfIntransitive = [Phenomena.Case.Studies.BakerVinokurova2010.subj "causer", Phenomena.Case.Studies.BakerVinokurova2010.shiftedVP "causee"]

def Phenomena.Case.Studies.BakerVinokurova2010.causIntransResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.caus_intrans_causee_acc : Syntax.Case.getCaseOf "causee" causIntransResult = some UD.Case.acc ∧ Syntax.Case.getSourceOf "causee" causIntransResult = some Syntax.Case.CaseSource.dependent

theorem Phenomena.Case.Studies.BakerVinokurova2010.caus_intrans_causer_nom : Syntax.Case.getCaseOf "causer" causIntransResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "causer" causIntransResult = some Syntax.Case.CaseSource.agree

def Phenomena.Case.Studies.BakerVinokurova2010.causativeOfTransitive : List Syntax.Case.PhasedNP

(23b) "Misha made Masha eat soup" — base verb 'eat' is transitive. Max VP contains the causee (Masha) and theme (soup), both argumental. On the VP cycle, (4a) fires: Masha (the higher of the two unmarked NPs) is valued DAT, bleeding (4b). The theme then shifts to the CP phase, competes with the causer (Misha), and is valued ACC.

Equations

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

def Phenomena.Case.Studies.BakerVinokurova2010.causTransResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.caus_trans_causee_dat : Syntax.Case.getCaseOf "causee" causTransResult = some UD.Case.dat ∧ Syntax.Case.getSourceOf "causee" causTransResult = some Syntax.Case.CaseSource.dependent

theorem Phenomena.Case.Studies.BakerVinokurova2010.caus_trans_theme_acc : Syntax.Case.getCaseOf "theme" causTransResult = some UD.Case.acc ∧ Syntax.Case.getSourceOf "theme" causTransResult = some Syntax.Case.CaseSource.dependent

theorem Phenomena.Case.Studies.BakerVinokurova2010.caus_trans_causer_nom : Syntax.Case.getCaseOf "causer" causTransResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "causer" causTransResult = some Syntax.Case.CaseSource.agree

theorem Phenomena.Case.Studies.BakerVinokurova2010.causee_case_depends_on_base_transitivity : Syntax.Case.getCaseOf "causee" causIntransResult = some UD.Case.acc ∧ Syntax.Case.getCaseOf "causee" causTransResult = some UD.Case.dat

The causative cascade: the same causative morpheme produces ACC on the causee in (23a) and DAT on the causee in (23b). The only difference is the transitivity of the base verb — i.e., the number of argumental NPs in max VP. This is the structural signature of dependent case.

@cite{baker-vinokurova-2010} (8)–(9): rules (4a)/(4b) only apply between argumental NPs (those bearing a θ-role w.r.t. some case- assigning head). Bare-NP adverbs like sajyn 'summer' do not count as case competitors, even when c-commanded by another caseless NP.

The PhasedNP isArgumental field captures this: when set to false, the NP is filtered out of unmarkedVisible and so cannot trigger or receive dependent case. The very same noun that surfaces as ACC when functioning as the object of a transitive verb (8c) surfaces unmarked when functioning as a temporal adverb (8a)/(8b).

def Phenomena.Case.Studies.BakerVinokurova2010.adverb (label : String) : Syntax.Case.PhasedNP

Adverbial NP — bears no θ-role w.r.t. a case-assigning head.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.adverb label = { label := label, lexicalCase := none, basePhase := Syntax.Case.CasePhase.cp, isArgumental := false }

def Phenomena.Case.Studies.BakerVinokurova2010.intransitiveWithAdverb : List Syntax.Case.PhasedNP

(8a) "Bihigi beqehee ystan-nybyt" 'we yesterday jumped'. Two NPs: 'we' (subject, argumental) and 'yesterday' (adverb, non-argumental). The adverb is filtered from case competition; only one argumental NP is visible to T-Agree on the CP cycle.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.intransitiveWithAdverb = [Phenomena.Case.Studies.BakerVinokurova2010.subj "subj", Phenomena.Case.Studies.BakerVinokurova2010.adverb "yesterday"]

def Phenomena.Case.Studies.BakerVinokurova2010.intrAdvResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.adverb_does_not_get_acc : Syntax.Case.getCaseOf "yesterday" intrAdvResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "yesterday" intrAdvResult = some Syntax.Case.CaseSource.unmarked

The adverb is not marked ACC: rule (4b) does not see it as a case competitor. The subject is valued NOM by T-Agree, and the adverb falls through to the default sweep with unmarked NOM.

theorem Phenomena.Case.Studies.BakerVinokurova2010.subj_with_adverb_nom_agree : Syntax.Case.getCaseOf "subj" intrAdvResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "subj" intrAdvResult = some Syntax.Case.CaseSource.agree

def Phenomena.Case.Studies.BakerVinokurova2010.transitiveSummerObject : List Syntax.Case.PhasedNP

(8c) "Masha sajyn-y axt-ar" 'Masha summer-ACC misses'. Same noun 'summer', now functioning as the object of transitive 'miss' — it bears a θ-role and so counts as argumental. Now (4b) applies and the object is marked ACC, exactly the contrast (8a/b vs 8c).

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.transitiveSummerObject = [Phenomena.Case.Studies.BakerVinokurova2010.subj "masha", Phenomena.Case.Studies.BakerVinokurova2010.shiftedVP "summer"]

def Phenomena.Case.Studies.BakerVinokurova2010.transSummerResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.summer_as_object_gets_acc : Syntax.Case.getCaseOf "summer" transSummerResult = some UD.Case.acc ∧ Syntax.Case.getSourceOf "summer" transSummerResult = some Syntax.Case.CaseSource.dependent

theorem Phenomena.Case.Studies.BakerVinokurova2010.argumental_status_drives_case : Syntax.Case.getCaseOf "summer" transSummerResult ≠ Syntax.Case.getCaseOf "yesterday" intrAdvResult ∨ Syntax.Case.getSourceOf "summer" transSummerResult ≠ Syntax.Case.getSourceOf "yesterday" intrAdvResult

The argumental contrast: the very same lexical noun receives ACC when argumental and unmarked NOM when adverbial. The grammar does not stipulate that 'summer' is ambiguous between an argumental and an adverbial entry; both readings reduce to a single algorithm parameterized by the isArgumental feature.

Replacing the trivial two_modalities_present (which only restated the config) with a theorem that no single modality — pure Marantz or pure Chomsky — can produce the Sakha derivational pattern. The two-modality grammar is empirically required, not just stipulated.

def Phenomena.Case.Studies.BakerVinokurova2010.pureMarantz : Syntax.Case.CaseSystemConfig

Pure Marantz (Sakha pattern with NOM as unmarked default and no Agree-based case): all structural cases are configurational.

Equations

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

def Phenomena.Case.Studies.BakerVinokurova2010.pureChomsky : Syntax.Case.CaseSystemConfig

Pure Chomsky: every structural case assigned by Agree with a functional head. v-Agree marks the lowest CP-visible argumental NP as ACC; T-Agree marks the highest as NOM; D-Agree marks DP- internals as GEN; DAT is purely lexical/inherent (.nonstructural). This is the standard @cite{chomsky-2000}/@cite{chomsky-2001} configuration.

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.pure_marantz_subj_unmarked : Syntax.Case.getSourceOf "subj" (Syntax.Case.assignCasesPhased pureMarantz ditransitive) = some Syntax.Case.CaseSource.unmarked

Pure Marantz produces the same surface NOM on the subject as Sakha — but with source := .unmarked, not .agree. The structural fingerprint of the modality differs even when the morphology coincides.

theorem Phenomena.Case.Studies.BakerVinokurova2010.sakha_subj_distinct_from_pure_marantz : Syntax.Case.getSourceOf "subj" (Syntax.Case.assignCasesPhased pureMarantz ditransitive) ≠ Syntax.Case.getSourceOf "subj" ditransitiveResult

theorem Phenomena.Case.Studies.BakerVinokurova2010.pure_chomsky_no_algorithmic_dat : ((Syntax.Case.assignCasesPhased pureChomsky ditransitive).all fun (x : Syntax.Case.CasedNP) => decide (x.case ≠ UD.Case.dat)) = true

Pure Chomsky has datMode := .nonstructural, so the algorithm never derives DAT — Mongolian-style, every DAT must be lexical. This contradicts the Sakha pattern where DAT is productive on structural goals.

theorem Phenomena.Case.Studies.BakerVinokurova2010.pure_chomsky_acc_via_agree : Syntax.Case.getCaseOf "theme" (Syntax.Case.assignCasesPhased pureChomsky ditransitive) = some UD.Case.acc ∧ Syntax.Case.getSourceOf "theme" (Syntax.Case.assignCasesPhased pureChomsky ditransitive) = some Syntax.Case.CaseSource.agree

Pure Chomsky's v-Agree fires under accMode := .agreeV and marks the theme ACC via Agree (not via the dependent rule). This makes the source-distinction operative, not just the case-distinction: Sakha derives ACC via .dependent, pure Chomsky via .agree.

theorem Phenomena.Case.Studies.BakerVinokurova2010.pure_chomsky_misses_causative_cascade : Syntax.Case.getCaseOf "causee" (Syntax.Case.assignCasesPhased pureChomsky causativeOfTransitive) ≠ some UD.Case.dat ∧ Syntax.Case.getCaseOf "causee" causTransResult = some UD.Case.dat

The causative cascade is the canonical wedge against any pure-Agree theory of structural case. Adding the lower theme to a transitive-base causative changes the case on the causee (ACC → DAT) — but no head's Agree relation has been altered, only the count of NPs in max VP. Pure Chomsky predicts the causee in (23b) surfaces with NOM-by-default, exactly because its v-Agree probe targets the theme; the (4a)/dependent-DAT rule cannot apply without datMode := .dependent.

theorem Phenomena.Case.Studies.BakerVinokurova2010.two_modalities_required : Syntax.Case.getSourceOf "subj" (Syntax.Case.assignCasesPhased pureMarantz ditransitive) ≠ some Syntax.Case.CaseSource.agree ∧ (¬∃ cn ∈ Syntax.Case.assignCasesPhased pureChomsky ditransitive, cn.case = UD.Case.dat) ∧ Syntax.Case.getCaseOf "causee" (Syntax.Case.assignCasesPhased pureChomsky causativeOfTransitive) ≠ some UD.Case.dat ∧ Syntax.Case.getSourceOf "subj" ditransitiveResult = some Syntax.Case.CaseSource.agree ∧ (∃ cn ∈ ditransitiveResult, cn.case = UD.Case.dat) ∧ Syntax.Case.getCaseOf "causee" causTransResult = some UD.Case.dat

The strong two-modality theorem: neither pure modality derives the Sakha pattern. Pure Marantz fails the NOM-as-Agree fingerprint (subject NOM source = .unmarked). Pure Chomsky fails on DAT — not just on the ditransitive but, more sharply, on the causative cascade where adding an NP changes another NP's case in a way no Agree relation can mediate. The two-modality grammar is required, not stipulated.

@cite{baker-vinokurova-2010} (5)/(86): D Agrees with the possessor inside DP and values it GEN. The clausal cycles see the DP as opaque — its possessor is filtered out of unmarkedVisible by the inDP flag — and applyGenAgree runs as the DP-internal counterpart to T-Agree. This is the second Agree-modality slot (genMode := .agreeD) that distinguishes the Sakha grammar from a purely Marantzian one.

def Phenomena.Case.Studies.BakerVinokurova2010.possessor (label : String) : Syntax.Case.PhasedNP

A DP-internal possessor: opaque to clause-level case competition but valued GEN by D-Agree.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.possessor label = { label := label, lexicalCase := none, basePhase := Syntax.Case.CasePhase.cp, inDP := true }

def Phenomena.Case.Studies.BakerVinokurova2010.possessedSubject : List Syntax.Case.PhasedNP

"Aisen's house [is in town]" — the matrix subject is a DP whose possessor aisen is valued GEN by D-Agree. The possessor is invisible to clausal probes; the head noun (house) is the subject of T-Agree and surfaces NOM.

Equations

• Phenomena.Case.Studies.BakerVinokurova2010.possessedSubject = [Phenomena.Case.Studies.BakerVinokurova2010.subj "house", Phenomena.Case.Studies.BakerVinokurova2010.possessor "aisen"]

def Phenomena.Case.Studies.BakerVinokurova2010.possessedResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.possessor_gets_gen_via_agree : Syntax.Case.getCaseOf "aisen" possessedResult = some UD.Case.gen ∧ Syntax.Case.getSourceOf "aisen" possessedResult = some Syntax.Case.CaseSource.agree

theorem Phenomena.Case.Studies.BakerVinokurova2010.possessed_head_gets_nom : Syntax.Case.getCaseOf "house" possessedResult = some UD.Case.nom ∧ Syntax.Case.getSourceOf "house" possessedResult = some Syntax.Case.CaseSource.agree

def Phenomena.Case.Studies.BakerVinokurova2010.transWithPossessedObj : List Syntax.Case.PhasedNP

The GEN possessor is invisible to (4b)/ACC: in a transitive with a possessed object, the head noun is what receives ACC, not the possessor (which is busy being valued GEN inside its DP).

Equations

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

def Phenomena.Case.Studies.BakerVinokurova2010.transPossResult : List Syntax.Case.CasedNP

Equations

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

theorem Phenomena.Case.Studies.BakerVinokurova2010.possessor_is_opaque_to_clausal_acc : Syntax.Case.getCaseOf "aisen" transPossResult = some UD.Case.gen ∧ Syntax.Case.getCaseOf "book" transPossResult = some UD.Case.acc

theorem Phenomena.Case.Studies.BakerVinokurova2010.all_four_modalities_in_one_clause : have cl := [subj "subj", lowVP "goal", shiftedVP "theme", possessor "aisen"]; have r := Syntax.Case.assignCasesPhased sakhaConfig cl; Syntax.Case.getSourceOf "subj" r = some Syntax.Case.CaseSource.agree ∧ Syntax.Case.getSourceOf "aisen" r = some Syntax.Case.CaseSource.agree ∧ Syntax.Case.getSourceOf "goal" r = some Syntax.Case.CaseSource.dependent ∧ Syntax.Case.getSourceOf "theme" r = some Syntax.Case.CaseSource.dependent

The two Agree modalities (T → NOM, D → GEN) coexist with the two dependent modalities (DAT, ACC) in a single derivation — the strongest empirical demonstration of the four-slot parameterization at work.

theorem Phenomena.Case.Studies.BakerVinokurova2010.all_sakha_derivations_total : transSpecificResult.length = transSpecific.length ∧ transNonspecificResult.length = transNonspecific.length ∧ ditransitiveResult.length = ditransitive.length ∧ unaccResult.length = unaccusative.length ∧ causIntransResult.length = causativeOfIntransitive.length ∧ causTransResult.length = causativeOfTransitive.length ∧ intrAdvResult.length = intransitiveWithAdverb.length ∧ transSummerResult.length = transitiveSummerObject.length ∧ possessedResult.length = possessedSubject.length ∧ transPossResult.length = transWithPossessedObj.length

The phased algorithm is total on every Sakha derivation in this file: each input NP appears in the output with exactly one case. Follows from assignCasesPhased_length in DependentCase.lean.