[Oza26] — Japanese Accusative/Ablative Alternation: Data

[Oza26]

Empirical data from [Oza26] on Japanese departure verbs that alternate between accusative -o and ablative kara marking on the source argument.

Key Empirical Facts

1. Alternation: Departure verbs like hanareru 'leave' and deru 'exit' allow both ACC and ABL on the source:

   • "Taro-ga mura-o hanare-ta" (ACC)
   • "Taro-ga mura-kara hanare-ta" (ABL)

2. Argumenthood of source: The source behaves as an argument regardless of case — it can undergo VP ellipsis and long-distance scrambling.

3. Unaccusativity: These verbs are unaccusative:

   • Only indirect passive (-rare), no direct passive (-niyotte)
   • Nani-o wh-adjunct test patterns with unaccusatives

Theory-Neutral

This file contains no theoretical commitments. See Bridge.lean for connection to dependent case theory and Minimalist syntax.

Case marking on the source argument of alternation verbs is recorded as a Japanese.Case.CaseMarker (the authoritative case-marker registry per [Tsu14]), not as a parallel local enum.

inductive Ozaki2026.ArgumenthoodDiagnostic : Type

Diagnostics for argumenthood (vs. adjuncthood).

• ellipsis : ArgumenthoodDiagnostic
• longDistanceScrambling : ArgumenthoodDiagnostic

@[implicit_reducible]

instance Ozaki2026.instDecidableEqArgumenthoodDiagnostic : DecidableEq ArgumenthoodDiagnostic

Equations

• Ozaki2026.instDecidableEqArgumenthoodDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ozaki2026.instReprArgumenthoodDiagnostic.repr : ArgumenthoodDiagnostic → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Ozaki2026.instReprArgumenthoodDiagnostic : Repr ArgumenthoodDiagnostic

Equations

• Ozaki2026.instReprArgumenthoodDiagnostic = { reprPrec := Ozaki2026.instReprArgumenthoodDiagnostic.repr }

inductive Ozaki2026.UnaccusativityDiagnostic : Type

Diagnostics for unaccusativity.

• passivization : UnaccusativityDiagnostic
• naniOWhAdjunct : UnaccusativityDiagnostic

@[implicit_reducible]

instance Ozaki2026.instDecidableEqUnaccusativityDiagnostic : DecidableEq UnaccusativityDiagnostic

Equations

• Ozaki2026.instDecidableEqUnaccusativityDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ozaki2026.instReprUnaccusativityDiagnostic.repr : UnaccusativityDiagnostic → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Ozaki2026.instReprUnaccusativityDiagnostic : Repr UnaccusativityDiagnostic

Equations

• Ozaki2026.instReprUnaccusativityDiagnostic = { reprPrec := Ozaki2026.instReprUnaccusativityDiagnostic.repr }

structure Ozaki2026.AlternationDatum : Type

A single case alternation datum: a verb form with a source argument in a particular case, plus grammaticality.

• verb : String
• sourceMarker : Japanese.Case.CaseMarker
• grammatical : Bool
• sentence : String
• exampleNum : String

structure Ozaki2026.UnaccusativityDatum : Type

An unaccusativity diagnostic datum.

• verb : String
• diagnostic : UnaccusativityDiagnostic
• passiveType : Option Japanese.Passive.PassiveType
• grammatical : Bool
• sentence : String
• exampleNum : String

@[implicit_reducible]

instance Ozaki2026.instDecidableEqUnaccusativityDatum : DecidableEq UnaccusativityDatum

Equations

• Ozaki2026.instDecidableEqUnaccusativityDatum = Ozaki2026.instDecidableEqUnaccusativityDatum.decEq

def Ozaki2026.instDecidableEqUnaccusativityDatum.decEq (x✝ x✝¹ : UnaccusativityDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Ozaki2026.instReprUnaccusativityDatum : Repr UnaccusativityDatum

Equations

• Ozaki2026.instReprUnaccusativityDatum = { reprPrec := Ozaki2026.instReprUnaccusativityDatum.repr }

def Ozaki2026.instReprUnaccusativityDatum.repr : UnaccusativityDatum → ℕ → Std.Format

Equations

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

structure Ozaki2026.ArgumenthoodDatum : Type

An argumenthood diagnostic datum.

• verb : String
• sourceMarker : Japanese.Case.CaseMarker
• diagnostic : ArgumenthoodDiagnostic
• grammatical : Bool
• sentence : String
• exampleNum : String

hanareru 'leave' — ACC/ABL alternation (ex. 1)

"Taro-ga mura-{o/kara} hanare-ta." (Taro-NOM village-{ACC/from} leave-PAST)

def Ozaki2026.hanareru_acc : AlternationDatum

Equations

• Ozaki2026.hanareru_acc = { verb := "hanareru", sourceMarker := Japanese.Case.o, grammatical := true, sentence := "Taro-ga mura-o hanare-ta", exampleNum := "1" }

def Ozaki2026.hanareru_abl : AlternationDatum

Equations

• Ozaki2026.hanareru_abl = { verb := "hanareru", sourceMarker := Japanese.Case.kara, grammatical := true, sentence := "Taro-ga mura-kara hanare-ta", exampleNum := "1" }

deru 'exit' — ACC/ABL alternation (implicit in ex. 9)

The paper uses deru with "eki" (station) in the ellipsis diagnostic (ex. 9). The basic alternation is implicit: "Taro-ga eki-{o/kara} deta."

def Ozaki2026.deru_acc : AlternationDatum

Equations

• Ozaki2026.deru_acc = { verb := "deru", sourceMarker := Japanese.Case.o, grammatical := true, sentence := "Taro-ga eki-o deta", exampleNum := "9" }

def Ozaki2026.deru_abl : AlternationDatum

Equations

• Ozaki2026.deru_abl = { verb := "deru", sourceMarker := Japanese.Case.kara, grammatical := true, sentence := "Taro-ga eki-kara deta", exampleNum := "9" }

def Ozaki2026.alternationData : List AlternationDatum

Equations

• Ozaki2026.alternationData = [Ozaki2026.hanareru_acc, Ozaki2026.hanareru_abl, Ozaki2026.deru_acc, Ozaki2026.deru_abl]

VP ellipsis — source elides as argument (ex. 9–10)

[Fun16]'s generalization: adjuncts can only be elided if no other VP-internal elements are present. The source of deru elides even with an overt adverb suguni 'quickly', confirming argumenthood. The continuation (10) is non-contradictory, showing the elided reading is available.

def Ozaki2026.deru_ellipsis_acc : ArgumenthoodDatum

Equations

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

def Ozaki2026.deru_ellipsis_abl : ArgumenthoodDatum

Equations

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

Long-distance scrambling — source scrambles freely (ex. 13)

[Sai85]: arguments can undergo long-distance scrambling, adjuncts cannot. The source of hanareru scrambles out of the embedded clause, confirming argumenthood regardless of case marking.

def Ozaki2026.hanareru_scrambling_acc : ArgumenthoodDatum

Equations

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

def Ozaki2026.hanareru_scrambling_abl : ArgumenthoodDatum

Equations

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

def Ozaki2026.argumenthoodData : List ArgumenthoodDatum

Equations

• Ozaki2026.argumenthoodData = [Ozaki2026.deru_ellipsis_acc, Ozaki2026.deru_ellipsis_abl, Ozaki2026.hanareru_scrambling_acc, Ozaki2026.hanareru_scrambling_abl]

Passive — only indirect passive available (ex. 14, 20)

Japanese has two passives: indirect (-rare-, adversative, available to all verbs including unaccusatives) and direct (-niyotte, requires thematic Voice). If alternation verbs had thematic Voice, direct passive should be possible — but it is not (ex. 20).

def Ozaki2026.hanareru_indirect_passive : UnaccusativityDatum

Equations

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

def Ozaki2026.hanareru_direct_passive : UnaccusativityDatum

Equations

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

nani-o wh-adjunct — blocked with unaccusatives (ex. 26)

[Kur97]: nani-o 'what-ACC' can mean 'why' with unergatives and transitives, but not with unaccusatives. Alternation verbs block this reading, patterning with unaccusatives.

def Ozaki2026.hanareru_nanio : UnaccusativityDatum

Equations

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

def Ozaki2026.unaccusativityData : List UnaccusativityDatum

Equations

• Ozaki2026.unaccusativityData = [Ozaki2026.hanareru_indirect_passive, Ozaki2026.hanareru_direct_passive, Ozaki2026.hanareru_nanio]

theorem Ozaki2026.both_variants_grammatical : (alternationData.all fun (x : AlternationDatum) => x.grammatical) = true

Both ACC and ABL variants are grammatical for alternation verbs.

theorem Ozaki2026.argumenthood_regardless_of_case : (argumenthoodData.all fun (x : ArgumenthoodDatum) => x.grammatical) = true

All argumenthood diagnostics succeed regardless of case marking.

theorem Ozaki2026.direct_passive_blocked : hanareru_direct_passive.grammatical = false

Direct passive is ungrammatical (hallmark of unaccusativity).

theorem Ozaki2026.indirect_passive_ok : hanareru_indirect_passive.grammatical = true

Indirect passive is grammatical (expected for unaccusatives).

theorem Ozaki2026.nanio_blocked : hanareru_nanio.grammatical = false

Nani-o is blocked — patterns with unaccusatives, not transitives.

theorem Ozaki2026.alternation_count : alternationData.length = 4

Four alternation data points total.

theorem Ozaki2026.argumenthood_count : argumenthoodData.length = 4

Four argumenthood data points total.

theorem Ozaki2026.unaccusativity_count : unaccusativityData.length = 3

Three unaccusativity data points total.

Provenance: source markers come from the Fragment

These four rfl theorems tie each alternation datum's sourceMarker to the corresponding Japanese.Case entry — the dissolution of this file's prior local CaseMarking enum (which re-stipulated four particles already present in Japanese.Case) is now mechanically auditable: editing the Fragment's o or kara definitions will cascade through these provenance theorems.

theorem Ozaki2026.hanareru_acc_uses_o : hanareru_acc.sourceMarker = Japanese.Case.o

theorem Ozaki2026.hanareru_abl_uses_kara : hanareru_abl.sourceMarker = Japanese.Case.kara

theorem Ozaki2026.deru_acc_uses_o : deru_acc.sourceMarker = Japanese.Case.o

theorem Ozaki2026.deru_abl_uses_kara : deru_abl.sourceMarker = Japanese.Case.kara

theorem Ozaki2026.alternation_crosses_tsujimura_split : Japanese.Case.o.omissibleInCasual = true ∧ Japanese.Case.kara.omissibleInCasual = false

The case-marker pair on each alternation datum is exactly Tsujimura's case-particle / postposition contrast: -o is omissible (case particle), -kara is not (postposition). The alternation thus crosses Tsujimura's morphosyntactic split — a Marantz/Baker dependent-case pivot (.dependent for ACC vs. .lexical for ABL, proved in §Bridge below) coincides with a Tsujimura case-particle / postposition pivot.

theorem Ozaki2026.departure_no_external : ¬Minimalist.voiceAnticausative.AssignsTheta

Departure verbs predict no external argument: non-thematic Voice does not assign a θ-role ([Kra96], [Sch25]).

theorem Ozaki2026.departure_is_inchoative : Minimalist.isInchoative (Minimalist.buildDecomposition Minimalist.voiceAnticausative [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE]) = true

Departure verbs have inchoative event structure (vGO + vBE, no vDO). Verified via buildDecomposition from Core/Voice.lean.

theorem Ozaki2026.departure_voice_no_theta : ¬Minimalist.voiceAnticausative.AssignsTheta

Non-thematic Voice assigns no θ-role.

theorem Ozaki2026.acc_derivation_correct : Syntax.Case.getCaseOf "source" Syntax.Case.accVariantResult = some Case.acc ∧ Syntax.Case.getCaseOf "leaver" Syntax.Case.accVariantResult = some Case.nom

ACC variant produces dependent ACC on source, unmarked NOM on leaver.

theorem Ozaki2026.abl_derivation_correct : Syntax.Case.getCaseOf "source" Syntax.Case.ablVariantResult = some Case.abl ∧ Syntax.Case.getCaseOf "leaver" Syntax.Case.ablVariantResult = some Case.nom

ABL variant produces lexical ABL on source, unmarked NOM on leaver.

theorem Ozaki2026.acc_source_from_configuration : Syntax.Case.getSourceOf "source" Syntax.Case.accVariantResult = some Syntax.Case.CaseSource.dependent

In the ACC variant, source case is dependent.

theorem Ozaki2026.abl_source_from_lexical_p : Syntax.Case.getSourceOf "source" Syntax.Case.ablVariantResult = some Syntax.Case.CaseSource.lexical

In the ABL variant, source case is lexical.

theorem Ozaki2026.agree_acc_needs_phase_head : ¬Minimalist.voiceAnticausative.IsPhasal

Anticausative Voice is not a phase head.

theorem Ozaki2026.agentive_has_phase_head : Minimalist.voiceAgent.IsPhasal

Agentive Voice IS a phase head.

theorem Ozaki2026.accusative_unaccusative_paradox : ¬Minimalist.voiceAnticausative.AssignsTheta ∧ ¬Minimalist.voiceAnticausative.IsPhasal ∧ Syntax.Case.getCaseOf "source" Syntax.Case.accVariantResult = some Case.acc ∧ Syntax.Case.getSourceOf "source" Syntax.Case.accVariantResult = some Syntax.Case.CaseSource.dependent

The accusative unaccusative paradox.

theorem Ozaki2026.hanareru_is_unaccusative : Japanese.Predicates.hanareru.unaccusative = true

Fragment entry for hanareru is marked unaccusative.

theorem Ozaki2026.deru_is_unaccusative : Japanese.Predicates.deru.unaccusative = true

Fragment entry for deru is marked unaccusative.

theorem Ozaki2026.hanareru_not_passivizable : Japanese.Predicates.hanareru.passivizable = false

Fragment entry for hanareru is not passivizable.

theorem Ozaki2026.deru_not_passivizable : Japanese.Predicates.deru.passivizable = false

Fragment entry for deru is not passivizable.

theorem Ozaki2026.passive_data_matches_fragment : hanareru_direct_passive.grammatical = false ∧ Japanese.Predicates.hanareru.passivizable = false

Non-passivizability aligns with direct passive being ungrammatical.

theorem Ozaki2026.passive_follows_from_voice : ¬Minimalist.voiceAnticausative.AssignsTheta ∧ Japanese.Predicates.hanareru.passivizable = false

Non-passivizability follows from Voice theory.

theorem Ozaki2026.hanareru_form_matches : hanareru_acc.verb = Japanese.Predicates.hanareru.form

Verb forms in Data match Fragment entries.

theorem Ozaki2026.deru_form_matches : deru_acc.verb = Japanese.Predicates.deru.form

theorem Ozaki2026.source_is_argument_both_frames : (argumenthoodData.all fun (x : ArgumenthoodDatum) => x.grammatical) = true

All argumenthood diagnostics succeed.

theorem Ozaki2026.hanareru_unaccusative_derived : Japanese.Predicates.hanareru.derivedUnaccusative = true

Hanareru's unaccusativity is DERIVED from its voice type, not stipulated. derivedUnaccusative uses the voiceType field to compute unaccusativity via VoiceType.assignsTheta.

theorem Ozaki2026.deru_unaccusative_derived : Japanese.Predicates.deru.derivedUnaccusative = true

Deru's unaccusativity is DERIVED from its voice type.

theorem Ozaki2026.hanareru_stored_matches_derived : Japanese.Predicates.hanareru.unaccusative = Japanese.Predicates.hanareru.derivedUnaccusative

The stored unaccusative flag agrees with the derived value. This consistency check ensures that the stipulated field and the Voice-based derivation produce the same answer.

theorem Ozaki2026.deru_stored_matches_derived : Japanese.Predicates.deru.unaccusative = Japanese.Predicates.deru.derivedUnaccusative

theorem Ozaki2026.direct_passive_requires_voice : Japanese.Passive.PassiveType.direct.requiresThematicVoice = true ∧ ¬Minimalist.voiceAnticausative.AssignsTheta

Direct passive requires thematic Voice, which departure verbs lack.