Japanese Prosody Fragment

[BP86] [Kaw15]

Japanese prosodic entries following the autosegmental-metrical analysis of [BP86], with accent assignment rules and affix typology from [Kaw15].

Key Properties

• Lexical accent: accent location specified in the lexicon as a linked H tone. The accent shape is fixed (H*+L); only the location varies.
• Accented vs unaccented: some words are lexically unaccented (e.g., compound nouns formed from unaccented words). Unaccented words can form well-formed utterances without any pitch accent.
• Accentual phrase: delimited by a phrasal H (on the second sonorant mora) and a boundary L. Contains at most one accent.
• Sparse tonal specification: only the accent H, the phrasal H, and the boundary L are specified; F0 between them is interpolated.
• Culminativity: at most one HL fall per prosodic word — Japanese is a pitch-accent language, not a tone language.
• Default accent: loanwords and nonce words receive antepenultimate accent (AAR) or Latin Stress Rule (LSR) accent.
• Eight affix accent types: recessive, dominant, recessive pre-accenting, dominant pre-accenting, accent-shifting, post-accenting, deaccenting, initial-accenting.

Default-accent rules (formerly Phonology/Prosody/Accent)

Language-neutral accent-placement rules over a syllable-weight profile, used in the Japanese accent analysis below ([McC68]; [Hay95a]; [Kub06]; [PS93]).

def Japanese.Prosody.defaultAccentAAR (weights : List Prosody.Syllable.Weight) : Option ℕ

The Antepenultimate Accent Rule ([McC68]): accent the syllable containing the antepenultimate (3rd-from-last) mora; words with fewer than three morae accent the initial syllable. Returns the 0-indexed syllable.

Equations

• One or more equations did not get rendered due to their size.
• Japanese.Prosody.defaultAccentAAR [] = none

@[irreducible]

def Japanese.Prosody.latinStressRule : List Prosody.Syllable.Weight → Option ℕ

The Latin Stress Rule ([Hay95a]): accent the penult if heavy (≥ 2μ), else the antepenult. Monosyllables accent the only syllable; disyllables the penult (= initial). [Kub06] argues it fits Japanese default accentuation better than defaultAccentAAR.

Equations

• Japanese.Prosody.latinStressRule [] = none
• Japanese.Prosody.latinStressRule [head] = some 0
• Japanese.Prosody.latinStressRule [head, head_1] = some 0
• Japanese.Prosody.latinStressRule [head, 0, head_1] = some 0
• Japanese.Prosody.latinStressRule [head, 1, head_1] = some 0
• Japanese.Prosody.latinStressRule [head, head_1, head_2] = some 1
• Japanese.Prosody.latinStressRule (head :: head_1 :: head_2 :: tail) = Option.map (fun (x : ℕ) => x + 1) (Japanese.Prosody.latinStressRule (head_1 :: head_2 :: tail))

def Japanese.Prosody.nonFinalitySigma (accentSyll : Option ℕ) (nSyll : ℕ) : ℕ

NonFinality(σ) ([PS93]): 1 if accent is on the word-final syllable, else 0 — drives the avoidance of final accent in Japanese compounds and loanwords ([Kaw15]).

Equations

• Japanese.Prosody.nonFinalitySigma (some pos) nSyll = if (pos + 1 == nSyll) = true then 1 else 0
• Japanese.Prosody.nonFinalitySigma none nSyll = 0

Accent-to-tone derivation and compound accent (Japanese-specific)

The Japanese pitch-accent tonal melody and the compound-accent rules ([Kaw15]) — the accentual HL + initial rise and the N1/N2 compound rules, which build on the default-accent placement above.

inductive Japanese.Prosody.LevelTone : Type

A level tone for pitch-accent systems. Japanese uses only H (high) and L (low) at the lexical level ([Kaw15]).

• H : LevelTone
• L : LevelTone

@[implicit_reducible]

instance Japanese.Prosody.instDecidableEqLevelTone : DecidableEq LevelTone

Equations

• Japanese.Prosody.instDecidableEqLevelTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Japanese.Prosody.instReprLevelTone.repr : LevelTone → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Japanese.Prosody.instReprLevelTone : Repr LevelTone

Equations

• Japanese.Prosody.instReprLevelTone = { reprPrec := Japanese.Prosody.instReprLevelTone.repr }

def Japanese.Prosody.instBEqLevelTone.beq : LevelTone → LevelTone → Bool

Equations

• Japanese.Prosody.instBEqLevelTone.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Japanese.Prosody.instBEqLevelTone : BEq LevelTone

Equations

• Japanese.Prosody.instBEqLevelTone = { beq := Japanese.Prosody.instBEqLevelTone.beq }

def Japanese.Prosody.accentToTones (accentMora : Option ℕ) (nMorae : ℕ) : List LevelTone

Derive the surface tone of each mora from accent position and mora count ([Kaw15]), returning one LevelTone per mora:

1. accentual HL — H on the accented mora, L on the next;
2. initial rise — L on mora 0, H on mora 1 (blocked by initial accent);
3. spreading — unspecified moras copy the rightmost specified tone.

Equations

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

def Japanese.Prosody.accentToTones.spread : List (Option LevelTone) → LevelTone → List LevelTone

Equations

• Japanese.Prosody.accentToTones.spread [] a✝ = []
• Japanese.Prosody.accentToTones.spread (some t :: rest) a✝ = t :: Japanese.Prosody.accentToTones.spread rest t
• Japanese.Prosody.accentToTones.spread (none :: rest) a✝ = a✝ :: Japanese.Prosody.accentToTones.spread rest a✝

def Japanese.Prosody.shortN2CompoundAccent (n1Morae : ℕ) (n2Accent : Option ℕ) (preAccenting : Bool) : Option ℕ

Short-N2 compound accent ([Kaw15]): when the second member N2 is short (≤ 2μ), accent may pre-accent the last syllable of N1, or N2 retains its own accent. Pre-accenting N2s lose their accent to NonFinality(Ft) and receive a new one, like dominant pre-accenting suffixes.

Equations

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

def Japanese.Prosody.longN2CompoundAccent (n1Morae : ℕ) (n2Accent : Option ℕ) (n2Morae : ℕ) : Option ℕ

Long-N2 compound accent ([Kaw15]): when N2 is long (≥ 3μ), an unaccented or final-accented N2 accents its initial syllable; otherwise N2's own accent is retained.

Equations

• Japanese.Prosody.longN2CompoundAccent n1Morae none n2Morae = some n1Morae
• Japanese.Prosody.longN2CompoundAccent n1Morae (some pos) n2Morae = if (pos + 1 == n2Morae) = true then some n1Morae else some (pos + n1Morae)

structure Japanese.Prosody.JProsodicEntry : Type

A Japanese lexical entry with prosodic specification.

The accent is specified as the mora position of the linked H tone (0-indexed from the beginning of the word). Unaccented words have accentMora = none.

• form : String

  Surface form (romanized)

• gloss : String

  Gloss

• accentMora : Option ℕ

  Mora position of the accent (none = unaccented)

• nMorae : ℕ

  Number of morae in the word

@[implicit_reducible]

instance Japanese.Prosody.instReprJProsodicEntry : Repr JProsodicEntry

Equations

• Japanese.Prosody.instReprJProsodicEntry = { reprPrec := Japanese.Prosody.instReprJProsodicEntry.repr }

def Japanese.Prosody.instReprJProsodicEntry.repr : JProsodicEntry → ℕ → Std.Format

Equations

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

def Japanese.Prosody.JProsodicEntry.isAccented (e : JProsodicEntry) : Bool

Is this entry accented?

Equations

• e.isAccented = e.accentMora.isSome

def Japanese.Prosody.JProsodicEntry.accentedBool (e : JProsodicEntry) : Bool

Convert to Bool accentedness for bridge to AccentualPhrase.

Equations

• e.accentedBool = e.isAccented

def Japanese.Prosody.kami_god : JProsodicEntry

kami 'god' — accented on first mora (initial accent). Contrasts with kami 'paper' (unaccented) and kamí 'hair' (accent on second mora).

Equations

• Japanese.Prosody.kami_god = { form := "kami", gloss := "god", accentMora := some 0, nMorae := 2 }

def Japanese.Prosody.kami_paper : JProsodicEntry

kami 'paper' — unaccented. No HL fall in the accentual phrase.

Equations

• Japanese.Prosody.kami_paper = { form := "kami", gloss := "paper", accentMora := none, nMorae := 2 }

def Japanese.Prosody.umai : JProsodicEntry

uma'i — accented adjective (§2.2, Figs. 6, 8, 9).

Equations

• Japanese.Prosody.umai = { form := "umai", gloss := "delicious", accentMora := some 1, nMorae := 3 }

def Japanese.Prosody.amai : JProsodicEntry

amai — accented adjective (§2.3, Fig. 8).

Equations

• Japanese.Prosody.amai = { form := "amai", gloss := "sweet", accentMora := some 1, nMorae := 3 }

def Japanese.Prosody.mame : JProsodicEntry

mame — unaccented noun (§2.2, Fig. 6).

Equations

• Japanese.Prosody.mame = { form := "mame", gloss := "beans", accentMora := none, nMorae := 2 }

def Japanese.Prosody.ame : JProsodicEntry

ame — unaccented noun (§2.2, Fig. 6).

Equations

• Japanese.Prosody.ame = { form := "ame", gloss := "rain", accentMora := none, nMorae := 2 }

structure Japanese.Prosody.JLexicalEntryextends Japanese.Prosody.JProsodicEntry : Type

A Japanese lexical entry extending JProsodicEntry with the two annotations needed for frequency-conditioned phonology (e.g., the Breiss-Katsuda-Kawahara compounds in Studies/BreissKatsudaKawahara2026.lean): a corpus token log-frequency and a free/bound flag.

Following CLAUDE.md's "infrastructure on demand", these annotations are kept on a thin extension structure rather than added to JProsodicEntry, so existing accent-only consumers are unaffected. The jTokenFreq accessor below exposes its token frequency as the ℝ-valued channel that frequency-conditioned phonology reads.

• form : String
• gloss : String
• accentMora : Option ℕ
• nMorae : ℕ
• tokenLogFreq : ℚ

  Token log-frequency in a reference corpus (e.g., BCCWJ). 0 conventionally means "log of 1 occurrence" — used as the no-info default for unannotated items. Stored as ℚ so that the lexicon remains computable while the abstract Phonology/ interface coerces to ℝ.

• canStandAlone : Bool

  Can this morpheme stand alone as a wordform? false for bound stems that occur only in compounds (e.g., the bound N2s targeted in [BKK26]).

@[implicit_reducible]

instance Japanese.Prosody.instReprJLexicalEntry : Repr JLexicalEntry

Equations

• Japanese.Prosody.instReprJLexicalEntry = { reprPrec := Japanese.Prosody.instReprJLexicalEntry.repr }

def Japanese.Prosody.instReprJLexicalEntry.repr : JLexicalEntry → ℕ → Std.Format

Equations

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

noncomputable def Japanese.Prosody.jTokenFreq (e : JLexicalEntry) : ℝ

The token-log-frequency of a JLexicalEntry: the fragment-level ℚ field cast to ℝ for frequency-conditioned phonology. noncomputable because ℝ is; the ℚ field itself stays computable for decide-style proofs.

Equations

• Japanese.Prosody.jTokenFreq e = ↑e.tokenLogFreq

structure Japanese.Prosody.JCompound : Type

A Japanese N1 + N2 nominal compound. Compound-medial position is the locus of voiced velar nasalisation (/g/ → [ŋ]) studied in [BKK26]: obligatory when N2 is bound, optional and frequency-conditioned when N2 is free.

The compound's own tokenLogFreq is independent of N1's and N2's — high-frequency compounds with low-frequency components, and vice versa, both occur. Frequency-conditioned theories that treat the compound's frequency as inherited from constituents (e.g., some RepresentationStrength variants with multiplicative inheritance) must reconcile this independence with empirical reality.

• n1 : JLexicalEntry
• n2 : JLexicalEntry
• compoundLogFreq : ℚ

  Token log-frequency of the compound as a unit — typically much lower than either constituent in isolation, but the principal conditioning variable on optional nasalisation.

@[implicit_reducible]

instance Japanese.Prosody.instReprJCompound : Repr JCompound

Equations

• Japanese.Prosody.instReprJCompound = { reprPrec := Japanese.Prosody.instReprJCompound.repr }

def Japanese.Prosody.instReprJCompound.repr : JCompound → ℕ → Std.Format

Equations

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

def Japanese.Prosody.JCompound.form (c : JCompound) : String

The compound's surface form: simple concatenation of N1 and N2 forms (the segmental alternation /g/→[ŋ] applies on top).

Equations

• c.form = c.n1.form ++ c.n2.form

def Japanese.Prosody.JCompound.nasalisationObligatory (c : JCompound) : Bool

A compound's nasalisation is obligatory iff its N2 is bound. The free-N2 case is the gradient one tested in [BKK26].

Equations

• c.nasalisationObligatory = !c.n2.canStandAlone

structure Japanese.Prosody.JAccentualPhrase : Type

Japanese accentual phrase tonal specification.

[BP86] §2.2: the AP is defined by:

• A boundary L at the beginning (or end of preceding AP)
• A phrasal H on the second sonorant mora
• An optional accent HL (if the word is accented)
• A boundary L at the end

The phrasal H is NOT the same as H-tone spreading from the accent; it has its own local pitch range and is always present, even in unaccented phrases (Fig. 3 vs earlier accounts).

• words : List JProsodicEntry

  Words grouped in this AP

• hasPhrasalH : Bool

  Whether the phrasal H is present (always true in Japanese)

@[implicit_reducible]

instance Japanese.Prosody.instReprJAccentualPhrase : Repr JAccentualPhrase

Equations

• Japanese.Prosody.instReprJAccentualPhrase = { reprPrec := Japanese.Prosody.instReprJAccentualPhrase.repr }

def Japanese.Prosody.instReprJAccentualPhrase.repr : JAccentualPhrase → ℕ → Std.Format

Equations

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

def Japanese.Prosody.JAccentualPhrase.isAccented (ap : JAccentualPhrase) : Bool

An AP is accented if any word in it is accented.

Equations

• ap.isAccented = ap.words.any fun (x : Japanese.Prosody.JProsodicEntry) => x.isAccented

def Japanese.Prosody.JAccentualPhrase.toGeneric (ap : JAccentualPhrase) : BeckmanPierrehumbert1986.AccentualPhrase

Convert to the generic AccentualPhrase type. Japanese accent shape is always H*+L; unaccented APs get null.

Equations

• ap.toGeneric = { accent := if ap.isAccented = true then Features.Prosody.PitchAccent.H_star_plus_L else Features.Prosody.PitchAccent.null, nWords := ap.words.length }

theorem Japanese.Prosody.kami_god_accented : kami_god.isAccented = true

Accented words have accent location.

theorem Japanese.Prosody.kami_paper_unaccented : kami_paper.isAccented = false

Unaccented words lack accent location.

theorem Japanese.Prosody.japanese_accent_is_lexical : BeckmanPierrehumbert1986.japanese.accentSpec = Features.Prosody.AccentSpecification.lexical

Japanese accent is lexical.

theorem Japanese.Prosody.japanese_accent_is_bitonal : Features.Prosody.PitchAccent.H_star_plus_L.isBitonal = true

The Japanese pitch accent shape is H*+L (a single bitonal accent).

theorem Japanese.Prosody.japanese_accented_ap_triggers_catathesis (ap : JAccentualPhrase) (h : ap.isAccented = true) : ap.toGeneric.accent.isBitonal = true

A Japanese accented AP always triggers catathesis (because H*+L is bitonal).

theorem Japanese.Prosody.japanese_unaccented_ap_no_catathesis (ap : JAccentualPhrase) (h : ap.isAccented = false) : ap.toGeneric.accent.isBitonal = false

A Japanese unaccented AP never triggers catathesis.

theorem Japanese.Prosody.unaccented_ap : { words := [kami_paper, mame] }.isAccented = false

An AP containing only unaccented words is unaccented.

theorem Japanese.Prosody.accented_ap : { words := [kami_god, mame] }.isAccented = true

An AP containing an accented word is accented.

structure Japanese.Prosody.JSuffixAccent : Type

Japanese suffix accent specification.

Japanese suffixes exhibit the same dominant/recessive distinction as IE accent systems ([KH77]) and GT systems ([Rol18]). Dominant suffixes remove stem accent; recessive suffixes preserve it when present.

• form : String
• gloss : String
• dominance : Features.Prosody.ProsodicDominance

@[implicit_reducible]

instance Japanese.Prosody.instReprJSuffixAccent : Repr JSuffixAccent

Equations

• Japanese.Prosody.instReprJSuffixAccent = { reprPrec := Japanese.Prosody.instReprJSuffixAccent.repr }

def Japanese.Prosody.instReprJSuffixAccent.repr : JSuffixAccent → ℕ → Std.Format

Equations

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

def Japanese.Prosody.teki_suffix : JSuffixAccent

-teki (的): deaccenting suffix. Removes stem accent regardless of whether the stem is accented or unaccented — classified as subtractive-dominant in GT terms ([Kaw15]).

Equations

• Japanese.Prosody.teki_suffix = { form := "-teki", gloss := "的 ADJ", dominance := Features.Prosody.ProsodicDominance.dominant }

def Japanese.Prosody.si_suffix : JSuffixAccent

-si (氏): non-deaccenting suffix. Preserves stem accent when present — classified as recessive ([Kaw15]).

Equations

• Japanese.Prosody.si_suffix = { form := "-si", gloss := "氏 Mr.", dominance := Features.Prosody.ProsodicDominance.recessive }

theorem Japanese.Prosody.teki_is_dominant : teki_suffix.dominance.IsDominant

Deaccenting suffixes are dominant.

theorem Japanese.Prosody.si_is_not_dominant : ¬si_suffix.dominance.IsDominant

Non-deaccenting suffixes are not dominant.

def Japanese.Prosody.suffixedAccent (stem : JProsodicEntry) (suffix : JSuffixAccent) : Option ℕ

Derive the accent of a suffixed word from stem accent + suffix dominance.

Equations

• Japanese.Prosody.suffixedAccent stem suffix = Features.Prosody.ProsodicDominance.combineAccent stem.accentMora suffix.dominance

theorem Japanese.Prosody.teki_deaccents_kami_god : suffixedAccent kami_god teki_suffix = none

-teki deaccents kami 'god' (accented).

theorem Japanese.Prosody.teki_leaves_kami_paper : suffixedAccent kami_paper teki_suffix = none

-teki leaves kami 'paper' (unaccented) unchanged.

theorem Japanese.Prosody.teki_neutralizes_kami : suffixedAccent kami_god teki_suffix = suffixedAccent kami_paper teki_suffix

-teki neutralizes the kami 'god' / kami 'paper' contrast.

theorem Japanese.Prosody.si_preserves_kami_god : suffixedAccent kami_god si_suffix = some 0

-si preserves the accent on kami 'god'.

theorem Japanese.Prosody.si_preserves_kami_paper : suffixedAccent kami_paper si_suffix = none

-si preserves the unaccentedness of kami 'paper'.

theorem Japanese.Prosody.si_maintains_kami_contrast : suffixedAccent kami_god si_suffix ≠ suffixedAccent kami_paper si_suffix

-si maintains the kami 'god' / kami 'paper' contrast.

structure Japanese.Prosody.JLoanwordEntry : Type

Loanword prosodic entry. Extends JProsodicEntry with syllable weight profile for testing AAR vs LSR predictions.

• entry : JProsodicEntry
• weights : List Prosody.Syllable.Weight

  Syllable weight profile (left to right)

@[implicit_reducible]

instance Japanese.Prosody.instReprJLoanwordEntry : Repr JLoanwordEntry

Equations

• Japanese.Prosody.instReprJLoanwordEntry = { reprPrec := Japanese.Prosody.instReprJLoanwordEntry.repr }

def Japanese.Prosody.instReprJLoanwordEntry.repr : JLoanwordEntry → ℕ → Std.Format

Equations

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

def Japanese.Prosody.kurisumasu : JLoanwordEntry

kurisumasu 'Christmas' — accent on antepenultimate mora (su). [Kaw15] (10a).

Equations

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

def Japanese.Prosody.asufaruto : JLoanwordEntry

asufaruto 'asphalt' — accent on antepenultimate mora (fa). [Kaw15] (10g).

Equations

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

def Japanese.Prosody.makudonarudo : JLoanwordEntry

makudonarudo 'McDonald' — accent on antepenultimate mora (na). [Kaw15] (10h).

Equations

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

def Japanese.Prosody.amerika : JLoanwordEntry

amerika 'America' — unaccented (4-mora with two final light σ). [Kaw15] (16a).

Equations

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

theorem Japanese.Prosody.kurisumasu_matches_aar : defaultAccentAAR kurisumasu.weights = kurisumasu.entry.accentMora

Loanword accent matches AAR prediction for all-light syllables.

theorem Japanese.Prosody.kurisumasu_matches_lsr : latinStressRule kurisumasu.weights = kurisumasu.entry.accentMora

Loanword accent matches LSR prediction for all-light syllables.

theorem Japanese.Prosody.aar_lsr_mismatch_hlh : defaultAccentAAR [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 1 ∧ latinStressRule [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 0

HLH: AAR predicts penultimate (σ₂), LSR predicts antepenultimate (σ₁). [Kaw15] Table 1, row (c).

theorem Japanese.Prosody.aar_lsr_mismatch_llh : defaultAccentAAR [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 1 ∧ latinStressRule [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy] = some 0

LLH: AAR predicts penultimate (σ₂), LSR predicts antepenultimate (σ₁). [Kaw15] Table 1, row (g).

theorem Japanese.Prosody.aar_lsr_match_hhh : defaultAccentAAR [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy] = latinStressRule [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy]

The remaining 6 conditions in Table 1 produce matching predictions.

theorem Japanese.Prosody.aar_lsr_match_hhl : defaultAccentAAR [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light] = latinStressRule [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light]

theorem Japanese.Prosody.aar_lsr_match_hll : defaultAccentAAR [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light] = latinStressRule [Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light]

theorem Japanese.Prosody.aar_lsr_match_lhh : defaultAccentAAR [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy] = latinStressRule [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.heavy]

theorem Japanese.Prosody.aar_lsr_match_lhl : defaultAccentAAR [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light] = latinStressRule [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.heavy, Prosody.Syllable.Weight.light]

theorem Japanese.Prosody.aar_lsr_match_lll : defaultAccentAAR [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light] = latinStressRule [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light]

structure Japanese.Prosody.JAffixEntry : Type

Japanese suffix with fine-grained accent classification.

• form : String
• gloss : String
• accentType : Features.Prosody.AffixAccentType

@[implicit_reducible]

instance Japanese.Prosody.instReprJAffixEntry : Repr JAffixEntry

Equations

• Japanese.Prosody.instReprJAffixEntry = { reprPrec := Japanese.Prosody.instReprJAffixEntry.repr }

def Japanese.Prosody.instReprJAffixEntry.repr : JAffixEntry → ℕ → Std.Format

Equations

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

def Japanese.Prosody.tara_suffix : JAffixEntry

-tara (conditional): recessive suffix — bears accent, loses to root. [Kaw15] (29).

Equations

• Japanese.Prosody.tara_suffix = { form := "-tara", gloss := "conditional", accentType := Features.Prosody.AffixAccentType.recessive }

def Japanese.Prosody.ppoi_suffix : JAffixEntry

-ppoi (-ish): dominant suffix — bears accent, overrides root. [Kaw15] (30).

Equations

• Japanese.Prosody.ppoi_suffix = { form := "-ppoi", gloss := "-ish", accentType := Features.Prosody.AffixAccentType.dominant }

def Japanese.Prosody.si_affix : JAffixEntry

-si (Mr.): recessive pre-accenting — inserts accent on root-final σ when root is unaccented, preserves root accent when present. [Kaw15] (31).

Equations

• Japanese.Prosody.si_affix = { form := "-si", gloss := "Mr.", accentType := Features.Prosody.AffixAccentType.recessivePreAccent }

def Japanese.Prosody.ke_suffix : JAffixEntry

-ke (family of): dominant pre-accenting — always inserts accent on root-final σ, deleting any root accent. [Kaw15] (32).

Equations

• Japanese.Prosody.ke_suffix = { form := "-ke", gloss := "family of", accentType := Features.Prosody.AffixAccentType.dominantPreAccent }

def Japanese.Prosody.mono_suffix : JAffixEntry

-mono (thing): accent-shifting — shifts existing root accent to pre-suffix position. Unaccented roots stay unaccented. [Kaw15] (33).

Equations

• Japanese.Prosody.mono_suffix = { form := "-mono", gloss := "thing", accentType := Features.Prosody.AffixAccentType.accentShifting }

def Japanese.Prosody.o_prefix : JAffixEntry

o- (honorific prefix): post-accenting — inserts accent after prefix. [Kaw15] (34).

Equations

• Japanese.Prosody.o_prefix = { form := "o-", gloss := "honorific", accentType := Features.Prosody.AffixAccentType.postAccenting }

def Japanese.Prosody.teki_affix : JAffixEntry

-teki (的 -like): deaccenting — deletes root accent, no new accent. [Kaw15] (36).

Equations

• Japanese.Prosody.teki_affix = { form := "-teki", gloss := "的 -like", accentType := Features.Prosody.AffixAccentType.deaccenting }

def Japanese.Prosody.zu_suffix : JAffixEntry

-zu (group/plural): initial-accenting — inserts accent on root-initial σ. [Kaw15] (39).

Equations

• Japanese.Prosody.zu_suffix = { form := "-zu", gloss := "group", accentType := Features.Prosody.AffixAccentType.initialAccenting }

theorem Japanese.Prosody.si_is_recessive_coarse : si_affix.accentType.toProsodicDominance = Features.Prosody.ProsodicDominance.recessive

Recessive pre-accenting is recessive at the coarse level (preserves root accent when present).

theorem Japanese.Prosody.teki_is_dominant_coarse : teki_affix.accentType.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant

Deaccenting is dominant at the coarse level (overrides root accent). This corrects the earlier classification of -teki in this fragment, which used ProsodicDominance.dominant — functionally the same projection, but the fine-grained type makes the behavior explicit.

theorem Japanese.Prosody.mono_is_recessive_coarse : mono_suffix.accentType.toProsodicDominance = Features.Prosody.ProsodicDominance.recessive

Accent-shifting is recessive at the coarse level: it only operates on accent that is already present, never creating new accent.

theorem Japanese.Prosody.kabuto_musi_compound : shortN2CompoundAccent 3 (some 0) true = some 2

kabuto+musi 'beetle': short N2 (musi, 2μ) pre-accents on N1-final syllable. [Kaw15] (22a).

theorem Japanese.Prosody.sin_yokohama_compound : longN2CompoundAccent 2 none 4 = some 2

sin+yokohama 'Shin-Yokohama': long N2 (yokohama, 4μ, unaccented) → accent on N2-initial syllable. [Kaw15] (23a).

theorem Japanese.Prosody.sin_tamanegi_compound : longN2CompoundAccent 2 (some 2) 4 = some 4

sin+tamane'gi 'new onion': long N2 retains accent. [Kaw15] (24a).

theorem Japanese.Prosody.ame_ga_tones : accentToTones ame.accentMora 3 = [LevelTone.L, LevelTone.H, LevelTone.H]

Unaccented trisyllable ame+ga → LHH (initial rise + H spread).

theorem Japanese.Prosody.kami_god_ga_tones : accentToTones kami_god.accentMora 3 = [LevelTone.H, LevelTone.L, LevelTone.L]

Accented ka'mi+ga → HLL (accent HL + L spread).