@cite{ozaki-2026} — Japanese Accusative/Ablative Alternation: Data

@cite{ozaki-2026}

Empirical data from @cite{ozaki-2026} 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 Fragments.Japanese.Case.CaseMarker (the authoritative case-marker registry per @cite{tsujimura-2014}), not as a parallel local enum.

inductive Phenomena.Case.Ozaki2026.Data.ArgumenthoodDiagnostic : Type

Diagnostics for argumenthood (vs. adjuncthood).

• ellipsis : ArgumenthoodDiagnostic
• longDistanceScrambling : ArgumenthoodDiagnostic

@[implicit_reducible]

instance Phenomena.Case.Ozaki2026.Data.instDecidableEqArgumenthoodDiagnostic : DecidableEq ArgumenthoodDiagnostic

Equations

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

@[implicit_reducible]

instance Phenomena.Case.Ozaki2026.Data.instReprArgumenthoodDiagnostic : Repr ArgumenthoodDiagnostic

Equations

• Phenomena.Case.Ozaki2026.Data.instReprArgumenthoodDiagnostic = { reprPrec := Phenomena.Case.Ozaki2026.Data.instReprArgumenthoodDiagnostic.repr }

def Phenomena.Case.Ozaki2026.Data.instReprArgumenthoodDiagnostic.repr : ArgumenthoodDiagnostic → ℕ → Std.Format

Equations

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

inductive Phenomena.Case.Ozaki2026.Data.UnaccusativityDiagnostic : Type

Diagnostics for unaccusativity.

• passivization : UnaccusativityDiagnostic
• naniOWhAdjunct : UnaccusativityDiagnostic

@[implicit_reducible]

instance Phenomena.Case.Ozaki2026.Data.instDecidableEqUnaccusativityDiagnostic : DecidableEq UnaccusativityDiagnostic

Equations

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

@[implicit_reducible]

instance Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDiagnostic : Repr UnaccusativityDiagnostic

Equations

• Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDiagnostic = { reprPrec := Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDiagnostic.repr }

def Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDiagnostic.repr : UnaccusativityDiagnostic → ℕ → Std.Format

Equations

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

structure Phenomena.Case.Ozaki2026.Data.AlternationDatum : Type

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

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

structure Phenomena.Case.Ozaki2026.Data.UnaccusativityDatum : Type

An unaccusativity diagnostic datum.

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

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

Equations

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

@[implicit_reducible]

instance Phenomena.Case.Ozaki2026.Data.instDecidableEqUnaccusativityDatum : DecidableEq UnaccusativityDatum

Equations

• Phenomena.Case.Ozaki2026.Data.instDecidableEqUnaccusativityDatum = Phenomena.Case.Ozaki2026.Data.instDecidableEqUnaccusativityDatum.decEq

def Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDatum.repr : UnaccusativityDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDatum : Repr UnaccusativityDatum

Equations

• Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDatum = { reprPrec := Phenomena.Case.Ozaki2026.Data.instReprUnaccusativityDatum.repr }

structure Phenomena.Case.Ozaki2026.Data.ArgumenthoodDatum : Type

An argumenthood diagnostic datum.

• verb : String
• sourceMarker : Fragments.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 Phenomena.Case.Ozaki2026.Data.hanareru_acc : AlternationDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.hanareru_abl : AlternationDatum

Equations

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

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 Phenomena.Case.Ozaki2026.Data.deru_acc : AlternationDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.deru_abl : AlternationDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.alternationData : List AlternationDatum

Equations

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

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

@cite{funakoshi-2016}'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 Phenomena.Case.Ozaki2026.Data.deru_ellipsis_acc : ArgumenthoodDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.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)

@cite{saito-1985}: 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 Phenomena.Case.Ozaki2026.Data.hanareru_scrambling_acc : ArgumenthoodDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.hanareru_scrambling_abl : ArgumenthoodDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.argumenthoodData : List ArgumenthoodDatum

Equations

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

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 Phenomena.Case.Ozaki2026.Data.hanareru_indirect_passive : UnaccusativityDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.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)

@cite{kurafuji-1997}: nani-o 'what-ACC' can mean 'why' with unergatives and transitives, but not with unaccusatives. Alternation verbs block this reading, patterning with unaccusatives.

def Phenomena.Case.Ozaki2026.Data.hanareru_nanio : UnaccusativityDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.unaccusativityData : List UnaccusativityDatum

Equations

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

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

Both ACC and ABL variants are grammatical for alternation verbs.

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

All argumenthood diagnostics succeed regardless of case marking.

theorem Phenomena.Case.Ozaki2026.Data.direct_passive_blocked : hanareru_direct_passive.grammatical = false

Direct passive is ungrammatical (hallmark of unaccusativity).

theorem Phenomena.Case.Ozaki2026.Data.indirect_passive_ok : hanareru_indirect_passive.grammatical = true

Indirect passive is grammatical (expected for unaccusatives).

theorem Phenomena.Case.Ozaki2026.Data.nanio_blocked : hanareru_nanio.grammatical = false

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

theorem Phenomena.Case.Ozaki2026.Data.alternation_count : alternationData.length = 4

Four alternation data points total.

theorem Phenomena.Case.Ozaki2026.Data.argumenthood_count : argumenthoodData.length = 4

Four argumenthood data points total.

theorem Phenomena.Case.Ozaki2026.Data.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 Fragments.Japanese.Case entry — the dissolution of this file's prior local CaseMarking enum (which re-stipulated four particles already present in Fragments.Japanese.Case) is now mechanically auditable: editing the Fragment's o or kara definitions will cascade through these provenance theorems.

theorem Phenomena.Case.Ozaki2026.Data.hanareru_acc_uses_o : hanareru_acc.sourceMarker = Fragments.Japanese.Case.o

theorem Phenomena.Case.Ozaki2026.Data.hanareru_abl_uses_kara : hanareru_abl.sourceMarker = Fragments.Japanese.Case.kara

theorem Phenomena.Case.Ozaki2026.Data.deru_acc_uses_o : deru_acc.sourceMarker = Fragments.Japanese.Case.o

theorem Phenomena.Case.Ozaki2026.Data.deru_abl_uses_kara : deru_abl.sourceMarker = Fragments.Japanese.Case.kara

theorem Phenomena.Case.Ozaki2026.Data.alternation_crosses_tsujimura_split : Fragments.Japanese.Case.o.omissibleInCasual = true ∧ Fragments.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 Phenomena.Case.Ozaki2026.Data.departure_no_external : ¬Minimalist.voiceAnticausative.AssignsTheta

Departure verbs predict no external argument: non-thematic Voice does not assign a θ-role (@cite{kratzer-1996}, @cite{schaefer-2025}).

theorem Phenomena.Case.Ozaki2026.Data.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 Phenomena.Case.Ozaki2026.Data.departure_voice_no_theta : ¬Minimalist.voiceAnticausative.AssignsTheta

Non-thematic Voice assigns no θ-role.

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

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

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

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

theorem Phenomena.Case.Ozaki2026.Data.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 Phenomena.Case.Ozaki2026.Data.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 Phenomena.Case.Ozaki2026.Data.agree_acc_needs_phase_head : ¬Minimalist.voiceAnticausative.IsPhasal

Anticausative Voice is not a phase head.

theorem Phenomena.Case.Ozaki2026.Data.agentive_has_phase_head : Minimalist.voiceAgent.IsPhasal

Agentive Voice IS a phase head.

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

The accusative unaccusative paradox.

theorem Phenomena.Case.Ozaki2026.Data.hanareru_is_unaccusative : Fragments.Japanese.Predicates.hanareru.unaccusative = true

Fragment entry for hanareru is marked unaccusative.

theorem Phenomena.Case.Ozaki2026.Data.deru_is_unaccusative : Fragments.Japanese.Predicates.deru.unaccusative = true

Fragment entry for deru is marked unaccusative.

theorem Phenomena.Case.Ozaki2026.Data.hanareru_not_passivizable : Fragments.Japanese.Predicates.hanareru.passivizable = false

Fragment entry for hanareru is not passivizable.

theorem Phenomena.Case.Ozaki2026.Data.deru_not_passivizable : Fragments.Japanese.Predicates.deru.passivizable = false

Fragment entry for deru is not passivizable.

theorem Phenomena.Case.Ozaki2026.Data.passive_data_matches_fragment : hanareru_direct_passive.grammatical = false ∧ Fragments.Japanese.Predicates.hanareru.passivizable = false

Non-passivizability aligns with direct passive being ungrammatical.

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

Non-passivizability follows from Voice theory.

theorem Phenomena.Case.Ozaki2026.Data.hanareru_form_matches : hanareru_acc.verb = Fragments.Japanese.Predicates.hanareru.form

Verb forms in Data match Fragment entries.

theorem Phenomena.Case.Ozaki2026.Data.deru_form_matches : deru_acc.verb = Fragments.Japanese.Predicates.deru.form

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

All argumenthood diagnostics succeed.

theorem Phenomena.Case.Ozaki2026.Data.hanareru_unaccusative_derived : Fragments.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 Phenomena.Case.Ozaki2026.Data.deru_unaccusative_derived : Fragments.Japanese.Predicates.deru.derivedUnaccusative = true

Deru's unaccusativity is DERIVED from its voice type.

theorem Phenomena.Case.Ozaki2026.Data.hanareru_stored_matches_derived : Fragments.Japanese.Predicates.hanareru.unaccusative = Fragments.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 Phenomena.Case.Ozaki2026.Data.deru_stored_matches_derived : Fragments.Japanese.Predicates.deru.unaccusative = Fragments.Japanese.Predicates.deru.derivedUnaccusative

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

Direct passive requires thematic Voice, which departure verbs lack.