Copredication: @cite{gotham-2017}'s account + bridge data

@cite{asher-2011} @cite{gotham-2017} @cite{pustejovsky-1995} @cite{chatzikyriakidis-etal-2025}

Copredication is the phenomenon where predicates selecting different semantic aspects apply to the same polysemous noun phrase ("the book is heavy and interesting"). This study file owns:

1. The TTR dot-type infrastructure (formerly Theories/Semantics/TypeTheoretic/Copredication.lean, absorbed here as the only consumer per linglib's substrate-by-need rule).
2. The canonical empirical data (formerly Polysemy/Data.lean, dissolved per the provenance-tracking policy).
3. Bridge theorems connecting (1) and (2).

Empirical phenomena

1. Book copredication: "The book is heavy and interesting" — heavy selects physical object, interesting selects informational content.
2. Counting under copredication: "Three books were mastered and burned" — ambiguous between counting physical volumes vs. informational contents.
3. Lunch copredication: "The lunch was delicious but took forever" — delicious selects food, took forever selects event.

Bridge theorems

1. Copredication is well-typed via meet-type projection.
2. Different individuation criteria yield different counts.
3. The counting puzzle from @cite{gotham-2017} is reproduced.

Copredication

Copredication applies predicates selecting different aspects to the same pair-typed argument. The aspects are accessed via Prod.fst/.snd projections (= the MeetType projections in TTR's Core).

def Phenomena.Polysemy.copred₁ {A₁ A₂ : Type} (P : A₁ → Prop) (x : A₁ × A₂) : Prop

Apply a predicate selecting the first aspect.

Equations

• Phenomena.Polysemy.copred₁ P x = P x.1

def Phenomena.Polysemy.copred₂ {A₁ A₂ : Type} (P : A₂ → Prop) (x : A₁ × A₂) : Prop

Apply a predicate selecting the second aspect.

Equations

• Phenomena.Polysemy.copred₂ P x = P x.2

def Phenomena.Polysemy.copredicate {A₁ A₂ : Type} (P : A₁ → Prop) (Q : A₂ → Prop) (x : A₁ × A₂) : Prop

Copredication: conjunction of predicates on different aspects. "The book is heavy and interesting" = heavy(book.phys) ∧ interesting(book.info).

Equations

• Phenomena.Polysemy.copredicate P Q x = (P x.1 ∧ Q x.2)

theorem Phenomena.Polysemy.copredicate_factors {A₁ A₂ : Type} (P : A₁ → Prop) (Q : A₂ → Prop) (x : A₁ × A₂) : copredicate P Q x ↔ copred₁ P x ∧ copred₂ Q x

Copredication factors into independent aspect predicates.

Dot types

A dot type bundles two aspect types with a Setoid for individuation. The individuation is part of the lexical specification — "book" = ⟨PhysObj, Info, individuate by volume⟩ — not just the raw product type.

Values of a dot type are pairs A₁ × A₂ (= MeetType A₁ A₂ in TTR).

structure Phenomena.Polysemy.DotType (A₁ A₂ : Type) : Type

A dot type: a polysemous type with two aspects and an individuation criterion (a Setoid). The individuation determines counting under copredication. @cite{chatzikyriakidis-etal-2025} §3.

• individuation : Setoid (A₁ × A₂)

  How to individuate objects of this complex type

def Phenomena.Polysemy.DotType.byAspect₁ {A₁ A₂ : Type} [DecidableEq A₁] : DotType A₁ A₂

Individuate by the first aspect. "book" individuated physically: two copies of Hamlet count as two.

Equations

• Phenomena.Polysemy.DotType.byAspect₁ = { individuation := { r := fun (x y : A₁ × A₂) => x.1 = y.1, iseqv := ⋯ } }

def Phenomena.Polysemy.DotType.byAspect₂ {A₁ A₂ : Type} [DecidableEq A₂] : DotType A₁ A₂

Individuate by the second aspect. "book" individuated informationally: two copies of Hamlet count as one.

Equations

• Phenomena.Polysemy.DotType.byAspect₂ = { individuation := { r := fun (x y : A₁ × A₂) => x.2 = y.2, iseqv := ⋯ } }

def Phenomena.Polysemy.countDistinct {α : Type} (s : Setoid α) [(x y : α) → Decidable (s x y)] (xs : List α) : ℕ

Count distinct individuals in a list under a Setoid. Uses a simple quadratic distinctness check (fine for finite linguistic examples).

Equations

• Phenomena.Polysemy.countDistinct s xs = (List.foldl (fun (seen : List α) (x : α) => if (seen.any fun (e : α) => decide (s e x)) = true then seen else x :: seen) [] xs).length

theorem Phenomena.Polysemy.individuation_can_diverge : ∃ (A₁ : Type) (A₂ : Type) (x : DecidableEq A₁) (x_1 : DecidableEq A₂) (xs : List (A₁ × A₂)) (x_2 : (x_2 y : A₁ × A₂) → Decidable (DotType.byAspect₁.individuation x_2 y)) (x_3 : (x y : A₁ × A₂) → Decidable (DotType.byAspect₂.individuation x y)), countDistinct DotType.byAspect₁.individuation xs ≠ countDistinct DotType.byAspect₂.individuation xs

Different individuation criteria can yield different counts for the same collection. This is the formal content of @cite{chatzikyriakidis-etal-2025} §3's counting puzzle.

inductive Phenomena.Polysemy.Acceptability : Type

Acceptability judgment for copredication examples.

• acceptable : Acceptability
• marginal : Acceptability
• unacceptable : Acceptability

def Phenomena.Polysemy.instReprAcceptability.repr : Acceptability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polysemy.instReprAcceptability : Repr Acceptability

Equations

• Phenomena.Polysemy.instReprAcceptability = { reprPrec := Phenomena.Polysemy.instReprAcceptability.repr }

@[implicit_reducible]

instance Phenomena.Polysemy.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

• Phenomena.Polysemy.instDecidableEqAcceptability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Polysemy.CopredDatum : Type

A copredication datum: a sentence with two predicates on different aspects.

• sentence : String

  The sentence

• noun : String

  The polysemous noun

• aspect₁ : String

  The aspect selected by the first predicate

• aspect₂ : String

  The aspect selected by the second predicate

• judgment : Acceptability

  Acceptability judgment

@[implicit_reducible]

instance Phenomena.Polysemy.instReprCopredDatum : Repr CopredDatum

Equations

• Phenomena.Polysemy.instReprCopredDatum = { reprPrec := Phenomena.Polysemy.instReprCopredDatum.repr }

def Phenomena.Polysemy.instReprCopredDatum.repr : CopredDatum → ℕ → Std.Format

Equations

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

def Phenomena.Polysemy.bookHeavyInteresting : CopredDatum

The canonical book copredication example.

Equations

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

def Phenomena.Polysemy.lunchDeliciousLong : CopredDatum

Lunch copredication: food + event aspects.

Equations

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

def Phenomena.Polysemy.newspaperFiredTore : CopredDatum

Newspaper copredication: organization + physical aspects.

Equations

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

structure Phenomena.Polysemy.CountingDatum : Type

A counting-under-copredication datum.

• sentence : String

  The sentence

• noun : String

  The polysemous noun

• physicalCount : ℕ

  Count under physical individuation

• informationalCount : ℕ

  Count under informational individuation

• countsDiverge : Bool

  Whether the two counts diverge

@[implicit_reducible]

instance Phenomena.Polysemy.instReprCountingDatum : Repr CountingDatum

Equations

• Phenomena.Polysemy.instReprCountingDatum = { reprPrec := Phenomena.Polysemy.instReprCountingDatum.repr }

def Phenomena.Polysemy.instReprCountingDatum.repr : CountingDatum → ℕ → Std.Format

Equations

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

def Phenomena.Polysemy.masteredAndBurned : CountingDatum

"Three books were mastered and burned" with two copies of the same novel. @cite{gotham-2017}: physical count = 3, informational count = 2 (if one novel has two copies).

Equations

• Phenomena.Polysemy.masteredAndBurned = { sentence := "Three books were mastered and burned", noun := "book", physicalCount := 3, informationalCount := 2, countsDiverge := true }

def Phenomena.Polysemy.copredData : List CopredDatum

All copredication data points.

Equations

• Phenomena.Polysemy.copredData = [Phenomena.Polysemy.bookHeavyInteresting, Phenomena.Polysemy.lunchDeliciousLong, Phenomena.Polysemy.newspaperFiredTore]

theorem Phenomena.Polysemy.all_copred_acceptable (d : CopredDatum) : d ∈ copredData → d.judgment = Acceptability.acceptable

All copredication data points are acceptable.

Book as a dot type

structure Phenomena.Polysemy.Bridge.PhysObj : Type

Physical-object aspect of a book.

• weight : ℕ

def Phenomena.Polysemy.Bridge.instReprPhysObj.repr : PhysObj → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polysemy.Bridge.instReprPhysObj : Repr PhysObj

Equations

• Phenomena.Polysemy.Bridge.instReprPhysObj = { reprPrec := Phenomena.Polysemy.Bridge.instReprPhysObj.repr }

def Phenomena.Polysemy.Bridge.instDecidableEqPhysObj.decEq (x✝ x✝¹ : PhysObj) : Decidable (x✝ = x✝¹)

Equations

• Phenomena.Polysemy.Bridge.instDecidableEqPhysObj.decEq { weight := a } { weight := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Polysemy.Bridge.instDecidableEqPhysObj : DecidableEq PhysObj

Equations

• Phenomena.Polysemy.Bridge.instDecidableEqPhysObj = Phenomena.Polysemy.Bridge.instDecidableEqPhysObj.decEq

structure Phenomena.Polysemy.Bridge.Info : Type

Informational-content aspect of a book.

• title : String

@[implicit_reducible]

instance Phenomena.Polysemy.Bridge.instReprInfo : Repr Info

Equations

• Phenomena.Polysemy.Bridge.instReprInfo = { reprPrec := Phenomena.Polysemy.Bridge.instReprInfo.repr }

def Phenomena.Polysemy.Bridge.instReprInfo.repr : Info → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polysemy.Bridge.instDecidableEqInfo : DecidableEq Info

Equations

• Phenomena.Polysemy.Bridge.instDecidableEqInfo = Phenomena.Polysemy.Bridge.instDecidableEqInfo.decEq

def Phenomena.Polysemy.Bridge.instDecidableEqInfo.decEq (x✝ x✝¹ : Info) : Decidable (x✝ = x✝¹)

Equations

• Phenomena.Polysemy.Bridge.instDecidableEqInfo.decEq { title := a } { title := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Phenomena.Polysemy.Bridge.bookDot : DotType PhysObj Info

"book" as a dot type: physical × informational, individuated physically. @cite{gotham-2017}: the default criterion for "book" counts physical volumes.

Equations

• Phenomena.Polysemy.Bridge.bookDot = Phenomena.Polysemy.DotType.byAspect₁

def Phenomena.Polysemy.Bridge.heavy (threshold : ℕ) (p : PhysObj) : Prop

"heavy": a predicate on the physical aspect.

Equations

• Phenomena.Polysemy.Bridge.heavy threshold p = (p.weight > threshold)

def Phenomena.Polysemy.Bridge.interesting (_i : Info) : Prop

"interesting": a predicate on the informational aspect.

Equations

• Phenomena.Polysemy.Bridge.interesting _i = True

theorem Phenomena.Polysemy.Bridge.book_heavy_and_interesting (b : PhysObj × Info) (h : b.1.weight > 500) : copredicate (heavy 500) interesting b

"The book is heavy and interesting" is well-typed copredication. This is the formal content of bookHeavyInteresting from Data.lean.

Counting under copredication

Model the scenario from @cite{gotham-2017} / @cite{chatzikyriakidis-etal-2025} §3: Two physical copies of one novel, plus one copy of a different novel. Physical count = 3, informational count = 2.

def Phenomena.Polysemy.Bridge.hamlet1 : PhysObj × Info

Three books: two copies of "Hamlet" and one of "Ulysses".

Equations

• Phenomena.Polysemy.Bridge.hamlet1 = ({ weight := 200 }, { title := "Hamlet" })

def Phenomena.Polysemy.Bridge.hamlet2 : PhysObj × Info

Equations

• Phenomena.Polysemy.Bridge.hamlet2 = ({ weight := 210 }, { title := "Hamlet" })

def Phenomena.Polysemy.Bridge.ulysses : PhysObj × Info

Equations

• Phenomena.Polysemy.Bridge.ulysses = ({ weight := 400 }, { title := "Ulysses" })

def Phenomena.Polysemy.Bridge.threeBooks : List (PhysObj × Info)

Equations

• Phenomena.Polysemy.Bridge.threeBooks = [Phenomena.Polysemy.Bridge.hamlet1, Phenomena.Polysemy.Bridge.hamlet2, Phenomena.Polysemy.Bridge.ulysses]

@[implicit_reducible]

instance Phenomena.Polysemy.Bridge.instDecidableRProdPhysObjInfo (x y : PhysObj × Info) : Decidable (bookDot.individuation x y)

Physical individuation: count by PhysObj (weight distinguishes copies).

Equations

• Phenomena.Polysemy.Bridge.instDecidableRProdPhysObjInfo x y = Phenomena.Polysemy.Bridge.instDecidableRProdPhysObjInfo._aux_1 x y

def Phenomena.Polysemy.Bridge.infoDot : DotType PhysObj Info

Informational individuation: count by Info (title).

Equations

• Phenomena.Polysemy.Bridge.infoDot = Phenomena.Polysemy.DotType.byAspect₂

@[implicit_reducible]

instance Phenomena.Polysemy.Bridge.instDecidableRProdPhysObjInfo_1 (x y : PhysObj × Info) : Decidable (infoDot.individuation x y)

Equations

• Phenomena.Polysemy.Bridge.instDecidableRProdPhysObjInfo_1 x y = Phenomena.Polysemy.Bridge.instDecidableRProdPhysObjInfo_1._aux_1 x y

theorem Phenomena.Polysemy.Bridge.physical_count : countDistinct bookDot.individuation threeBooks = 3

Under physical individuation: 3 distinct objects.

theorem Phenomena.Polysemy.Bridge.informational_count : countDistinct infoDot.individuation threeBooks = 2

Under informational individuation: 2 distinct contents.

theorem Phenomena.Polysemy.Bridge.counting_matches_datum : countDistinct bookDot.individuation threeBooks = masteredAndBurned.physicalCount ∧ countDistinct infoDot.individuation threeBooks = masteredAndBurned.informationalCount

The counting datum from Data.lean is reproduced. This bridges the empirical datum to the TTR formalization.

theorem Phenomena.Polysemy.Bridge.counts_diverge : countDistinct bookDot.individuation threeBooks ≠ countDistinct infoDot.individuation threeBooks

Counts diverge, as predicted by the datum.