[TBD14] — Polarity Marking in Dutch and German

[TBD14]

Cross-linguistic production study comparing how Dutch and German speakers mark polarity switches (negation → affirmation) in two discourse contexts: polarity contrast (different topic situations) and polarity correction (same topic situation, mutually exclusive claims).

Key Findings

1. Dutch uses the affirmative particle wel as its dominant strategy (~88% in contrast, ~63% in correction).
2. German uses Verum focus (pitch accent on finite verb) as its dominant strategy (~82% in contrast, ~78% in correction).
3. German has zero sentence-internal polarity particles.
4. Correction contexts elicit more prosodic prominence than contrast contexts in both languages.
5. Dutch wel accent type varies by context: downstepped fall (!HL L%) in contrast, plain fall (HL L%) in correction.

Theoretical contribution

[TBD14] (p. 104, following Blühdorn 2012) argue that VF and wel operate at different semantic levels: VF targets the assertion operator (the element carrying the assertive relation between topic and comment), while wel targets the polarity operator ([±Pol]). Both achieve polarity contrast/correction pragmatically, but they are structurally distinct; the two-level theory is formalised in the polarity-marking-levels section below.

Data Sources

• Fig. 2: Dutch production strategy distribution
• Fig. 3: Dutch wel accent rate by context
• Fig. 5: Dutch wel accent type by context
• Fig. 6: German production strategy distribution
• p. 102: German VF pitch range statistics

Note: Production percentages are approximate (read from bar charts).

Polarity-marking levels (p. 104, following Blühdorn 2012)

Particles target the polarity operator directly; Verum focus targets the assertion operator that wraps it — predicting opposite co-occurrence patterns with sentential negation.

inductive TurcoBraunDimroth2014.PolarityMarkingLevel : Type

The semantic level at which a polarity-marking device operates: polarity (affirmative particles like Dutch wel set [+Pol]) vs assertion (German Verum focus highlights the assertion operator, [Hoh92]).

• polarity : PolarityMarkingLevel
• assertion : PolarityMarkingLevel

@[implicit_reducible]

instance TurcoBraunDimroth2014.instDecidableEqPolarityMarkingLevel : DecidableEq PolarityMarkingLevel

Equations

• TurcoBraunDimroth2014.instDecidableEqPolarityMarkingLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance TurcoBraunDimroth2014.instReprPolarityMarkingLevel : Repr PolarityMarkingLevel

Equations

• TurcoBraunDimroth2014.instReprPolarityMarkingLevel = { reprPrec := TurcoBraunDimroth2014.instReprPolarityMarkingLevel.repr }

def TurcoBraunDimroth2014.instReprPolarityMarkingLevel.repr : PolarityMarkingLevel → ℕ → Std.Format

Equations

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

def TurcoBraunDimroth2014.strategyLevel : Semantics.Polarity.Marking.Strategy → Option PolarityMarkingLevel

The semantic level of each polarity-marking strategy; none for strategies without a clear level assignment.

Equations

• TurcoBraunDimroth2014.strategyLevel Semantics.Polarity.Marking.Strategy.particle = some TurcoBraunDimroth2014.PolarityMarkingLevel.polarity
• TurcoBraunDimroth2014.strategyLevel Semantics.Polarity.Marking.Strategy.verumFocus = some TurcoBraunDimroth2014.PolarityMarkingLevel.assertion
• TurcoBraunDimroth2014.strategyLevel Semantics.Polarity.Marking.Strategy.polarityReversal = some TurcoBraunDimroth2014.PolarityMarkingLevel.polarity
• TurcoBraunDimroth2014.strategyLevel Semantics.Polarity.Marking.Strategy.other = none
• TurcoBraunDimroth2014.strategyLevel Semantics.Polarity.Marking.Strategy.unmarked = none

structure TurcoBraunDimroth2014.SentenceStructure (W : Type u_2) : Type u_2

A sentence decomposed into its polarity-relevant layers: a polarity-neutral radical, the polarity value [±Pol], and the overtly marked level, if any (Option — assertion-level and polarity-level marking are mutually exclusive by construction).

• radical : W → Bool

  Polarity-neutral propositional content

• pol : Features.Polarity

  The polarity value [±Pol]

• marking : Option PolarityMarkingLevel

  Which structural level is overtly marked, if any

def TurcoBraunDimroth2014.SentenceStructure.eval {W : Type u_1} (s : SentenceStructure W) : W → Bool

Apply polarity to the radical: polarity is the innermost operator.

Equations

• s.eval = match (motive := Features.Polarity → W → Bool) s.pol with | Features.Polarity.positive => s.radical | Features.Polarity.negative => fun (w : W) => !s.radical w

def TurcoBraunDimroth2014.PolarityMarkingLevel.compatibleWith : PolarityMarkingLevel → Features.Polarity → Bool

Assertion-level marking (VF) is compatible with either polarity; polarity-level marking (particles) requires [+Pol] — the particle IS the polarity operator.

Equations

• TurcoBraunDimroth2014.PolarityMarkingLevel.assertion.compatibleWith x✝ = true
• TurcoBraunDimroth2014.PolarityMarkingLevel.polarity.compatibleWith Features.Polarity.positive = true
• TurcoBraunDimroth2014.PolarityMarkingLevel.polarity.compatibleWith Features.Polarity.negative = false

def TurcoBraunDimroth2014.SentenceStructure.wellFormed {W : Type u_1} (s : SentenceStructure W) : Bool

Unmarked sentences are always well-formed; marked sentences need a level compatible with their polarity value.

Equations

• s.wellFormed = match s.marking with | none => true | some level => level.compatibleWith s.pol

theorem TurcoBraunDimroth2014.vf_negative_wellformed {W : Type u_1} (radical : W → Bool) : { radical := radical, pol := Features.Polarity.negative, marking := some PolarityMarkingLevel.assertion }.wellFormed = true

VF on a negative sentence is well-formed: Das Kind HAT nicht geweint — emphatic denial (Gussenhoven 1983).

theorem TurcoBraunDimroth2014.vf_positive_wellformed {W : Type u_1} (radical : W → Bool) : { radical := radical, pol := Features.Polarity.positive, marking := some PolarityMarkingLevel.assertion }.wellFormed = true

theorem TurcoBraunDimroth2014.particle_negative_illformed {W : Type u_1} (radical : W → Bool) : { radical := radical, pol := Features.Polarity.negative, marking := some PolarityMarkingLevel.polarity }.wellFormed = false

Polarity particles require [+Pol]: *Het kind heeft wel niet gehuild is contradictory.

theorem TurcoBraunDimroth2014.particle_positive_wellformed {W : Type u_1} (radical : W → Bool) : { radical := radical, pol := Features.Polarity.positive, marking := some PolarityMarkingLevel.polarity }.wellFormed = true

theorem TurcoBraunDimroth2014.levels_differ_on_negation : PolarityMarkingLevel.polarity.compatibleWith Features.Polarity.negative ≠ PolarityMarkingLevel.assertion.compatibleWith Features.Polarity.negative

The two levels differ exactly on negation compatibility.

theorem TurcoBraunDimroth2014.functional_equivalence_positive {W : Type u_1} (radical : W → Bool) : have vf := { radical := radical, pol := Features.Polarity.positive, marking := some PolarityMarkingLevel.assertion }; have prt := { radical := radical, pol := Features.Polarity.positive, marking := some PolarityMarkingLevel.polarity }; vf.eval = prt.eval

Both strategies yield the same truth conditions on a positive proposition — the paper's "functional equivalence" of wel and VF.

Types

inductive TurcoBraunDimroth2014.Language : Type

Languages compared in the study.

• dutch : Language
• german : Language

@[implicit_reducible]

instance TurcoBraunDimroth2014.instDecidableEqLanguage : DecidableEq Language

Equations

• TurcoBraunDimroth2014.instDecidableEqLanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TurcoBraunDimroth2014.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TurcoBraunDimroth2014.instReprLanguage : Repr Language

Equations

• TurcoBraunDimroth2014.instReprLanguage = { reprPrec := TurcoBraunDimroth2014.instReprLanguage.repr }

structure TurcoBraunDimroth2014.ProductionDatum : Type

A production-strategy distribution datum (percentages as rationals). The distribution is keyed by Strategy, so adding a strategy constructor forces updating every datum.

• language : Language
• context : Discourse.Coherence.CoherenceRelation
• pctByStrategy : Semantics.Polarity.Marking.Strategy → ℚ

  Percentage of trials per strategy (approximate, from bar charts)

structure TurcoBraunDimroth2014.ProminenceDatum : Type

A prosodic prominence datum (pitch range in semitones).

• context : Discourse.Coherence.CoherenceRelation
• pitchRangeST : ℚ

  Pitch range in semitones

• beta : ℚ

  Regression coefficient (contrast relative to correction baseline)

• se : ℚ

  Standard error

• pValue : ℚ

  p-value (encoded as rational for decidable comparison)

def TurcoBraunDimroth2014.instReprProminenceDatum.repr : ProminenceDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TurcoBraunDimroth2014.instReprProminenceDatum : Repr ProminenceDatum

Equations

• TurcoBraunDimroth2014.instReprProminenceDatum = { reprPrec := TurcoBraunDimroth2014.instReprProminenceDatum.repr }

def TurcoBraunDimroth2014.instBEqProminenceDatum.beq : ProminenceDatum → ProminenceDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• TurcoBraunDimroth2014.instBEqProminenceDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance TurcoBraunDimroth2014.instBEqProminenceDatum : BEq ProminenceDatum

Equations

• TurcoBraunDimroth2014.instBEqProminenceDatum = { beq := TurcoBraunDimroth2014.instBEqProminenceDatum.beq }

structure TurcoBraunDimroth2014.AccentRateDatum : Type

An accent-rate datum for Dutch wel (Fig. 3).

• context : Discourse.Coherence.CoherenceRelation
• pctAccented : ℚ

  Percentage of wel tokens that were accented

@[implicit_reducible]

instance TurcoBraunDimroth2014.instReprAccentRateDatum : Repr AccentRateDatum

Equations

• TurcoBraunDimroth2014.instReprAccentRateDatum = { reprPrec := TurcoBraunDimroth2014.instReprAccentRateDatum.repr }

def TurcoBraunDimroth2014.instReprAccentRateDatum.repr : AccentRateDatum → ℕ → Std.Format

Equations

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

def TurcoBraunDimroth2014.instBEqAccentRateDatum.beq : AccentRateDatum → AccentRateDatum → Bool

Equations

• TurcoBraunDimroth2014.instBEqAccentRateDatum.beq { context := a, pctAccented := a_1 } { context := b, pctAccented := b_1 } = (a == b && a_1 == b_1)
• TurcoBraunDimroth2014.instBEqAccentRateDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance TurcoBraunDimroth2014.instBEqAccentRateDatum : BEq AccentRateDatum

Equations

• TurcoBraunDimroth2014.instBEqAccentRateDatum = { beq := TurcoBraunDimroth2014.instBEqAccentRateDatum.beq }

structure TurcoBraunDimroth2014.AccentTypeDatum : Type

Accent type distribution on Dutch wel (Fig. 5). ToDI annotation: !HL L% (downstepped fall) vs HL L% (fall).

• context : Discourse.Coherence.CoherenceRelation
• pctDownsteppedFall : ℚ

  Percentage realized as downstepped fall (!H*L L%)

• pctFall : ℚ

  Percentage realized as plain fall (H*L L%)

• pctOther : ℚ

  Percentage other realizations

@[implicit_reducible]

instance TurcoBraunDimroth2014.instReprAccentTypeDatum : Repr AccentTypeDatum

Equations

• TurcoBraunDimroth2014.instReprAccentTypeDatum = { reprPrec := TurcoBraunDimroth2014.instReprAccentTypeDatum.repr }

def TurcoBraunDimroth2014.instReprAccentTypeDatum.repr : AccentTypeDatum → ℕ → Std.Format

Equations

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

def TurcoBraunDimroth2014.instBEqAccentTypeDatum.beq : AccentTypeDatum → AccentTypeDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• TurcoBraunDimroth2014.instBEqAccentTypeDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance TurcoBraunDimroth2014.instBEqAccentTypeDatum : BEq AccentTypeDatum

Equations

• TurcoBraunDimroth2014.instBEqAccentTypeDatum = { beq := TurcoBraunDimroth2014.instBEqAccentTypeDatum.beq }

Production Strategy Data (Fig. 2: Dutch, Fig. 6: German)

def TurcoBraunDimroth2014.dutchContrast : ProductionDatum

Dutch contrast: ~88% particle, 0% VF, ~5% other, ~7% unmarked

Equations

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

def TurcoBraunDimroth2014.dutchCorrection : ProductionDatum

Dutch correction: ~63% particle, ~5% VF, ~7% other, ~25% unmarked

Equations

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

def TurcoBraunDimroth2014.germanContrast : ProductionDatum

German contrast: 0% particle, ~82% VF, 0% other, ~18% unmarked. "Others" in the paper's coding = doch pre-utterance + VF combinations; these occur only in correction (p. 102).

Equations

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

def TurcoBraunDimroth2014.germanCorrection : ProductionDatum

German correction: 0% particle, ~78% VF, ~8% other, ~14% unmarked. The ~8% "other" = doch pre-utterance followed by VF (p. 102): "always followed by a Verum focus utterance."

Equations

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

def TurcoBraunDimroth2014.allProductionData : List ProductionDatum

Equations

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

Dutch wel Accent Data (Fig. 3)

def TurcoBraunDimroth2014.welAccentContrast : AccentRateDatum

Wel is accented ~93% of the time in contrast contexts.

Equations

• TurcoBraunDimroth2014.welAccentContrast = { context := Discourse.Coherence.CoherenceRelation.contrast, pctAccented := 93 }

def TurcoBraunDimroth2014.welAccentCorrection : AccentRateDatum

Wel is accented ~97% of the time in correction contexts.

Equations

• TurcoBraunDimroth2014.welAccentCorrection = { context := Discourse.Coherence.CoherenceRelation.correction, pctAccented := 97 }

Dutch wel Accent Type Data (Fig. 5)

ToDI annotation (Gussenhoven 2005): in contrast, wel is mostly realized as a downstepped fall (!HL L%); in correction, as a plain fall (HL L%). The plain fall is more prominent.

def TurcoBraunDimroth2014.welTypeContrast : AccentTypeDatum

Contrast: ~60% downstepped fall, ~30% fall, ~10% other

Equations

• TurcoBraunDimroth2014.welTypeContrast = { context := Discourse.Coherence.CoherenceRelation.contrast, pctDownsteppedFall := 60, pctFall := 30, pctOther := 10 }

def TurcoBraunDimroth2014.welTypeCorrection : AccentTypeDatum

Correction: ~30% downstepped fall, ~60% fall, ~10% other

Equations

• TurcoBraunDimroth2014.welTypeCorrection = { context := Discourse.Coherence.CoherenceRelation.correction, pctDownsteppedFall := 30, pctFall := 60, pctOther := 10 }

Prosodic Prominence Data (p. 102)

def TurcoBraunDimroth2014.germanVFContrast : ProminenceDatum

German VF pitch range in contrast: 3.1 semitones. β = −1.85 (contrast is 1.85 ST below correction baseline), SE = 0.39, p < .0001. The regression coefficient is for the contrast condition relative to the correction baseline (correction is the reference level).

Equations

• TurcoBraunDimroth2014.germanVFContrast = { context := Discourse.Coherence.CoherenceRelation.contrast, pitchRangeST := 31 / 10, beta := -185 / 100, se := 39 / 100, pValue := 1 / 10000 }

def TurcoBraunDimroth2014.germanVFCorrection : ProminenceDatum

German VF pitch range in correction: 5.3 semitones. This is the reference level (baseline) in the regression model.

Equations

• TurcoBraunDimroth2014.germanVFCorrection = { context := Discourse.Coherence.CoherenceRelation.correction, pitchRangeST := 53 / 10, beta := 0, se := 0, pValue := 1 }

Verification Theorems — Dominant Strategies

theorem TurcoBraunDimroth2014.dutch_contrast_particle_dominant (s : Semantics.Polarity.Marking.Strategy) : s ≠ Semantics.Polarity.Marking.Strategy.particle → dutchContrast.pctByStrategy Semantics.Polarity.Marking.Strategy.particle > dutchContrast.pctByStrategy s

Dutch dominant strategy is particles in contrast.

theorem TurcoBraunDimroth2014.dutch_correction_particle_dominant (s : Semantics.Polarity.Marking.Strategy) : s ≠ Semantics.Polarity.Marking.Strategy.particle → dutchCorrection.pctByStrategy Semantics.Polarity.Marking.Strategy.particle > dutchCorrection.pctByStrategy s

Dutch dominant strategy is particles in correction.

theorem TurcoBraunDimroth2014.german_contrast_vf_dominant (s : Semantics.Polarity.Marking.Strategy) : s ≠ Semantics.Polarity.Marking.Strategy.verumFocus → germanContrast.pctByStrategy Semantics.Polarity.Marking.Strategy.verumFocus > germanContrast.pctByStrategy s

German dominant strategy is Verum focus in contrast.

theorem TurcoBraunDimroth2014.german_correction_vf_dominant (s : Semantics.Polarity.Marking.Strategy) : s ≠ Semantics.Polarity.Marking.Strategy.verumFocus → germanCorrection.pctByStrategy Semantics.Polarity.Marking.Strategy.verumFocus > germanCorrection.pctByStrategy s

German dominant strategy is Verum focus in correction.

Verification Theorems — German Zero Particles

theorem TurcoBraunDimroth2014.german_contrast_no_particles : germanContrast.pctByStrategy Semantics.Polarity.Marking.Strategy.particle = 0

German has zero sentence-internal particles in contrast.

theorem TurcoBraunDimroth2014.german_correction_no_particles : germanCorrection.pctByStrategy Semantics.Polarity.Marking.Strategy.particle = 0

German has zero sentence-internal particles in correction.

Verification Theorems — Dutch VF Asymmetry

theorem TurcoBraunDimroth2014.dutch_contrast_no_vf : dutchContrast.pctByStrategy Semantics.Polarity.Marking.Strategy.verumFocus = 0

Dutch speakers never use VF in polarity contrast (0%).

theorem TurcoBraunDimroth2014.dutch_vf_correction_only : dutchContrast.pctByStrategy Semantics.Polarity.Marking.Strategy.verumFocus = 0 ∧ dutchCorrection.pctByStrategy Semantics.Polarity.Marking.Strategy.verumFocus > 0

Dutch speakers occasionally use VF in polarity correction (~5%), but never in contrast — an asymmetry the paper notes (p. 102) but does not explain.

Verification Theorems — German doch Correction-Only

The "others" category in German is exclusively doch+VF combinations (p. 102). These appear only in correction, consistent with Env.contrast ∉ dochPreUtterance.environments in the Fragment.

theorem TurcoBraunDimroth2014.german_doch_vf_correction_only : germanContrast.pctByStrategy Semantics.Polarity.Marking.Strategy.other = 0 ∧ germanCorrection.pctByStrategy Semantics.Polarity.Marking.Strategy.other > 0

German "others" (doch+VF) appears only in correction, never contrast.

theorem TurcoBraunDimroth2014.german_doch_production_matches_fragment : Semantics.Polarity.Marking.Env.contrast ∉ German.PolarityMarking.dochPreUtterance.environments ∧ germanContrast.pctByStrategy Semantics.Polarity.Marking.Strategy.other = 0

The production data matches the Fragment: doch is correction-only.

Verification Theorems — Dutch wel Accent

theorem TurcoBraunDimroth2014.wel_mostly_accented : welAccentContrast.pctAccented > 90 ∧ welAccentCorrection.pctAccented > 90

Wel is accented in >90% of tokens in both contexts.

theorem TurcoBraunDimroth2014.correction_favors_fall : welTypeCorrection.pctFall > welTypeCorrection.pctDownsteppedFall ∧ welTypeContrast.pctDownsteppedFall > welTypeContrast.pctFall

Accent type shifts between contexts: correction favors plain fall (HL) over downstepped fall (!HL). The plain fall is more prominent, consistent with the cross-linguistic pattern that correction elicits more prosodic prominence.

Verification Theorems — Prosodic Prominence

theorem TurcoBraunDimroth2014.correction_more_prominent : germanVFCorrection.pitchRangeST > germanVFContrast.pitchRangeST

Correction elicits more prosodic prominence than contrast on German VF.

theorem TurcoBraunDimroth2014.correction_prominence_significant : germanVFContrast.pValue < 5 / 100

The correction–contrast difference is significant (p < .05).

Bridge Theorems — Fragment Connections

theorem TurcoBraunDimroth2014.dominant_strategies_both_marked : Dutch.Particles.wel.strategy ≠ Semantics.Polarity.Marking.Strategy.unmarked ∧ German.PolarityMarking.verumFocus.strategy ≠ Semantics.Polarity.Marking.Strategy.unmarked

Neither Dutch wel nor German VF maps to .unmarked: both languages have overt polarity-marking strategies.

theorem TurcoBraunDimroth2014.strategies_differ : Dutch.Particles.wel.strategy ≠ German.PolarityMarking.verumFocus.strategy

Dutch wel and German VF instantiate different strategy types.

theorem TurcoBraunDimroth2014.dutch_particle_internal_german_doch_not : Semantics.Polarity.Marking.Env.sentenceInternal ∈ Dutch.Particles.wel.environments ∧ Semantics.Polarity.Marking.Env.sentenceInternal ∉ German.PolarityMarking.dochPreUtterance.environments

Dutch wel is sentence-internal; German doch is not. This captures the key typological contrast: Dutch has a sentence-internal particle for polarity switches, German does not.

theorem TurcoBraunDimroth2014.both_strategies_context_general : (Semantics.Polarity.Marking.Env.contrast ∈ Dutch.Particles.wel.environments ∧ Semantics.Polarity.Marking.Env.correction ∈ Dutch.Particles.wel.environments) ∧ Semantics.Polarity.Marking.Env.contrast ∈ German.PolarityMarking.verumFocus.environments ∧ Semantics.Polarity.Marking.Env.correction ∈ German.PolarityMarking.verumFocus.environments

Both Dutch wel and German VF are available in both contexts.

Bridge Theorems — Polarity-Marking Levels

Blühdorn (2012): Dutch wel targets [±Pol] (polarity level); German VF targets the assertion operator (assertion level). This explains why VF can co-occur with negation (emphatic denial) while wel cannot.

theorem TurcoBraunDimroth2014.wel_targets_polarity : strategyLevel Dutch.Particles.wel.strategy = some PolarityMarkingLevel.polarity

Dutch wel targets the polarity level.

theorem TurcoBraunDimroth2014.vf_targets_assertion : strategyLevel German.PolarityMarking.verumFocus.strategy = some PolarityMarkingLevel.assertion

German VF targets the assertion level.

theorem TurcoBraunDimroth2014.strategies_target_different_levels : strategyLevel Dutch.Particles.wel.strategy ≠ strategyLevel German.PolarityMarking.verumFocus.strategy

The two dominant strategies operate at different semantic levels. This is the paper's key theoretical claim (p. 104).

Cross-Linguistic Extension

[TBD14] compare Dutch and German; the analysis naturally extends to other Western European languages with comparable polarity-marking inventories: English (emphatic do), French (si), Swedish (jo), Spanish (sí (que)), Italian (sì che). See also [Hol16], [BH13], [Wil13], [GJ18].

We aggregate the seven-language sample and verify the strategy–level, correction-only, context-general, and sentence-internality generalizations as quantified statements over the inventory rather than as individual per-entry rfls.

def TurcoBraunDimroth2014.allEntries : List Semantics.Polarity.Marking.Entry

All polarity-marking entries across the seven-language sample.

Equations

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

theorem TurcoBraunDimroth2014.strategy_level_partition (e : Semantics.Polarity.Marking.Entry) : e ∈ allEntries → (e.strategy = Semantics.Polarity.Marking.Strategy.particle ∨ e.strategy = Semantics.Polarity.Marking.Strategy.polarityReversal → strategyLevel e.strategy = some PolarityMarkingLevel.polarity) ∧ (e.strategy = Semantics.Polarity.Marking.Strategy.verumFocus → strategyLevel e.strategy = some PolarityMarkingLevel.assertion)

Generalization 1 — Strategy/level mapping. Every particle and polarity-reversal entry targets the polarity level; every Verum-focus entry targets the assertion level.

theorem TurcoBraunDimroth2014.all_reversal_license_correction (e : Semantics.Polarity.Marking.Entry) : e ∈ allEntries → e.strategy = Semantics.Polarity.Marking.Strategy.polarityReversal → Semantics.Polarity.Marking.Env.correction ∈ e.environments

Generalization 2 — Reversal particles license correction. Every polarity-reversal entry has .correction present in environments. The earlier "correction-only" version of this generalization (also asserting .contrast ∉ e.environments) was falsified by Italian sì che and Spanish sí que per [GJ18] ex. 17 + [BH13] ex. 4-5 (both license non-contradictory contrast contexts). The surviving cross-linguistic generalization is the correction direction only.

theorem TurcoBraunDimroth2014.all_nonreversal_context_general (e : Semantics.Polarity.Marking.Entry) : e ∈ allEntries → e.strategy = Semantics.Polarity.Marking.Strategy.particle ∨ e.strategy = Semantics.Polarity.Marking.Strategy.verumFocus → Semantics.Polarity.Marking.Env.contrast ∈ e.environments ∧ Semantics.Polarity.Marking.Env.correction ∈ e.environments

Generalization 3 — Non-reversal strategies are context-general. Every particle or Verum-focus entry has both .contrast and .correction present in environments.

theorem TurcoBraunDimroth2014.sentence_internality_by_strategy (e : Semantics.Polarity.Marking.Entry) : e ∈ allEntries → (e.strategy = Semantics.Polarity.Marking.Strategy.polarityReversal → Semantics.Polarity.Marking.Env.sentenceInternal ∉ e.environments) ∧ (e.strategy = Semantics.Polarity.Marking.Strategy.particle ∨ e.strategy = Semantics.Polarity.Marking.Strategy.verumFocus → Semantics.Polarity.Marking.Env.sentenceInternal ∈ e.environments)

Generalization 4 — Sentence-internality splits by strategy type. Polarity-reversal entries are not sentence-internal; particles and Verum-focus entries are.