PPCDRT — Cumulativity Bridge

@cite{langendoen-1978} @cite{haug-dalrymple-2020}

@cite{langendoen-1978} first observed that reciprocity is a species of cumulativity: in the women pointed at each other, every woman points at some other woman and every woman is pointed at by some other woman. @cite{haug-dalrymple-2020} §1 reaffirms this. The link is structural: the PPCDRT condition groupIdentityCond u_anaph u_ant (Plurality.Cumulativity is the bidirectional-coverage version of equality on the value-sets ∪u_anaph(S) = ∪u_ant(S)) collapses to Cumulative (· = ·) on the Finset of value pairs.

The Plurality/Cumulativity.lean substrate is Prop-valued over Finset × Finset (with a Decidable instance), while PPCDRT is also Prop-valued over PluralAssign. The bridge theorem under [DecidableEq E] and finiteness assumptions on the value-sets establishes the structural identity that the original Reference/Reciprocals.lean docstring asserted as prose.

theorem Theories.Semantics.Dynamic.PPCDRT.cumulative_eq_iff_finset_eq {E : Type} [DecidableEq E] (x y : Finset E) : Semantics.Plurality.Cumulativity.Cumulative (fun (a b : E) => a = b) x y ↔ x = y

The cumulative operator ** of @cite{krifka-1989}/Beck-Sauerland on the equality relation reduces to Finset equality.

This is the structural identity behind the Langendoen reciprocity-as- cumulativity claim: bidirectional value-coverage IS the equality of value sets.

⊆ direction: if Cumulative (· = ·) x y, then for every a ∈ x there is b ∈ y with a = b, so a ∈ y; and symmetrically. ⊇ direction: if x = y, every element witnesses itself.

theorem Theories.Semantics.Dynamic.PPCDRT.groupIdentityCond_iff_cumulative_eq {E : Type} [DecidableEq E] (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (xa xb : Finset E) (hxa : ∀ (d : E), d ∈ xa ↔ d ∈ S.sumDref uAnaph) (hxb : ∀ (d : E), d ∈ xb ↔ d ∈ S.sumDref uAnt) : groupIdentityCond uAnaph uAnt S ∅ ↔ Semantics.Plurality.Cumulativity.Cumulative (fun (a b : E) => a = b) xa xb

Bridge: when the value-sets of the two drefs across the plural state are given as Finsets matching sumDref, group identity holds iff those Finsets are equal — iff Cumulative (· = ·) returns true.

The hypothesis is stated as Set membership on sumDref because Set E → Finset E requires Set.Finite, which is downstream of the consumer's choice of value domain. Concrete H&D examples (Phase 4) instantiate this with [Fintype] toy domains where the value-sets are automatically finite.

This theorem is the formal realisation of @cite{langendoen-1978}'s reciprocity-as-cumulativity claim within PPCDRT.