Copredication Bridge @cite{chatzikyriakidis-etal-2025}

@cite{gotham-2017}

Bridge theorems connecting copredication data to the TTR dot-type infrastructure. We model the "book" examples from §3 of @cite{chatzikyriakidis-etal-2025} and prove that:

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

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.

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 ⋯

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

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.

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 ⋯

instance Phenomena.Polysemy.Bridge.instDecidableEqInfo : DecidableEq Info

Equations

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

def Phenomena.Polysemy.Bridge.bookDot : Semantics.TypeTheoretic.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 = Semantics.TypeTheoretic.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) : Semantics.TypeTheoretic.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]

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 = inferInstanceAs (Decidable (x.1 = y.1))

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

Informational individuation: count by Info (title).

Equations

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

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

Equations

• Phenomena.Polysemy.Bridge.instDecidableRProdPhysObjInfo_1 x y = inferInstanceAs (Decidable (x.2 = y.2))

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

Under physical individuation: 3 distinct objects.

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

Under informational individuation: 2 distinct contents.

theorem Phenomena.Polysemy.Bridge.counting_matches_datum : Semantics.TypeTheoretic.countDistinct bookDot.individuation threeBooks = masteredAndBurned.physicalCount ∧ Semantics.TypeTheoretic.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 : Semantics.TypeTheoretic.countDistinct bookDot.individuation threeBooks ≠ Semantics.TypeTheoretic.countDistinct infoDot.individuation threeBooks

Counts diverge, as predicted by the datum.