inductive HaslingerEtAl2025.SyntacticUse : Type

Syntactic distribution of a distributive element

• dpInternal : SyntacticUse
• distance : SyntacticUse

@[implicit_reducible]

instance HaslingerEtAl2025.instDecidableEqSyntacticUse : DecidableEq SyntacticUse

Equations

• HaslingerEtAl2025.instDecidableEqSyntacticUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HaslingerEtAl2025.instReprSyntacticUse.repr : SyntacticUse → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaslingerEtAl2025.instReprSyntacticUse : Repr SyntacticUse

Equations

• HaslingerEtAl2025.instReprSyntacticUse = { reprPrec := HaslingerEtAl2025.instReprSyntacticUse.repr }

structure HaslingerEtAl2025.LexicalItem : Type

A German distributive item with its properties

• form : String
• gloss : String
• uses : List SyntacticUse
• semanticClass : Semantics.Plurality.Distributivity.DistMaxClass

def HaslingerEtAl2025.instReprLexicalItem.repr : LexicalItem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaslingerEtAl2025.instReprLexicalItem : Repr LexicalItem

Equations

• HaslingerEtAl2025.instReprLexicalItem = { reprPrec := HaslingerEtAl2025.instReprLexicalItem.repr }

def HaslingerEtAl2025.LexicalItem.ofEntry (e : German.Distributives.DistributiveEntry) : LexicalItem

Derive a LexicalItem from the German distributive Fragment entry, so the form/gloss/classification are read off Fragments/German/Distributives.lean rather than restated here (the fragment is anchored to this same paper).

Equations

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

def HaslingerEtAl2025.jeder : LexicalItem

jeder (DP-internal and distance): +distributive, +maximal. Derived from the German fragment's jederEntry.

Equations

• HaslingerEtAl2025.jeder = HaslingerEtAl2025.LexicalItem.ofEntry German.Distributives.jederEntry

def HaslingerEtAl2025.jeweils : LexicalItem

jeweils (distance only): +distributive, -maximal. Derived from jeweilsEntry.

Equations

• HaslingerEtAl2025.jeweils = HaslingerEtAl2025.LexicalItem.ofEntry German.Distributives.jeweilsEntry

def HaslingerEtAl2025.alle : LexicalItem

alle (DP-internal): -distributive, +maximal. Derived from alleEntry.

Equations

• HaslingerEtAl2025.alle = HaslingerEtAl2025.LexicalItem.ofEntry German.Distributives.alleEntry

def HaslingerEtAl2025.definitePlural : LexicalItem

Definite plurals: -distributive, -maximal

Equations

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

structure HaslingerEtAl2025.NonMaxContext : Type

Context for testing non-maximality (QUD makes exceptions irrelevant)

• description : String
• totalItems : ℕ
• exceptions : ℕ
• implicitQUD : String

@[implicit_reducible]

instance HaslingerEtAl2025.instReprNonMaxContext : Repr NonMaxContext

Equations

• HaslingerEtAl2025.instReprNonMaxContext = { reprPrec := HaslingerEtAl2025.instReprNonMaxContext.repr }

def HaslingerEtAl2025.instReprNonMaxContext.repr : NonMaxContext → ℕ → Std.Format

Equations

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

def HaslingerEtAl2025.magnetsContext : NonMaxContext

Magnets scenario (example 23): 5 boxes, 4 have 2 magnets, 1 has 1

Equations

• HaslingerEtAl2025.magnetsContext = { description := "Magnets that shouldn't be stored together", totalItems := 5, exceptions := 1, implicitQUD := "Is there explosion risk?" }

def HaslingerEtAl2025.volunteersContext : NonMaxContext

Volunteers scenario (example 24): 5 volunteers, 4 have 2 dogs, 1 has 1

Equations

• HaslingerEtAl2025.volunteersContext = { description := "Attack dogs that shouldn't be walked together", totalItems := 5, exceptions := 1, implicitQUD := "Is there a dog fight risk?" }

structure HaslingerEtAl2025.Observation : Type

Experimental observation

• item : LexicalItem
• context : NonMaxContext
• pattern : String

  Qualitative acceptance pattern from Figures 1-2

@[implicit_reducible]

instance HaslingerEtAl2025.instReprObservation : Repr Observation

Equations

• HaslingerEtAl2025.instReprObservation = { reprPrec := HaslingerEtAl2025.instReprObservation.repr }

def HaslingerEtAl2025.instReprObservation.repr : Observation → ℕ → Std.Format

Equations

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

def HaslingerEtAl2025.dpJederInNonMax : Observation

DP-jeder overwhelmingly rejected in non-maximal contexts (Figure 1)

Equations

• HaslingerEtAl2025.dpJederInNonMax = { item := HaslingerEtAl2025.jeder, context := HaslingerEtAl2025.magnetsContext, pattern := "overwhelmingly rejected (modal rating 1)" }

def HaslingerEtAl2025.jeweilsInNonMax : Observation

jeweils shows mixed judgments across speakers (Figure 1)

Equations

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

def HaslingerEtAl2025.distanceJederInNonMax : Observation

Distance jeder mostly rejected, less categorically than DP-jeder (Figure 2)

Equations

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

theorem HaslingerEtAl2025.independence_attested : (jeder.semanticClass.isDistributive ↔ jeweils.semanticClass.isDistributive) ∧ jeder.semanticClass ≠ jeweils.semanticClass

The independence claim: same distributivity, different maximality

def HaslingerEtAl2025.hasDPUse (item : LexicalItem) : Bool

Correlation (Section 4): No DP use ↔ permits non-maximality?

Equations

• HaslingerEtAl2025.hasDPUse item = item.uses.contains HaslingerEtAl2025.SyntacticUse.dpInternal

def HaslingerEtAl2025.typologyTable : List (String × Semantics.Plurality.Distributivity.DistMaxClass)

The typological table (5) from the paper, extended with jeweils

Equations

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

theorem HaslingerEtAl2025.all_four_cells_populated : (∃ e ∈ typologyTable, e.2 = Semantics.Plurality.Distributivity.DistMaxClass.distMax) ∧ (∃ e ∈ typologyTable, e.2 = Semantics.Plurality.Distributivity.DistMaxClass.distNonMax) ∧ (∃ e ∈ typologyTable, e.2 = Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax) ∧ ∃ e ∈ typologyTable, e.2 = Semantics.Plurality.Distributivity.DistMaxClass.nonDistNonMax

All four cells of the 2×2 are populated

Demonstrate the jeder/jeweils contrast on a concrete model.

5 boxes, predicate "contains two magnets":

• Boxes 1-4: contain 2 magnets (satisfy P)
• Box 5: contains 1 magnet (exception)

QUD: "Is there explosion risk?" — any box with 2 magnets is dangerous, so the exception in box 5 is irrelevant.

• distMaximal rejects: not all boxes have 2 magnets
• distTolerant with a tolerance that accepts 4/5 sub-plurality: accepts

inductive HaslingerEtAl2025.Box : Type

• b1 : Box
• b2 : Box
• b3 : Box
• b4 : Box
• b5 : Box

@[implicit_reducible]

instance HaslingerEtAl2025.instDecidableEqBox : DecidableEq Box

Equations

• HaslingerEtAl2025.instDecidableEqBox x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HaslingerEtAl2025.instReprBox : Repr Box

Equations

• HaslingerEtAl2025.instReprBox = { reprPrec := HaslingerEtAl2025.instReprBox.repr }

def HaslingerEtAl2025.instReprBox.repr : Box → ℕ → Std.Format

Equations

• HaslingerEtAl2025.instReprBox.repr HaslingerEtAl2025.Box.b1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HaslingerEtAl2025.Box.b1")).group prec✝
• HaslingerEtAl2025.instReprBox.repr HaslingerEtAl2025.Box.b2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HaslingerEtAl2025.Box.b2")).group prec✝
• HaslingerEtAl2025.instReprBox.repr HaslingerEtAl2025.Box.b3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HaslingerEtAl2025.Box.b3")).group prec✝
• HaslingerEtAl2025.instReprBox.repr HaslingerEtAl2025.Box.b4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HaslingerEtAl2025.Box.b4")).group prec✝
• HaslingerEtAl2025.instReprBox.repr HaslingerEtAl2025.Box.b5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HaslingerEtAl2025.Box.b5")).group prec✝

@[implicit_reducible]

instance HaslingerEtAl2025.instFintypeBox : Fintype Box

Equations

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

inductive HaslingerEtAl2025.MWorld : Type

World with 4 of 5 boxes containing 2 magnets

• actual : MWorld

@[implicit_reducible]

instance HaslingerEtAl2025.instDecidableEqMWorld : DecidableEq MWorld

Equations

• HaslingerEtAl2025.instDecidableEqMWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HaslingerEtAl2025.instReprMWorld : Repr MWorld

Equations

• HaslingerEtAl2025.instReprMWorld = { reprPrec := HaslingerEtAl2025.instReprMWorld.repr }

def HaslingerEtAl2025.instReprMWorld.repr : MWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaslingerEtAl2025.instFintypeMWorld : Fintype MWorld

Equations

• HaslingerEtAl2025.instFintypeMWorld = { elems := {HaslingerEtAl2025.MWorld.actual}, complete := HaslingerEtAl2025.instFintypeMWorld._proof_1 }

def HaslingerEtAl2025.hasTwoMagnets : Box → MWorld → Prop

"This box contains two magnets"

Equations

• HaslingerEtAl2025.hasTwoMagnets HaslingerEtAl2025.Box.b1 x✝ = True
• HaslingerEtAl2025.hasTwoMagnets HaslingerEtAl2025.Box.b2 x✝ = True
• HaslingerEtAl2025.hasTwoMagnets HaslingerEtAl2025.Box.b3 x✝ = True
• HaslingerEtAl2025.hasTwoMagnets HaslingerEtAl2025.Box.b4 x✝ = True
• HaslingerEtAl2025.hasTwoMagnets HaslingerEtAl2025.Box.b5 x✝ = False

@[implicit_reducible]

instance HaslingerEtAl2025.hasTwoMagnets.instDecidable (b : Box) (w : MWorld) : Decidable (hasTwoMagnets b w)

Equations

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

def HaslingerEtAl2025.allBoxes : Finset Box

Equations

• HaslingerEtAl2025.allBoxes = Finset.univ

theorem HaslingerEtAl2025.jeder_rejects_magnets : ¬Semantics.Plurality.distMaximal hasTwoMagnets allBoxes MWorld.actual

jeder rejects: not all boxes have 2 magnets

theorem HaslingerEtAl2025.jeweils_accepts_magnets : Semantics.Plurality.Distributivity.distTolerant hasTwoMagnets Semantics.Plurality.Tolerance.trivial allBoxes MWorld.actual

jeweils accepts: there exists a sub-plurality where all boxes have 2 magnets. We use trivial tolerance (any subset is tolerant) — the 4-box subset {b1,b2,b3,b4} witnesses truth because all four satisfy hasTwoMagnets.

theorem HaslingerEtAl2025.each_box_maximal (b : Box) : Semantics.Plurality.distMaximal hasTwoMagnets {b} MWorld.actual ↔ hasTwoMagnets b MWorld.actual

The atom-vacuity principle in action: distributing to individual boxes, maximality follows because each singleton has no room for tolerance.