@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.

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

Case marking on the source argument of alternation verbs.

• accusative : CaseMarking
• ablative : CaseMarking
• nominative : CaseMarking
• dative : CaseMarking

instance Phenomena.Case.Ozaki2026.Data.instDecidableEqCaseMarking : DecidableEq CaseMarking

Equations

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

instance Phenomena.Case.Ozaki2026.Data.instBEqCaseMarking : BEq CaseMarking

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqCaseMarking = { beq := Phenomena.Case.Ozaki2026.Data.instBEqCaseMarking.beq }

def Phenomena.Case.Ozaki2026.Data.instBEqCaseMarking.beq : CaseMarking → CaseMarking → Bool

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqCaseMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Ozaki2026.Data.instReprCaseMarking : Repr CaseMarking

Equations

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

def Phenomena.Case.Ozaki2026.Data.instReprCaseMarking.repr : CaseMarking → ℕ → Std.Format

Equations

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

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

Diagnostics for argumenthood (vs. adjuncthood).

• ellipsis : ArgumenthoodDiagnostic
• longDistanceScrambling : ArgumenthoodDiagnostic

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 ⋯

def Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDiagnostic.beq : ArgumenthoodDiagnostic → ArgumenthoodDiagnostic → Bool

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDiagnostic : BEq ArgumenthoodDiagnostic

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDiagnostic = { beq := Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDiagnostic.beq }

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

Equations

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

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

Equations

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

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

Diagnostics for unaccusativity.

• passivization : UnaccusativityDiagnostic
• naniOWhAdjunct : UnaccusativityDiagnostic

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 ⋯

def Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDiagnostic.beq : UnaccusativityDiagnostic → UnaccusativityDiagnostic → Bool

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDiagnostic : BEq UnaccusativityDiagnostic

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDiagnostic = { beq := Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDiagnostic.beq }

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

Equations

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

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

Equations

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

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
• sourceCase : CaseMarking
• grammatical : Bool
• sentence : String
• exampleNum : String

def Phenomena.Case.Ozaki2026.Data.instDecidableEqAlternationDatum.decEq (x✝ x✝¹ : AlternationDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Case.Ozaki2026.Data.instDecidableEqAlternationDatum : DecidableEq AlternationDatum

Equations

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

instance Phenomena.Case.Ozaki2026.Data.instBEqAlternationDatum : BEq AlternationDatum

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqAlternationDatum = { beq := Phenomena.Case.Ozaki2026.Data.instBEqAlternationDatum.beq }

def Phenomena.Case.Ozaki2026.Data.instBEqAlternationDatum.beq : AlternationDatum → AlternationDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Case.Ozaki2026.Data.instBEqAlternationDatum.beq x✝¹ x✝ = false

def Phenomena.Case.Ozaki2026.Data.instReprAlternationDatum.repr : AlternationDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Case.Ozaki2026.Data.instReprAlternationDatum : Repr AlternationDatum

Equations

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

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.

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

Equations

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

instance Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDatum : BEq UnaccusativityDatum

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDatum = { beq := Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDatum.beq }

def Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDatum.beq : UnaccusativityDatum → UnaccusativityDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Case.Ozaki2026.Data.instBEqUnaccusativityDatum.beq x✝¹ x✝ = false

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

Equations

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

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

Equations

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

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

An argumenthood diagnostic datum.

• verb : String
• sourceCase : CaseMarking
• diagnostic : ArgumenthoodDiagnostic
• grammatical : Bool
• sentence : String
• exampleNum : String

def Phenomena.Case.Ozaki2026.Data.instDecidableEqArgumenthoodDatum.decEq (x✝ x✝¹ : ArgumenthoodDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Case.Ozaki2026.Data.instDecidableEqArgumenthoodDatum : DecidableEq ArgumenthoodDatum

Equations

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

instance Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDatum : BEq ArgumenthoodDatum

Equations

• Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDatum = { beq := Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDatum.beq }

def Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDatum.beq : ArgumenthoodDatum → ArgumenthoodDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Case.Ozaki2026.Data.instBEqArgumenthoodDatum.beq x✝¹ x✝ = false

instance Phenomena.Case.Ozaki2026.Data.instReprArgumenthoodDatum : Repr ArgumenthoodDatum

Equations

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

def Phenomena.Case.Ozaki2026.Data.instReprArgumenthoodDatum.repr : ArgumenthoodDatum → ℕ → Std.Format

Equations

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

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

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

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

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

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

Equations

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

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.

theorem Phenomena.Case.Ozaki2026.Data.departure_no_external : Minimalism.voiceAnticausative.assignsTheta = false

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 : Minimalism.isInchoative (Minimalism.buildDecomposition Minimalism.voiceAnticausative [Minimalism.VerbHead.vCAUSE, Minimalism.VerbHead.vGO, Minimalism.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 : Minimalism.voiceAnticausative.assignsTheta = false

Non-thematic Voice assigns no θ-role.

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

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

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

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

theorem Phenomena.Case.Ozaki2026.Data.acc_source_from_configuration : Minimalism.getSourceOf "source" Minimalism.accVariantResult = some Minimalism.CaseSource.dependent

In the ACC variant, source case is dependent.

theorem Phenomena.Case.Ozaki2026.Data.abl_source_from_lexical_p : Minimalism.getSourceOf "source" Minimalism.ablVariantResult = some Minimalism.CaseSource.lexical

In the ABL variant, source case is lexical.

theorem Phenomena.Case.Ozaki2026.Data.agree_acc_needs_phase_head : Minimalism.voiceAnticausative.phaseHead = false

Anticausative Voice is not a phase head.

theorem Phenomena.Case.Ozaki2026.Data.agentive_has_phase_head : Minimalism.voiceAgent.phaseHead = true

Agentive Voice IS a phase head.

theorem Phenomena.Case.Ozaki2026.Data.accusative_unaccusative_paradox : Minimalism.voiceAnticausative.assignsTheta = false ∧ Minimalism.voiceAnticausative.phaseHead = false ∧ Minimalism.getCaseOf "source" Minimalism.accVariantResult = some Minimalism.CaseVal.acc ∧ Minimalism.getSourceOf "source" Minimalism.accVariantResult = some Minimalism.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 : Minimalism.voiceAnticausative.assignsTheta = false ∧ 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 ∧ Minimalism.voiceAnticausative.assignsTheta = false

Direct passive requires thematic Voice, which departure verbs lack.