Benz (2025): Structure and Interpretation Across Categories

@cite{benz-2025}

Structure and Interpretation Across Categories. PhD dissertation, University of Pennsylvania.

Overview

This file formalizes three interconnected contributions from @cite{benz-2025}:

1. Content nominalizations (Ch. 3): German -ung nominalizations are systematically three-ways ambiguous (event/result/content), derived from allosemy of v and n in the structure [nP n [vP v [√Root]]].

2. Co-occurrence restrictions (Ch. 4): German preverbal elements (prefixes, particles, RSPs) show a striking co-occurrence paradigm explained by the conjunction of phrase-structural and interpretive constraints.

3. Allosemy and locality (Ch. 2, Ch. 4): RSPs are always interpreted transparently (outside v's locality domain), while prefixes and particles can receive non-transparent interpretations (inside v's complex head).

Architecture

• Theories.Morphology.DM.Allosemy: general framework + v/n/Voice allosemy
• Core.Empirical: Acceptability type

structure Phenomena.Morphology.Studies.Benz2025.NominalizationDatum : Type

A German nominalization datum with reading and diagnostic properties.

• form : String

  The nominalized form.

• baseVerb : String

  Base verb.

• suffix : String

  Nominalizing suffix.

• reading : Morphology.DM.Allosemy.NominalizationReading

  The reading exhibited in this example.

• sentence : String

  Example sentence.

• translation : String

  Translation.

• temporalModifiers : Bool

  Accepts temporal modifiers?

• pluralizable : Bool

  Can be pluralized?

• takesCPComplement : Bool

  Takes CP complement?

instance Phenomena.Morphology.Studies.Benz2025.instReprNominalizationDatum : Repr NominalizationDatum

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprNominalizationDatum = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprNominalizationDatum.repr }

def Phenomena.Morphology.Studies.Benz2025.instReprNominalizationDatum.repr : NominalizationDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationDatum : BEq NominalizationDatum

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationDatum = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationDatum.beq }

def Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationDatum.beq : NominalizationDatum → NominalizationDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationDatum.beq x✝¹ x✝ = false

def Phenomena.Morphology.Studies.Benz2025.beobachtung_CEN : NominalizationDatum

Beobachtung ('observation') — the running example in Ch. 3. All three readings are available for this single form.

Equations

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

def Phenomena.Morphology.Studies.Benz2025.beobachtung_RN : NominalizationDatum

Equations

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

def Phenomena.Morphology.Studies.Benz2025.beobachtung_CCN : NominalizationDatum

Equations

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

def Phenomena.Morphology.Studies.Benz2025.allBeobachtungReadings : List NominalizationDatum

Equations

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

theorem Phenomena.Morphology.Studies.Benz2025.beobachtung_three_readings : (allBeobachtungReadings.any fun (x : NominalizationDatum) => x.reading == Morphology.DM.Allosemy.NominalizationReading.complexEvent) = true ∧ (allBeobachtungReadings.any fun (x : NominalizationDatum) => x.reading == Morphology.DM.Allosemy.NominalizationReading.simpleEntity) = true ∧ (allBeobachtungReadings.any fun (x : NominalizationDatum) => x.reading == Morphology.DM.Allosemy.NominalizationReading.content) = true

All three readings are attested for Beobachtung.

theorem Phenomena.Morphology.Studies.Benz2025.cen_temporal : beobachtung_CEN.temporalModifiers = true

CENs accept temporal modifiers.

theorem Phenomena.Morphology.Studies.Benz2025.rn_plural : beobachtung_RN.pluralizable = true

RNs are pluralizable.

theorem Phenomena.Morphology.Studies.Benz2025.ccn_cp : beobachtung_CCN.takesCPComplement = true

CCNs take CP complements.

theorem Phenomena.Morphology.Studies.Benz2025.cen_no_plural : beobachtung_CEN.pluralizable = false

CENs resist pluralization (event readings are mass-like).

theorem Phenomena.Morphology.Studies.Benz2025.rn_no_temporal : beobachtung_RN.temporalModifiers = false

RNs lack temporal modifiers.

def Phenomena.Morphology.Studies.Benz2025.readingAllosemePair : Morphology.DM.Allosemy.NominalizationReading → Morphology.DM.Allosemy.VAlloseme × Morphology.DM.Allosemy.NAlloseme

Map each reading to its alloseme pair.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Morphology.Studies.Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.result = (Morphology.DM.Allosemy.VAlloseme.eventive, Morphology.DM.Allosemy.NAlloseme.result)
• Phenomena.Morphology.Studies.Benz2025.readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleState = (Morphology.DM.Allosemy.VAlloseme.zero, Morphology.DM.Allosemy.NAlloseme.state)

theorem Phenomena.Morphology.Studies.Benz2025.alloseme_derivation_CEN : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.eventive Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.complexEvent

The alloseme pair correctly derives each reading.

theorem Phenomena.Morphology.Studies.Benz2025.alloseme_derivation_RN : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.zero Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.simpleEntity

theorem Phenomena.Morphology.Studies.Benz2025.alloseme_derivation_CCN : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.eventive Morphology.DM.Allosemy.NAlloseme.content = some Morphology.DM.Allosemy.NominalizationReading.content

theorem Phenomena.Morphology.Studies.Benz2025.alloseme_roundtrip (r : Morphology.DM.Allosemy.NominalizationReading) : match readingAllosemePair r with | (v, n) => Morphology.DM.Allosemy.readingFromAllosemes v n = some r

Round-trip: each reading maps to allosemes that reconstruct it.

theorem Phenomena.Morphology.Studies.Benz2025.zero_content_impossible : Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.zero Morphology.DM.Allosemy.NAlloseme.content = none

The impossible combination: zero v + content n yields no reading. Content requires an underlying event.

theorem Phenomena.Morphology.Studies.Benz2025.cen_simpleEntity_mirror : (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.complexEvent).1 = Morphology.DM.Allosemy.VAlloseme.eventive ∧ (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleEntity).1 = Morphology.DM.Allosemy.VAlloseme.zero ∧ (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.complexEvent).2 = Morphology.DM.Allosemy.NAlloseme.sortal ∧ (readingAllosemePair Morphology.DM.Allosemy.NominalizationReading.simpleEntity).2 = Morphology.DM.Allosemy.NAlloseme.sortal

CEN and simple entity RN are "mirror images" of the division of semantic labor: in CEN, v does the work (introducing the event variable) while n merely nominalizes; in simple entity RN, v is null (zero) and the referential/object interpretation comes from the nominalization context. Both use the same n alloseme (sortal) — it's v that varies.

inductive Phenomena.Morphology.Studies.Benz2025.PreverbalElement : Type

The three types of German preverbal elements.

Ch. 4: prefixes are inseparable and attach as heads; particles are separable and attach as phrases; RSPs are adjectival phrases that form complex predicates with the verb.

• pfx : PreverbalElement
• prt : PreverbalElement
• rsp : PreverbalElement

instance Phenomena.Morphology.Studies.Benz2025.instDecidableEqPreverbalElement : DecidableEq PreverbalElement

Equations

• Phenomena.Morphology.Studies.Benz2025.instDecidableEqPreverbalElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Benz2025.instBEqPreverbalElement : BEq PreverbalElement

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqPreverbalElement = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqPreverbalElement.beq }

def Phenomena.Morphology.Studies.Benz2025.instBEqPreverbalElement.beq : PreverbalElement → PreverbalElement → Bool

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqPreverbalElement.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Morphology.Studies.Benz2025.instReprPreverbalElement.repr : PreverbalElement → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Benz2025.instReprPreverbalElement : Repr PreverbalElement

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprPreverbalElement = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprPreverbalElement.repr }

def Phenomena.Morphology.Studies.Benz2025.PreverbalElement.isHead : PreverbalElement → Bool

Syntactic status: head or phrase.

§4.3.1: following Wurmbrand (1998) and Zeller (2001a), prefixes are heads (inseparable under V2 movement) while particles are phrases (obligatorily stranded under V2). RSPs are unambiguously phrasal (they can be modified: total flach gehämmert).

Equations

• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.pfx.isHead = true
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.prt.isHead = false
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.rsp.isHead = false

def Phenomena.Morphology.Studies.Benz2025.PreverbalElement.alwaysSpecifiesResult : PreverbalElement → Bool

Does this element always specify a result state that conflicts with other delimiters?

§4.1: prefixes and RSPs always contribute a (potentially conflicting) result state specification. Particles can have non-delimiting readings (directional, completive) that don't necessarily conflict — this is why PRT-pfx combinations like aus-er-wählen are interpretively acceptable.

Equations

• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.pfx.alwaysSpecifiesResult = true
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.prt.alwaysSpecifiesResult = false
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.rsp.alwaysSpecifiesResult = true

def Phenomena.Morphology.Studies.Benz2025.inseparablePrefixes : List String

German inseparable prefixes (closed class).

Table 4. The prefix ge- is the rare non-participial prefix (as in ge-bären, ge-denken).

Equations

• Phenomena.Morphology.Studies.Benz2025.inseparablePrefixes = ["be", "ent", "er", "ge", "miss", "ver", "zer"]

def Phenomena.Morphology.Studies.Benz2025.separableParticles : List String

German separable particles (open class, representative sample).

Table 4. Elements like durch-, über-, um- are ambiguous between prefix and particle uses.

Equations

• Phenomena.Morphology.Studies.Benz2025.separableParticles = ["ab", "an", "auf", "aus", "bei", "ein", "los", "nach", "vor", "zu"]

def Phenomena.Morphology.Studies.Benz2025.ambiguousElements : List String

Ambiguous preverbal elements: prefix or particle depending on verb.

Equations

• Phenomena.Morphology.Studies.Benz2025.ambiguousElements = ["durch", "hinter", "über", "um", "unter", "wider"]

structure Phenomena.Morphology.Studies.Benz2025.CooccurrenceDatum : Type

A co-occurrence pair: two preverbal elements in order (outer, inner), where the inner element is closer to the root.

• outer : PreverbalElement
• inner : PreverbalElement
• allowed : Bool
• structurePredicts : Bool

  Structure (head/phrase) predicts this restriction?

• interpretationPredicts : Bool

  Interpretation (delimitation) predicts this restriction?

• exampleStr : String

instance Phenomena.Morphology.Studies.Benz2025.instReprCooccurrenceDatum : Repr CooccurrenceDatum

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprCooccurrenceDatum = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprCooccurrenceDatum.repr }

def Phenomena.Morphology.Studies.Benz2025.instReprCooccurrenceDatum.repr : CooccurrenceDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Benz2025.instBEqCooccurrenceDatum : BEq CooccurrenceDatum

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqCooccurrenceDatum = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqCooccurrenceDatum.beq }

def Phenomena.Morphology.Studies.Benz2025.instBEqCooccurrenceDatum.beq : CooccurrenceDatum → CooccurrenceDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Morphology.Studies.Benz2025.instBEqCooccurrenceDatum.beq x✝¹ x✝ = false

def Phenomena.Morphology.Studies.Benz2025.cooccurrenceTable : List CooccurrenceDatum

The full co-occurrence paradigm from Table 3.

Equations

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

def Phenomena.Morphology.Studies.Benz2025.structurallyCompatible (outer inner : PreverbalElement) : Bool

Structural compatibility: phrase can take headed complement; two heads can combine; head cannot wrap phrase; two phrases cannot stack.

§4.3.1, §4.4.

Equations

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

theorem Phenomena.Morphology.Studies.Benz2025.structural_prediction_matches : List.map (fun (d : CooccurrenceDatum) => structurallyCompatible d.outer d.inner) cooccurrenceTable = List.map (fun (d : CooccurrenceDatum) => d.structurePredicts) cooccurrenceTable

The structural prediction matches Table 3's "Structure Predicts" column.

def Phenomena.Morphology.Studies.Benz2025.interpretivelyCompatible (outer inner : PreverbalElement) : Bool

Two elements that both always specify a result state cannot co-occur, as a single event cannot be delimited twice with conflicting endpoints.

§4.1: the interpretive constraint is about conflicting result state specifications. Particles escape this because they can have non-result (directional/completive) readings.

Equations

• Phenomena.Morphology.Studies.Benz2025.interpretivelyCompatible outer inner = !(outer.alwaysSpecifiesResult && inner.alwaysSpecifiesResult)

theorem Phenomena.Morphology.Studies.Benz2025.interpretive_prediction_matches : List.map (fun (d : CooccurrenceDatum) => interpretivelyCompatible d.outer d.inner) cooccurrenceTable = List.map (fun (d : CooccurrenceDatum) => d.interpretationPredicts) cooccurrenceTable

The interpretive prediction matches Table 3's "Interpretation Predicts" column.

def Phenomena.Morphology.Studies.Benz2025.predictedAllowed (outer inner : PreverbalElement) : Bool

A combination is allowed iff both structurally compatible AND interpretively compatible (no conflicting result states).

§4.4: both factors are needed; neither alone explains the full paradigm.

Equations

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

theorem Phenomena.Morphology.Studies.Benz2025.combined_prediction_matches : List.map (fun (d : CooccurrenceDatum) => predictedAllowed d.outer d.inner) cooccurrenceTable = List.map (fun (d : CooccurrenceDatum) => d.allowed) cooccurrenceTable

The combined prediction matches Table 3's "Allowed" column.

theorem Phenomena.Morphology.Studies.Benz2025.prt_pfx_uniquely_allowed : (List.filter (fun (x : CooccurrenceDatum) => x.allowed) cooccurrenceTable).length = 1

PRT-pfx is the unique allowed combination.

structure Phenomena.Morphology.Studies.Benz2025.GermanResultativeDatum : Type

A German resultative datum with gloss and judgment.

• sentence : String
• gloss : String
• translation : String
• judgment : Core.Empirical.Acceptability
• verbClass : String

instance Phenomena.Morphology.Studies.Benz2025.instReprGermanResultativeDatum : Repr GermanResultativeDatum

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprGermanResultativeDatum = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprGermanResultativeDatum.repr }

def Phenomena.Morphology.Studies.Benz2025.instReprGermanResultativeDatum.repr : GermanResultativeDatum → ℕ → Std.Format

Equations

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

def Phenomena.Morphology.Studies.Benz2025.instBEqGermanResultativeDatum.beq : GermanResultativeDatum → GermanResultativeDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Morphology.Studies.Benz2025.instBEqGermanResultativeDatum.beq x✝¹ x✝ = false

instance Phenomena.Morphology.Studies.Benz2025.instBEqGermanResultativeDatum : BEq GermanResultativeDatum

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqGermanResultativeDatum = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqGermanResultativeDatum.beq }

def Phenomena.Morphology.Studies.Benz2025.germanRSPData : List GermanResultativeDatum

German RSP data from §4.2.

German allows obligatorily transitive, unaccusative, and inherently reflexive M predicates in resultatives — not just unergatives.

Equations

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

theorem Phenomena.Morphology.Studies.Benz2025.german_allows_non_unergative_M : (germanRSPData.any fun (x : GermanResultativeDatum) => x.verbClass == "obligatorily transitive") = true ∧ (germanRSPData.any fun (x : GermanResultativeDatum) => x.verbClass == "unaccusative") = true ∧ (germanRSPData.any fun (x : GermanResultativeDatum) => x.verbClass == "inherently reflexive") = true

German allows non-unergative M predicates in resultatives.

def Phenomena.Morphology.Studies.Benz2025.rsp_pfx_contrasts : List (GermanResultativeDatum × GermanResultativeDatum)

RSPs are incompatible with prefixed verbs. Ch. 4: adding an RSP to a prefix verb is ungrammatical, but the same RSP with the simplex verb is fine.

Equations

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

theorem Phenomena.Morphology.Studies.Benz2025.rsp_pfx_contrast_pattern : (rsp_pfx_contrasts.all fun (x : GermanResultativeDatum × GermanResultativeDatum) => match x with | (bad, good) => bad.judgment == Core.Empirical.Acceptability.unacceptable && good.judgment == Core.Empirical.Acceptability.ok) = true

Every RSP+pfx-verb contrast: pfx-verb ungrammatical, simplex OK.

def Phenomena.Morphology.Studies.Benz2025.rsp_prt_contrasts : List (GermanResultativeDatum × GermanResultativeDatum)

RSPs are also incompatible with particles. Ch. 4: adding an RSP to a particle verb is ungrammatical, but the same RSP with the simplex verb is fine.

Equations

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

theorem Phenomena.Morphology.Studies.Benz2025.rsp_prt_contrast_pattern : (rsp_prt_contrasts.all fun (x : GermanResultativeDatum × GermanResultativeDatum) => match x with | (bad, good) => bad.judgment == Core.Empirical.Acceptability.unacceptable && good.judgment == Core.Empirical.Acceptability.ok) = true

Every RSP+PRT-verb contrast: PRT-verb ungrammatical, simplex OK.

inductive Phenomena.Morphology.Studies.Benz2025.InterpretiveTransparency : Type

Claim 2: RSPs are always transparent (outside v's locality domain for allosemy); prefixes and particles can be opaque (inside the complex head).

• transparent : InterpretiveTransparency
• nonTransparent : InterpretiveTransparency

instance Phenomena.Morphology.Studies.Benz2025.instDecidableEqInterpretiveTransparency : DecidableEq InterpretiveTransparency

Equations

• Phenomena.Morphology.Studies.Benz2025.instDecidableEqInterpretiveTransparency x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Morphology.Studies.Benz2025.instBEqInterpretiveTransparency.beq : InterpretiveTransparency → InterpretiveTransparency → Bool

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqInterpretiveTransparency.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Morphology.Studies.Benz2025.instBEqInterpretiveTransparency : BEq InterpretiveTransparency

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqInterpretiveTransparency = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqInterpretiveTransparency.beq }

def Phenomena.Morphology.Studies.Benz2025.instReprInterpretiveTransparency.repr : InterpretiveTransparency → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Benz2025.instReprInterpretiveTransparency : Repr InterpretiveTransparency

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprInterpretiveTransparency = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprInterpretiveTransparency.repr }

def Phenomena.Morphology.Studies.Benz2025.typicalTransparency : PreverbalElement → InterpretiveTransparency

Equations

• Phenomena.Morphology.Studies.Benz2025.typicalTransparency Phenomena.Morphology.Studies.Benz2025.PreverbalElement.rsp = Phenomena.Morphology.Studies.Benz2025.InterpretiveTransparency.transparent
• Phenomena.Morphology.Studies.Benz2025.typicalTransparency Phenomena.Morphology.Studies.Benz2025.PreverbalElement.pfx = Phenomena.Morphology.Studies.Benz2025.InterpretiveTransparency.nonTransparent
• Phenomena.Morphology.Studies.Benz2025.typicalTransparency Phenomena.Morphology.Studies.Benz2025.PreverbalElement.prt = Phenomena.Morphology.Studies.Benz2025.InterpretiveTransparency.nonTransparent

theorem Phenomena.Morphology.Studies.Benz2025.rsp_always_transparent : typicalTransparency PreverbalElement.rsp = InterpretiveTransparency.transparent

Complex predicate semantics

Following Williams (2015), adopted by §4.2: resultatives are complex predicates with semantics:

K(e₁, e₂, s) = Means(e₁, e₂) & End(e₁, s)

where e₁ is the complex event of change, e₂ is the means/manner subevent, and s is the result state. The M predicate is the verb; the R predicate is the RSP. This is NOT a causal relation — the means event can be concurrent with the change.

The End Theme Postulate links the Theme of the complex event to the end state: End(e₁, s) & Theme(e₁, x) |= Theme(s, x).

See also Causative.Resultatives for the complementary analysis via causal dynamics, structural sufficiency, and CC-selection.

theorem Phenomena.Morphology.Studies.Benz2025.claim1_two_factors : (cooccurrenceTable.any fun (d : CooccurrenceDatum) => d.structurePredicts && !d.interpretationPredicts && !d.allowed) = true ∧ (cooccurrenceTable.any fun (d : CooccurrenceDatum) => d.interpretationPredicts && !d.structurePredicts && !d.allowed) = true

Claim 1: Neither factor alone predicts the full co-occurrence paradigm. Structure alone is insufficient: some structurally OK combinations are blocked by interpretation (pfx-pfx, RSP-pfx). Interpretation alone is insufficient: some interpretively OK combinations are blocked by structure (pfx-PRT, PRT-PRT, RSP-PRT).

inductive Phenomena.Morphology.Studies.Benz2025.NominalizationType : Type

German nominalization types discussed in Ch. 5.

• ung: -ung suffixation (Beobachtung, Erzählung). Requires the verb to project a full verbal shell including v; the entire vP is nominalized by n.
• ge_e: Ge-...-e circumfixation (Gerede, Gelaufe). Directly nominalizes the root without a full verbal projection; the root must be able to stand without obligatory internal arguments.
• nomInfinitive: Nominalized infinitive (das Beobachten, das Erzählen). The most permissive: the full verbal structure is preserved under nominalization.

• ung : NominalizationType
• ge_e : NominalizationType
• nomInfinitive : NominalizationType

instance Phenomena.Morphology.Studies.Benz2025.instDecidableEqNominalizationType : DecidableEq NominalizationType

Equations

• Phenomena.Morphology.Studies.Benz2025.instDecidableEqNominalizationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationType : BEq NominalizationType

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationType = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationType.beq }

def Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationType.beq : NominalizationType → NominalizationType → Bool

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqNominalizationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Morphology.Studies.Benz2025.instReprNominalizationType : Repr NominalizationType

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprNominalizationType = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprNominalizationType.repr }

def Phenomena.Morphology.Studies.Benz2025.instReprNominalizationType.repr : NominalizationType → ℕ → Std.Format

Equations

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

def Phenomena.Morphology.Studies.Benz2025.peAcceptable : NominalizationType → PreverbalElement → Bool

Whether a preverbal element is acceptable in a given nominalization type.

Ch. 5: the distribution of preverbal elements across nominalization types reveals complementary distribution between prefixes and RSPs:

	pfx	prt	RSP
-ung	✓	✓	✗
Ge-...-e	✗	✓	✓
nom. inf.	✓	✓	✓

• -ung + RSP = ✗: RSPs are phrasal and cannot be trapped inside the complex head that -ung nominalization creates. The RSP would need to be inside the vP that n selects, but as a phrase it cannot incorporate.
• Ge-...-e + pfx = ✗: Ge-...-e directly nominalizes the root; it requires the root to be available without obligatory internal arguments. Prefixed verbs (where the prefix saturates argument structure) are incompatible because the prefix has already formed a complex head with the root, and the Ge-...-e circumfix cannot wrap around a complex head.
• Nom. inf.: maximally permissive because the full verbal projection (including any preverbal element) is preserved under nominalization.

Equations

• Phenomena.Morphology.Studies.Benz2025.peAcceptable Phenomena.Morphology.Studies.Benz2025.NominalizationType.ung Phenomena.Morphology.Studies.Benz2025.PreverbalElement.pfx = true
• Phenomena.Morphology.Studies.Benz2025.peAcceptable Phenomena.Morphology.Studies.Benz2025.NominalizationType.ung Phenomena.Morphology.Studies.Benz2025.PreverbalElement.prt = true
• Phenomena.Morphology.Studies.Benz2025.peAcceptable Phenomena.Morphology.Studies.Benz2025.NominalizationType.ung Phenomena.Morphology.Studies.Benz2025.PreverbalElement.rsp = false
• Phenomena.Morphology.Studies.Benz2025.peAcceptable Phenomena.Morphology.Studies.Benz2025.NominalizationType.ge_e Phenomena.Morphology.Studies.Benz2025.PreverbalElement.pfx = false
• Phenomena.Morphology.Studies.Benz2025.peAcceptable Phenomena.Morphology.Studies.Benz2025.NominalizationType.ge_e Phenomena.Morphology.Studies.Benz2025.PreverbalElement.prt = true
• Phenomena.Morphology.Studies.Benz2025.peAcceptable Phenomena.Morphology.Studies.Benz2025.NominalizationType.ge_e Phenomena.Morphology.Studies.Benz2025.PreverbalElement.rsp = true
• Phenomena.Morphology.Studies.Benz2025.peAcceptable Phenomena.Morphology.Studies.Benz2025.NominalizationType.nomInfinitive x✝ = true

theorem Phenomena.Morphology.Studies.Benz2025.pfx_rsp_complementary_ung_ge : peAcceptable NominalizationType.ung PreverbalElement.pfx = true ∧ peAcceptable NominalizationType.ung PreverbalElement.rsp = false ∧ peAcceptable NominalizationType.ge_e PreverbalElement.pfx = false ∧ peAcceptable NominalizationType.ge_e PreverbalElement.rsp = true

Prefixes and RSPs show complementary distribution across -ung and Ge-...-e: pfx is accepted where RSP is rejected, and vice versa.

Ch. 5: this complementarity follows from the structural difference between head-level (pfx) and phrase-level (RSP) preverbal elements, interacting with the different structural requirements of -ung (requires full vP) vs Ge-...-e (directly nominalizes root).

theorem Phenomena.Morphology.Studies.Benz2025.prt_accepted_in_both : peAcceptable NominalizationType.ung PreverbalElement.prt = true ∧ peAcceptable NominalizationType.ge_e PreverbalElement.prt = true

Particles are accepted in both -ung and Ge-...-e: they are structurally flexible enough to appear in both configurations.

theorem Phenomena.Morphology.Studies.Benz2025.nom_inf_maximally_permissive (pe : PreverbalElement) : peAcceptable NominalizationType.nomInfinitive pe = true

Nominalized infinitives accept all three PE types.

theorem Phenomena.Morphology.Studies.Benz2025.rsp_blocked_in_ung : peAcceptable NominalizationType.ung PreverbalElement.rsp = false

RSPs are blocked in -ung nominalizations — this connects to the co-occurrence restriction: RSPs as phrases cannot incorporate into the complex head structure that -ung creates.

theorem Phenomena.Morphology.Studies.Benz2025.pfx_blocked_in_ge_e : peAcceptable NominalizationType.ge_e PreverbalElement.pfx = false

Prefixes are blocked in Ge-...-e nominalizations — the circumfix cannot wrap around a root that already has a prefix head.

theorem Phenomena.Morphology.Studies.Benz2025.ung_head_phrase_pattern : peAcceptable NominalizationType.ung PreverbalElement.pfx = PreverbalElement.pfx.isHead ∧ peAcceptable NominalizationType.ung PreverbalElement.rsp = PreverbalElement.rsp.isHead

The head/phrase distinction predicts the -ung pattern: heads (pfx) are accepted, phrases (rsp) are not. Particles are the exception — separable but still accepted.

Benz's core theoretical argument (Chs. 4–5)

central claim is that the 9-cell co-occurrence paradigm (§6, Table 3) and the PE×nominalization distribution (§16, the table in Ch. 5) are not stipulated — they follow from the conjunction of two independently motivated principles:

1. Lexical Integrity (structural): a phrase cannot incorporate into a head. Only head+head or phrase+head are licit; head+phrase and phrase+phrase are not.

2. Result State Uniqueness (interpretive): an event can have at most one telos. Two elements that both obligatorily specify a result state cannot co-occur.

The types SynLevel and ResultStateSpec below formalize these two dimensions abstractly. The compatibility functions incorporationAllowed and resultStatesCompatible are defined purely over these abstract types, with no reference to PreverbalElement. Only then do we classify each PE into these dimensions and prove that the predicted paradigm matches.

inductive Phenomena.Morphology.Studies.Benz2025.SynLevel : Type

The syntactic level of a morphological element: head (X⁰) or phrase (XP).

This distinction is standard in X-bar theory and is logically prior to the PE typology — it applies to any syntactic object, not just German preverbal elements.

• head : SynLevel
• phrase : SynLevel

instance Phenomena.Morphology.Studies.Benz2025.instDecidableEqSynLevel : DecidableEq SynLevel

Equations

• Phenomena.Morphology.Studies.Benz2025.instDecidableEqSynLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Benz2025.instBEqSynLevel : BEq SynLevel

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqSynLevel = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqSynLevel.beq }

def Phenomena.Morphology.Studies.Benz2025.instBEqSynLevel.beq : SynLevel → SynLevel → Bool

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqSynLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Morphology.Studies.Benz2025.instReprSynLevel : Repr SynLevel

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprSynLevel = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprSynLevel.repr }

def Phenomena.Morphology.Studies.Benz2025.instReprSynLevel.repr : SynLevel → ℕ → Std.Format

Equations

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

def Phenomena.Morphology.Studies.Benz2025.incorporationAllowed (outer inner : SynLevel) : Bool

Lexical Integrity: a head can take a head complement (head-adjunction / incorporation), and a phrase can take a head complement (normal complementation), but a head cannot take a phrase complement in a word-internal structure, and two phrases cannot form a word.

This is a general principle of morphosyntactic structure, not specific to German preverbal elements. It follows from the ban on phrasal incorporation (§4.3.1, following Baker 1988).

Equations

• Phenomena.Morphology.Studies.Benz2025.incorporationAllowed Phenomena.Morphology.Studies.Benz2025.SynLevel.head Phenomena.Morphology.Studies.Benz2025.SynLevel.head = true
• Phenomena.Morphology.Studies.Benz2025.incorporationAllowed Phenomena.Morphology.Studies.Benz2025.SynLevel.phrase Phenomena.Morphology.Studies.Benz2025.SynLevel.head = true
• Phenomena.Morphology.Studies.Benz2025.incorporationAllowed Phenomena.Morphology.Studies.Benz2025.SynLevel.head Phenomena.Morphology.Studies.Benz2025.SynLevel.phrase = false
• Phenomena.Morphology.Studies.Benz2025.incorporationAllowed Phenomena.Morphology.Studies.Benz2025.SynLevel.phrase Phenomena.Morphology.Studies.Benz2025.SynLevel.phrase = false

inductive Phenomena.Morphology.Studies.Benz2025.ResultStateSpec : Type

Whether an element obligatorily introduces a result state specification.

This is a semantic property that applies to any predicate-modifying element — it is not specific to German PEs. An element that always specifies a result state will conflict with another such element because a single event has at most one telos.

• specifies : ResultStateSpec
• neutral : ResultStateSpec

instance Phenomena.Morphology.Studies.Benz2025.instDecidableEqResultStateSpec : DecidableEq ResultStateSpec

Equations

• Phenomena.Morphology.Studies.Benz2025.instDecidableEqResultStateSpec x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Benz2025.instBEqResultStateSpec : BEq ResultStateSpec

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqResultStateSpec = { beq := Phenomena.Morphology.Studies.Benz2025.instBEqResultStateSpec.beq }

def Phenomena.Morphology.Studies.Benz2025.instBEqResultStateSpec.beq : ResultStateSpec → ResultStateSpec → Bool

Equations

• Phenomena.Morphology.Studies.Benz2025.instBEqResultStateSpec.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Morphology.Studies.Benz2025.instReprResultStateSpec.repr : ResultStateSpec → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Benz2025.instReprResultStateSpec : Repr ResultStateSpec

Equations

• Phenomena.Morphology.Studies.Benz2025.instReprResultStateSpec = { reprPrec := Phenomena.Morphology.Studies.Benz2025.instReprResultStateSpec.repr }

def Phenomena.Morphology.Studies.Benz2025.resultStatesCompatible (a b : ResultStateSpec) : Bool

Result State Uniqueness: two elements that both obligatorily specify a result state cannot co-occur, because a single event cannot be delimited by two conflicting endpoints.

This is an instance of a general thematic uniqueness constraint: just as an event has at most one agent (Carlson 1998), it has at most one telos. The constraint is purely interpretive — it says nothing about syntax.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Morphology.Studies.Benz2025.resultStatesCompatible a b = true

def Phenomena.Morphology.Studies.Benz2025.PreverbalElement.synLevel : PreverbalElement → SynLevel

Classify each PE by its syntactic level.

§4.3.1: prefixes are heads (inseparable under V2); particles and RSPs are phrases (stranded under V2, can be modified).

Equations

• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.pfx.synLevel = Phenomena.Morphology.Studies.Benz2025.SynLevel.head
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.prt.synLevel = Phenomena.Morphology.Studies.Benz2025.SynLevel.phrase
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.rsp.synLevel = Phenomena.Morphology.Studies.Benz2025.SynLevel.phrase

def Phenomena.Morphology.Studies.Benz2025.PreverbalElement.resultSpec : PreverbalElement → ResultStateSpec

Classify each PE by its result state specification.

§4.1: prefixes and RSPs obligatorily specify a result state. Particles are neutral — they can have non-delimiting readings (directional, completive) that do not introduce a result state.

Equations

• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.pfx.resultSpec = Phenomena.Morphology.Studies.Benz2025.ResultStateSpec.specifies
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.prt.resultSpec = Phenomena.Morphology.Studies.Benz2025.ResultStateSpec.neutral
• Phenomena.Morphology.Studies.Benz2025.PreverbalElement.rsp.resultSpec = Phenomena.Morphology.Studies.Benz2025.ResultStateSpec.specifies

theorem Phenomena.Morphology.Studies.Benz2025.synLevel_matches_isHead (pe : PreverbalElement) : (pe.synLevel == SynLevel.head) = pe.isHead

The abstract synLevel classification is equivalent to isHead.

theorem Phenomena.Morphology.Studies.Benz2025.resultSpec_matches_alwaysSpecifies (pe : PreverbalElement) : (pe.resultSpec == ResultStateSpec.specifies) = pe.alwaysSpecifiesResult

The abstract resultSpec classification is equivalent to alwaysSpecifiesResult.

inductive Phenomena.Morphology.Studies.Benz2025.Blocked : PreverbalElement → PreverbalElement → Prop

A blocking derivation: a proof that a PE combination violates one of Benz's two independently motivated principles.

Each constructor is a derivation rule whose premises are stated in terms of the abstract classification (SynLevel, ResultStateSpec), not PE-specific Booleans. A combination is blocked iff at least one derivation can be constructed.

byLexicalIntegrity (§4.3.1, Baker 1988): only heads can occupy the inner (closer-to-root) position in a word-internal combination. A phrasal inner element cannot incorporate.

byResultUniqueness (§4.1): an event has at most one telos. Two elements that both obligatorily specify a result state yield conflicting endpoints.

• byLexicalIntegrity {o i : PreverbalElement} : i.synLevel = SynLevel.phrase → Blocked o i
• byResultUniqueness {o i : PreverbalElement} : o.resultSpec = ResultStateSpec.specifies → i.resultSpec = ResultStateSpec.specifies → Blocked o i

theorem Phenomena.Morphology.Studies.Benz2025.paradigm_from_principles (o i : PreverbalElement) : predictedAllowed o i = (incorporationAllowed o.synLevel i.synLevel && resultStatesCompatible o.resultSpec i.resultSpec)

Boolean decomposition lemma: predictedAllowed factors into the conjunction of the two abstract compatibility functions. Used as a stepping stone in the soundness proof below.

The derivation system (Blocked) is both sound and complete with respect to the empirical paradigm (predictedAllowed). Together with combined_prediction_matches (§9), this means the two principles exactly generate the data: every blocked cell has a derivation, every derivation corresponds to a blocked cell, and the unique allowed cell (PRT-pfx) has no derivation.

theorem Phenomena.Morphology.Studies.Benz2025.blocked_sound {o i : PreverbalElement} (h : Blocked o i) : predictedAllowed o i = false

Soundness: every blocking derivation corresponds to a genuinely blocked combination. The theory does not over-generate.

• byLexicalIntegrity: a phrasal inner element makes incorporationAllowed return false regardless of the outer element's level.
• byResultUniqueness: two result-specifying elements make resultStatesCompatible return false regardless of structure.

theorem Phenomena.Morphology.Studies.Benz2025.blocked_complete {o i : PreverbalElement} (h : predictedAllowed o i = false) : Blocked o i

Completeness: every blocked combination has a blocking derivation. The two principles account for ALL restrictions — nothing is left unexplained.

For each of the 8 blocked cells, an explicit derivation is constructed (6 by Lexical Integrity, 2 by Result State Uniqueness). For PRT-pfx, the hypothesis is contradictory.

theorem Phenomena.Morphology.Studies.Benz2025.prt_pfx_no_derivation : ¬Blocked PreverbalElement.prt PreverbalElement.pfx

The allowed combination has no derivation. PRT-pfx is allowed precisely because neither principle applies:

• pfx is a head (not a phrase), so Lexical Integrity is satisfied
• prt is result-neutral (not specifying), so Result Uniqueness is satisfied

We examine each possible derivation and show its premises are contradicted by the PE classifications.

theorem Phenomena.Morphology.Studies.Benz2025.pfx_pfx_only_by_result : Blocked PreverbalElement.pfx PreverbalElement.pfx ∧ PreverbalElement.pfx.synLevel ≠ SynLevel.phrase

pfx-pfx is blocked ONLY by Result State Uniqueness — Lexical Integrity cannot derive it (both are heads, so the inner is not phrasal). This shows the interpretive rule is not redundant.

theorem Phenomena.Morphology.Studies.Benz2025.pfx_prt_only_by_structure : Blocked PreverbalElement.pfx PreverbalElement.prt ∧ PreverbalElement.prt.resultSpec ≠ ResultStateSpec.specifies

pfx-PRT is blocked ONLY by Lexical Integrity — Result State Uniqueness cannot derive it (PRT is result-neutral). This shows the structural rule is not redundant.

theorem Phenomena.Morphology.Studies.Benz2025.incorporation_only_depends_on_inner (outer inner : SynLevel) : incorporationAllowed outer inner = (inner == SynLevel.head)

Incorporation depends only on the inner element's level: the outer element's level is irrelevant. This is a derived property of the incorporationAllowed function, not stipulated.

theorem Phenomena.Morphology.Studies.Benz2025.ung_from_principles (pe : PreverbalElement) : peAcceptable NominalizationType.ung pe = (incorporationAllowed pe.synLevel pe.synLevel || resultStatesCompatible pe.resultSpec pe.resultSpec)

The nominalization theorem. -ung acceptability (Ch. 5) follows from the same two abstract principles applied reflexively: a PE is acceptable in -ung iff it can incorporate with itself (headedness) OR its result state does not conflict with itself (neutrality).

This connects Ch. 5 to Ch. 4: the PE×nominalization distribution is not an independent observation — it is a projection of the same two principles that generate the co-occurrence paradigm.

theorem Phenomena.Morphology.Studies.Benz2025.ge_e_from_principles (pe : PreverbalElement) : peAcceptable NominalizationType.ge_e pe = (pe.synLevel == SynLevel.phrase)

Ge-...-e acceptability reduces to a single abstract principle: a PE is acceptable in Ge-...-e iff it is a phrase (not a head). The circumfix directly nominalizes the root, so only non-head elements are compatible.

theorem Phenomena.Morphology.Studies.Benz2025.ung_ge_e_mirror (pe : PreverbalElement) (h : pe.synLevel = SynLevel.head) : peAcceptable NominalizationType.ung pe = true ∧ peAcceptable NominalizationType.ge_e pe = false

The -ung / Ge-...-e mirror: for heads, the two nominalization types give opposite results. This follows from ge_e_from_principles and the fact that heads satisfy incorporationAllowed reflexively.

These theorems chain through four independently defined modules: RootTypology.lean (root semantics) → Allosemy.lean (v alloseme selection) → Allosemy.lean (nominalization reading) → Benz2025.lean (PE distribution from abstract principles). No single module defines the full path.

theorem Phenomena.Morphology.Studies.Benz2025.end_to_end_result_root : have v := Morphology.DM.Allosemy.VAlloseme.fromRootType RootType.result; v = Morphology.DM.Allosemy.VAlloseme.eventive ∧ Morphology.DM.Allosemy.readingFromAllosemes v Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.complexEvent ∧ incorporationAllowed PreverbalElement.pfx.synLevel PreverbalElement.pfx.synLevel = true ∧ resultStatesCompatible PreverbalElement.rsp.resultSpec PreverbalElement.rsp.resultSpec = false

End-to-end for result roots: a result root selects eventive v, yielding CEN in -ung nominalizations. -ung accepts heads (pfx) and rejects phrases that specify results (RSP) — both predictions derived from the abstract principles, not from the peAcceptable table.

theorem Phenomena.Morphology.Studies.Benz2025.end_to_end_pc_root : have v := Morphology.DM.Allosemy.VAlloseme.fromRootType RootType.propertyConcept; v = Morphology.DM.Allosemy.VAlloseme.zero ∧ Morphology.DM.Allosemy.readingFromAllosemes v Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.simpleEntity ∧ (PreverbalElement.rsp.synLevel == SynLevel.phrase) = true ∧ (PreverbalElement.pfx.synLevel == SynLevel.phrase) = false

Mirror chain for PC roots: zero v → simple entity reading → Ge-...-e, which accepts phrases (RSP) and rejects heads (pfx).

def Phenomena.Morphology.Studies.Benz2025.canUngNominalize : Option Semantics.Tense.Aspect.LexicalAspect.VendlerClass → Bool

Whether a verb can undergo -ung nominalization, based on its Vendler class.

Ch. 5, following Roßdeutscher & Kamp (2010): -ung requires complex change-of-state event structure. Only accomplishments and achievements (which contain a result state component) qualify. Activities and states do not.

Equations

• Phenomena.Morphology.Studies.Benz2025.canUngNominalize (some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment) = true
• Phenomena.Morphology.Studies.Benz2025.canUngNominalize (some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement) = true
• Phenomena.Morphology.Studies.Benz2025.canUngNominalize x✝ = false

theorem Phenomena.Morphology.Studies.Benz2025.activity_no_ung : canUngNominalize Fragments.German.Predicates.haemmern.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.malen.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.kuessen.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.fuehren.vendlerClass = false ∧ canUngNominalize Fragments.German.Predicates.rauben.vendlerClass = false

Activity simplex verbs cannot form -ung nominalizations: *Hämmer-ung, *Mal-ung, *Küss-ung.

theorem Phenomena.Morphology.Studies.Benz2025.complex_event_ung : canUngNominalize Fragments.German.Predicates.beobachten.vendlerClass = true ∧ canUngNominalize Fragments.German.Predicates.einfuehren.vendlerClass = true ∧ canUngNominalize Fragments.German.Predicates.verbinden.vendlerClass = true ∧ canUngNominalize Fragments.German.Predicates.brechen.vendlerClass = true

Prefix/particle verbs with complex event structure CAN form -ung nominalizations: Beobacht-ung, Einführ-ung, Verbind-ung.

def Phenomena.Morphology.Studies.Benz2025.isTransitiveVerb (v : Fragments.German.Predicates.GermanVerbEntry) : Bool

Transitivity derived from fragment fields (not from a raw string).

Equations

• Phenomena.Morphology.Studies.Benz2025.isTransitiveVerb v = (v.complementType == Core.Verbs.ComplementType.np && !v.unaccusative)

theorem Phenomena.Morphology.Studies.Benz2025.rsp_data_grounded_in_fragments : isTransitiveVerb Fragments.German.Predicates.haemmern = true ∧ isTransitiveVerb Fragments.German.Predicates.brechen = true ∧ Fragments.German.Predicates.frieren.unaccusative = true ∧ isTransitiveVerb Fragments.German.Predicates.frieren = false

The verb classifications in the RSP data (§10, encoded as raw strings) are derivable from the fragment entries' typed fields. Changing frieren's unaccusative field or hämmern's complementType would break this theorem without touching the RSP data.

theorem Phenomena.Morphology.Studies.Benz2025.rootType_alloseme_divergence : Option.map Morphology.DM.Allosemy.VAlloseme.fromRootType Fragments.German.Predicates.brechen.rootType = some Morphology.DM.Allosemy.VAlloseme.eventive ∧ Option.map Morphology.DM.Allosemy.VAlloseme.fromRootType Fragments.German.Predicates.frieren.rootType = some Morphology.DM.Allosemy.VAlloseme.zero ∧ Option.map (fun (x : RootType) => (Morphology.DM.Allosemy.VAlloseme.fromRootType x).introducesEvent) Fragments.German.Predicates.brechen.rootType = some true ∧ Option.map (fun (x : RootType) => (Morphology.DM.Allosemy.VAlloseme.fromRootType x).introducesEvent) Fragments.German.Predicates.frieren.rootType = some false

brechen (result root) and frieren (PC root) yield opposite v allosemes. This connects three modules: the fragment entry's rootType (Predicates.lean), VAlloseme.fromRootType (Allosemy.lean), and VAlloseme.introducesEvent (Allosemy.lean).

theorem Phenomena.Morphology.Studies.Benz2025.brechen_two_paths : (Fragments.German.Predicates.brechen.rootType.bind fun (rt : RootType) => Morphology.DM.Allosemy.readingFromAllosemes (Morphology.DM.Allosemy.VAlloseme.fromRootType rt) Morphology.DM.Allosemy.NAlloseme.sortal) = some Morphology.DM.Allosemy.NominalizationReading.complexEvent ∧ canUngNominalize Fragments.German.Predicates.brechen.vendlerClass = true

The allosemy-based CEN prediction and the event-structure-based -ung prediction agree for brechen: result root → eventive v → CEN reading → can -ung, and achievement vendlerClass → can -ung. Two independent paths to the same conclusion.

theorem Phenomena.Morphology.Studies.Benz2025.frieren_canonical_vs_possible : (Fragments.German.Predicates.frieren.rootType.bind fun (rt : RootType) => Morphology.DM.Allosemy.readingFromAllosemes (Morphology.DM.Allosemy.VAlloseme.fromRootType rt) Morphology.DM.Allosemy.NAlloseme.sortal) = some Morphology.DM.Allosemy.NominalizationReading.simpleEntity ∧ canUngNominalize Fragments.German.Predicates.frieren.vendlerClass = true ∧ Morphology.DM.Allosemy.readingFromAllosemes Morphology.DM.Allosemy.VAlloseme.eventive Morphology.DM.Allosemy.NAlloseme.sortal = some Morphology.DM.Allosemy.NominalizationReading.complexEvent

The two paths DISAGREE for frieren: the canonical PC root → zero v → RN (not CEN), yet the achievement vendlerClass → can -ung. This is not a bug — it captures key insight that allosemy means BOTH v allosemes are available for any verb. The canonical alloseme is a default, not a constraint. Frieren CAN have eventive v and thus CAN form a CEN, even though its canonical alloseme is zero.