Japanese Prosody Fragment

@cite{beckman-pierrehumbert-1986} @cite{kawahara-2015}

Japanese prosodic entries following the autosegmental-metrical analysis of @cite{beckman-pierrehumbert-1986}, with accent assignment rules and affix typology from @cite{kawahara-2015}.

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.

structure Fragments.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 Fragments.Japanese.Prosody.instReprJProsodicEntry : Repr JProsodicEntry

Equations

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

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

Equations

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

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

Is this entry accented?

Equations

• e.isAccented = e.accentMora.isSome

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

Convert to Bool accentedness for bridge to AccentualPhrase.

Equations

• e.accentedBool = e.isAccented

def Fragments.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

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

def Fragments.Japanese.Prosody.kami_paper : JProsodicEntry

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

Equations

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

def Fragments.Japanese.Prosody.umai : JProsodicEntry

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

Equations

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

def Fragments.Japanese.Prosody.amai : JProsodicEntry

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

Equations

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

def Fragments.Japanese.Prosody.mame : JProsodicEntry

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

Equations

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

def Fragments.Japanese.Prosody.ame : JProsodicEntry

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

Equations

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

structure Fragments.Japanese.Prosody.JLexicalEntryextends Fragments.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 Phenomena/Phonology/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 HasTokenFreq typeclass instance below makes this entry consumable by any module under Theories/Phonology/ItemSpecificity/.

• 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 Theories/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 @cite{breiss-katsuda-kawahara-2026}).

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Prosody.instReprJLexicalEntry : Repr JLexicalEntry

Equations

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

@[implicit_reducible]

noncomputable instance Fragments.Japanese.Prosody.instHasTokenFreqJLexicalEntry : Phonology.ItemSpecificity.HasTokenFreq JLexicalEntry

HasTokenFreq instance routing tokenLogFreq through the fragment-level ℚ field into the abstract LogFreq := ℝ interface used by Theories/Phonology/ItemSpecificity/. Rat.cast is the standard mathlib coercion. The instance is noncomputable because ℝ is noncomputable; the ℚ field itself remains computable for decide-style proofs.

Equations

• Fragments.Japanese.Prosody.instHasTokenFreqJLexicalEntry = { tokenLogFreq := fun (e : Fragments.Japanese.Prosody.JLexicalEntry) => ↑e.tokenLogFreq }

structure Fragments.Japanese.Prosody.JCompound : Type

A Japanese N1 + N2 nominal compound. Compound-medial position is the locus of voiced velar nasalisation (/g/ → [ŋ]) studied in @cite{breiss-katsuda-kawahara-2026}: 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 Fragments.Japanese.Prosody.instReprJCompound : Repr JCompound

Equations

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

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

Equations

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

def Fragments.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 Fragments.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 @cite{breiss-katsuda-kawahara-2026}.

Equations

• c.nasalisationObligatory = !c.n2.canStandAlone

structure Fragments.Japanese.Prosody.JAccentualPhrase : Type

Japanese accentual phrase tonal specification.

@cite{beckman-pierrehumbert-1986} §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 Fragments.Japanese.Prosody.instReprJAccentualPhrase : Repr JAccentualPhrase

Equations

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

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

Equations

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

def Fragments.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 : Fragments.Japanese.Prosody.JProsodicEntry) => x.isAccented

def Fragments.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 Fragments.Japanese.Prosody.kami_god_accented : kami_god.isAccented = true

Accented words have accent location.

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

Unaccented words lack accent location.

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

Japanese accent is lexical.

theorem Fragments.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 Fragments.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 Fragments.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 Fragments.Japanese.Prosody.unaccented_ap : { words := [kami_paper, mame] }.isAccented = false

An AP containing only unaccented words is unaccented.

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

An AP containing an accented word is accented.

structure Fragments.Japanese.Prosody.JSuffixAccent : Type

Japanese suffix accent specification.

Japanese suffixes exhibit the same dominant/recessive distinction as IE accent systems (@cite{kiparsky-halle-1977}) and GT systems (@cite{rolle-2018}). Dominant suffixes remove stem accent; recessive suffixes preserve it when present.

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Prosody.instReprJSuffixAccent : Repr JSuffixAccent

Equations

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

def Fragments.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 (@cite{kawahara-2015}).

Equations

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

def Fragments.Japanese.Prosody.si_suffix : JSuffixAccent

-si (氏): non-deaccenting suffix. Preserves stem accent when present — classified as recessive (@cite{kawahara-2015}).

Equations

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

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

Deaccenting suffixes are dominant.

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

Non-deaccenting suffixes are not dominant.

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

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

Equations

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

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

-teki deaccents kami 'god' (accented).

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

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

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

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

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

-si preserves the accent on kami 'god'.

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

-si preserves the unaccentedness of kami 'paper'.

theorem Fragments.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 Fragments.Japanese.Prosody.JLoanwordEntry : Type

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

• entry : JProsodicEntry
• weights : List Phonology.Syllable.SyllWeight

  Syllable weight profile (left to right)

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Prosody.instReprJLoanwordEntry : Repr JLoanwordEntry

Equations

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

def Fragments.Japanese.Prosody.kurisumasu : JLoanwordEntry

kurisumasu 'Christmas' — accent on antepenultimate mora (su). @cite{kawahara-2015} (10a).

Equations

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

def Fragments.Japanese.Prosody.asufaruto : JLoanwordEntry

asufaruto 'asphalt' — accent on antepenultimate mora (fa). @cite{kawahara-2015} (10g).

Equations

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

def Fragments.Japanese.Prosody.makudonarudo : JLoanwordEntry

makudonarudo 'McDonald' — accent on antepenultimate mora (na). @cite{kawahara-2015} (10h).

Equations

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

def Fragments.Japanese.Prosody.amerika : JLoanwordEntry

amerika 'America' — unaccented (4-mora with two final light σ). @cite{kawahara-2015} (16a).

Equations

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

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

Loanword accent matches AAR prediction for all-light syllables.

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

Loanword accent matches LSR prediction for all-light syllables.

theorem Fragments.Japanese.Prosody.aar_lsr_mismatch_hlh : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy] = some 1 ∧ Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy] = some 0

HLH: AAR predicts penultimate (σ₂), LSR predicts antepenultimate (σ₁). @cite{kawahara-2015} Table 1, row (c).

theorem Fragments.Japanese.Prosody.aar_lsr_mismatch_llh : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy] = some 1 ∧ Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy] = some 0

LLH: AAR predicts penultimate (σ₂), LSR predicts antepenultimate (σ₁). @cite{kawahara-2015} Table 1, row (g).

theorem Fragments.Japanese.Prosody.aar_lsr_match_hhh : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy] = Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy]

The remaining 6 conditions in Table 1 produce matching predictions.

theorem Fragments.Japanese.Prosody.aar_lsr_match_hhl : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light] = Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light]

theorem Fragments.Japanese.Prosody.aar_lsr_match_hll : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light] = Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light]

theorem Fragments.Japanese.Prosody.aar_lsr_match_lhh : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy] = Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.heavy]

theorem Fragments.Japanese.Prosody.aar_lsr_match_lhl : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light] = Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.heavy, Phonology.Syllable.SyllWeight.light]

theorem Fragments.Japanese.Prosody.aar_lsr_match_lll : Phonology.Accent.defaultAccentAAR [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light] = Phonology.Accent.latinStressRule [Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light, Phonology.Syllable.SyllWeight.light]

structure Fragments.Japanese.Prosody.JAffixEntry : Type

Japanese suffix with fine-grained accent classification.

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Prosody.instReprJAffixEntry : Repr JAffixEntry

Equations

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

def Fragments.Japanese.Prosody.tara_suffix : JAffixEntry

-tara (conditional): recessive suffix — bears accent, loses to root. @cite{kawahara-2015} (29).

Equations

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

def Fragments.Japanese.Prosody.ppoi_suffix : JAffixEntry

-ppoi (-ish): dominant suffix — bears accent, overrides root. @cite{kawahara-2015} (30).

Equations

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

def Fragments.Japanese.Prosody.si_affix : JAffixEntry

-si (Mr.): recessive pre-accenting — inserts accent on root-final σ when root is unaccented, preserves root accent when present. @cite{kawahara-2015} (31).

Equations

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

def Fragments.Japanese.Prosody.ke_suffix : JAffixEntry

-ke (family of): dominant pre-accenting — always inserts accent on root-final σ, deleting any root accent. @cite{kawahara-2015} (32).

Equations

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

def Fragments.Japanese.Prosody.mono_suffix : JAffixEntry

-mono (thing): accent-shifting — shifts existing root accent to pre-suffix position. Unaccented roots stay unaccented. @cite{kawahara-2015} (33).

Equations

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

def Fragments.Japanese.Prosody.o_prefix : JAffixEntry

o- (honorific prefix): post-accenting — inserts accent after prefix. @cite{kawahara-2015} (34).

Equations

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

def Fragments.Japanese.Prosody.teki_affix : JAffixEntry

-teki (的 -like): deaccenting — deletes root accent, no new accent. @cite{kawahara-2015} (36).

Equations

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

def Fragments.Japanese.Prosody.zu_suffix : JAffixEntry

-zu (group/plural): initial-accenting — inserts accent on root-initial σ. @cite{kawahara-2015} (39).

Equations

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

theorem Fragments.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 Fragments.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 Fragments.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 Fragments.Japanese.Prosody.kabuto_musi_compound : Phonology.Accent.shortN2CompoundAccent 3 (some 0) true = some 2

kabuto+musi 'beetle': short N2 (musi, 2μ) pre-accents on N1-final syllable. @cite{kawahara-2015} (22a).

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

sin+yokohama 'Shin-Yokohama': long N2 (yokohama, 4μ, unaccented) → accent on N2-initial syllable. @cite{kawahara-2015} (23a).

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

sin+tamane'gi 'new onion': long N2 retains accent. @cite{kawahara-2015} (24a).

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

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

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

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