Interaction, Satisfaction, and the PCC @cite{deal-2024} #

@cite{deal-2024} unifies the Person Case Constraint (PCC) typology under a single Agree operation with two independently parameterized conditions:

Interaction (INT): what features the probe copies from a goal.
Satisfaction (SAT): what features halt the probe.

The probe encounters DO first ("DO preference"). If DO satisfies the probe, it halts before reaching IO — creating a PCC violation when IO requires licensing. If DO does not satisfy, the probe copies DO's features and continues to IO. Dynamic interaction narrows the probe's subsequent INT condition based on what was copied from DO.

PCC Typology #

Two parameters — satisfaction feature and dynamic interaction configuration — derive five attested PCC varieties:

SAT	DynINT	PCC type	Licit
[PART]	none	Strong	3
[SPKR]	none	Me-first	6
none	[PART]↑	Weak	7
[SPKR]	[PART]↑	Strictly descending	5
none	none	No PCC	9

Bridge Results #

This study file connects @cite{deal-2024}'s framework to both:

@cite{pancheva-zubizarreta-2018} (PConstraint.lean): exact match for Strong, Weak, and Me-first (all 9 cells); 7/9 match for Strictly Descending vs Ultra-strong (discrepancies on reflexive SAP combinations).
@cite{bejar-rezac-2009} (CyclicAgree.lean): probe satisfaction in Deal's sense corresponds to residue depletion in cyclic Agree — a DP satisfies SAT:[PART] iff it depletes the partial probe's residue.

source

inductive Phenomena.Agreement.Studies.Deal2024.PersonFeature :

Type

Person features in @cite{deal-2024}'s geometry.

[φ] → [PART] → [SPKR]
             → [ADDR]

Maps onto DecomposedPerson: [PART] = hasParticipant, [SPKR] = hasAuthor, [ADDR] = (person == .second).

Instances For

source

instance Phenomena.Agreement.Studies.Deal2024.instDecidableEqPersonFeature :

DecidableEq PersonFeature

Equations

Phenomena.Agreement.Studies.Deal2024.instDecidableEqPersonFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Agreement.Studies.Deal2024.instBEqPersonFeature.beq :

PersonFeature → PersonFeature → Bool

Equations

Phenomena.Agreement.Studies.Deal2024.instBEqPersonFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Agreement.Studies.Deal2024.instBEqPersonFeature :

BEq PersonFeature

Equations

Phenomena.Agreement.Studies.Deal2024.instBEqPersonFeature = { beq := Phenomena.Agreement.Studies.Deal2024.instBEqPersonFeature.beq }

source

def Phenomena.Agreement.Studies.Deal2024.instReprPersonFeature.repr :

PersonFeature → Nat → Std.Format

Equations

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

Instances For

source

instance Phenomena.Agreement.Studies.Deal2024.instReprPersonFeature :

Repr PersonFeature

Equations

Phenomena.Agreement.Studies.Deal2024.instReprPersonFeature = { reprPrec := Phenomena.Agreement.Studies.Deal2024.instReprPersonFeature.repr }

source

inductive Phenomena.Agreement.Studies.Deal2024.DynInteraction :

Type

Dynamic interaction configurations.

After copying features from DO, the probe's subsequent INT condition may narrow. The ↑ notation indicates which features trigger narrowing.

none_: no dynamic narrowing
part: [PART]↑ — if DO bears [PART], INT narrows to [PART]
spkr: [SPKR]↑ — if DO bears [SPKR], INT narrows to [SPKR]
partAndSpkr: both [PART]↑ and [SPKR]↑ — [SPKR]↑ takes priority

none_ : DynInteraction
part : DynInteraction
spkr : DynInteraction
partAndSpkr : DynInteraction

Instances For

source

instance Phenomena.Agreement.Studies.Deal2024.instDecidableEqDynInteraction :

DecidableEq DynInteraction

Equations

Phenomena.Agreement.Studies.Deal2024.instDecidableEqDynInteraction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Agreement.Studies.Deal2024.instBEqDynInteraction.beq :

DynInteraction → DynInteraction → Bool

Equations

Phenomena.Agreement.Studies.Deal2024.instBEqDynInteraction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Agreement.Studies.Deal2024.instBEqDynInteraction :

BEq DynInteraction

Equations

Phenomena.Agreement.Studies.Deal2024.instBEqDynInteraction = { beq := Phenomena.Agreement.Studies.Deal2024.instBEqDynInteraction.beq }

source

instance Phenomena.Agreement.Studies.Deal2024.instReprDynInteraction :

Repr DynInteraction

Equations

Phenomena.Agreement.Studies.Deal2024.instReprDynInteraction = { reprPrec := Phenomena.Agreement.Studies.Deal2024.instReprDynInteraction.repr }

source

def Phenomena.Agreement.Studies.Deal2024.instReprDynInteraction.repr :

DynInteraction → Nat → Std.Format

Equations

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

Instances For

source

structure Phenomena.Agreement.Studies.Deal2024.DealGrammar :

Type

A grammar in @cite{deal-2024}'s framework.

Two parameters determine the PCC type:

satisfaction: which feature, if present on DO, halts the probe. none means the probe is never satisfied by DO alone.
dynInteraction: which features trigger dynamic narrowing of the probe's INT condition after interacting with DO.

satisfaction : Option PersonFeature
dynInteraction : DynInteraction

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.instDecidableEqDealGrammar.decEq (x✝ x✝¹ : DealGrammar) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Phenomena.Agreement.Studies.Deal2024.instDecidableEqDealGrammar :

DecidableEq DealGrammar

Equations

Phenomena.Agreement.Studies.Deal2024.instDecidableEqDealGrammar = Phenomena.Agreement.Studies.Deal2024.instDecidableEqDealGrammar.decEq

source

instance Phenomena.Agreement.Studies.Deal2024.instBEqDealGrammar :

BEq DealGrammar

Equations

Phenomena.Agreement.Studies.Deal2024.instBEqDealGrammar = { beq := Phenomena.Agreement.Studies.Deal2024.instBEqDealGrammar.beq }

source

def Phenomena.Agreement.Studies.Deal2024.instBEqDealGrammar.beq :

DealGrammar → DealGrammar → Bool

Equations

Phenomena.Agreement.Studies.Deal2024.instBEqDealGrammar.beq { satisfaction := a, dynInteraction := a_1 } { satisfaction := b, dynInteraction := b_1 } = (a == b && a_1 == b_1)
Phenomena.Agreement.Studies.Deal2024.instBEqDealGrammar.beq x✝¹ x✝ = false

Instances For

source

instance Phenomena.Agreement.Studies.Deal2024.instReprDealGrammar :

Repr DealGrammar

Equations

Phenomena.Agreement.Studies.Deal2024.instReprDealGrammar = { reprPrec := Phenomena.Agreement.Studies.Deal2024.instReprDealGrammar.repr }

source

def Phenomena.Agreement.Studies.Deal2024.instReprDealGrammar.repr :

DealGrammar → Nat → Std.Format

Equations

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

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.isLicit (g : DealGrammar) (io do_ : Core.Prominence.PersonLevel) :

Bool

Is a clitic combination ⟨IO, DO⟩ licit under a Deal grammar?

The probe encounters DO first ("DO preference"):

If DO bears the SAT feature → probe satisfied → halts before IO → IO not licensed → illicit.
Otherwise, the probe copies features from DO. Dynamic interaction may narrow the probe's subsequent INT condition.
If narrowing occurred, IO must bear the narrowed feature to be visible to the probe. If IO is invisible → illicit.
If no narrowing, IO is always visible → licit.

Equations

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

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.strong :

DealGrammar

Strong PCC: SAT:[PART], no dynamic interaction. DO bearing [PART] satisfies the probe → only 3P DOs survive.

Equations

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

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.meFirst :

DealGrammar

Me-first PCC: SAT:[SPKR], no dynamic interaction. Only 1P DOs satisfy the probe → only 1P DOs are banned.

Equations

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

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.weak :

DealGrammar

Weak PCC: no satisfaction, [PART]↑ dynamic interaction. The probe is never satisfied by DO, but copying [PART] from a SAP DO narrows the probe so it can only see [PART]-bearing IOs.

Equations

Phenomena.Agreement.Studies.Deal2024.weak = { satisfaction := none, dynInteraction := Phenomena.Agreement.Studies.Deal2024.DynInteraction.part }

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.strictlyDescending :

DealGrammar

Strictly descending PCC: SAT:[SPKR], [PART]↑ dynamic interaction. 1P DOs satisfy (banned); SAP DOs narrow the probe to require [PART] on IO.

Equations

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

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.noPCC :

DealGrammar

No PCC: no satisfaction, no dynamic interaction. The probe never halts at DO and never narrows.

Equations

Phenomena.Agreement.Studies.Deal2024.noPCC = { satisfaction := none, dynInteraction := Phenomena.Agreement.Studies.Deal2024.DynInteraction.none_ }

Instances For

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_1_3 :

isLicit strong Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_2_3 :

isLicit strong Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_3_3 :

isLicit strong Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_1_2 :

isLicit strong Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_2_1 :

isLicit strong Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_3_1 :

isLicit strong Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_3_2 :

isLicit strong Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_1_1 :

isLicit strong Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_2_2 :

isLicit strong Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_1_2 :

isLicit meFirst Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = true

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_1_3 :

isLicit meFirst Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_2_3 :

isLicit meFirst Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_3_2 :

isLicit meFirst Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = true

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_3_3 :

isLicit meFirst Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_2_2 :

isLicit meFirst Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = true

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_3_1 :

isLicit meFirst Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_2_1 :

isLicit meFirst Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_1_1 :

isLicit meFirst Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_1_3 :

isLicit weak Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_2_3 :

isLicit weak Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_3_3 :

isLicit weak Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_1_2 :

isLicit weak Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = true

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_2_1 :

isLicit weak Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_1_1 :

isLicit weak Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_2_2 :

isLicit weak Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = true

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_3_1 :

isLicit weak Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_3_2 :

isLicit weak Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_1_3 :

isLicit strictlyDescending Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_2_3 :

isLicit strictlyDescending Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_3_3 :

isLicit strictlyDescending Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_1_2 :

isLicit strictlyDescending Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = true

⟨1,2⟩ is licit: 2P DO doesn't bear [SPKR] (no SAT); dynamic narrowing requires IO to bear [PART]; 1P bears [PART].

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_2_2 :

isLicit strictlyDescending Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = true

⟨2,2⟩ is licit: 2P DO lacks [SPKR]; narrowing requires [PART] on IO; 2P IO bears [PART].

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_2_1 :

isLicit strictlyDescending Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_1_1 :

isLicit strictlyDescending Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_3_1 :

isLicit strictlyDescending Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_3_2 :

isLicit strictlyDescending Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = false

⟨3,2⟩ is illicit: 2P DO lacks [SPKR] but bears [PART]; narrowing requires [PART] on IO; 3P IO lacks [PART].

source

theorem Phenomena.Agreement.Studies.Deal2024.nopcc_all_licit (io do_ : Core.Prominence.PersonLevel) :

isLicit noPCC io do_ = true

source

def Phenomena.Agreement.Studies.Deal2024.licitCount (g : DealGrammar) :

Nat

Count licit combinations (out of 9 = 3×3).

Equations

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

Instances For

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_licit_count :

licitCount strong = 3

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_licit_count :

licitCount meFirst = 6

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_licit_count :

licitCount weak = 7

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_licit_count :

licitCount strictlyDescending = 5

source

theorem Phenomena.Agreement.Studies.Deal2024.nopcc_licit_count :

licitCount noPCC = 9

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_entails_mefirst (io do_ : Core.Prominence.PersonLevel) :

isLicit strong io do_ = true → isLicit meFirst io do_ = true

Strong entails Me-first: anything licit under Strong is licit under Me-first. (Strong has SAT:[PART] ⊇ SAT:[SPKR].)

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_entails_weak (io do_ : Core.Prominence.PersonLevel) :

isLicit strong io do_ = true → isLicit weak io do_ = true

Strong entails Weak: anything licit under Strong is licit under Weak.

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_matches_pz (io do_ : Core.Prominence.PersonLevel) :

isLicit strong io do_ = Minimalism.PConstraint.pccLicit Minimalism.PConstraint.strongGrammar io do_

Deal's Strong PCC matches P&Z's Strong PCC on all 9 cells.

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_matches_pz (io do_ : Core.Prominence.PersonLevel) :

isLicit weak io do_ = Minimalism.PConstraint.pccLicit Minimalism.PConstraint.weakGrammar io do_

Deal's Weak PCC matches P&Z's Weak PCC on all 9 cells.

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_matches_pz (io do_ : Core.Prominence.PersonLevel) :

isLicit meFirst io do_ = Minimalism.PConstraint.pccLicit Minimalism.PConstraint.meFirstGrammar io do_

Deal's Me-first PCC matches P&Z's Me-first PCC on all 9 cells.

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_matches_ultra_non_reflexive :

Strictly descending agrees with ultra-strong on 7 of 9 cells. All non-reflexive-SAP combinations match.

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_ultra_discrepancy_1_1 :

isLicit strictlyDescending Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = false ∧ Minimalism.PConstraint.pccLicit Minimalism.PConstraint.ultraStrongGrammar Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = true

Strictly descending diverges from ultra-strong on ⟨1,1⟩: Deal bans it (1P DO satisfies SAT:[SPKR]), P&Z allows it (P-Primacy rescues: 1P IO is [+author]).

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_ultra_discrepancy_2_2 :

isLicit strictlyDescending Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = true ∧ Minimalism.PConstraint.pccLicit Minimalism.PConstraint.ultraStrongGrammar Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = false

Strictly descending diverges from ultra-strong on ⟨2,2⟩: Deal allows it (2P lacks [SPKR]; narrowing requires [PART]; 2P bears [PART]), P&Z bans it (P-Uniqueness violated, 2P lacks [+author] so no P-Primacy rescue).

source

theorem Phenomena.Agreement.Studies.Deal2024.residue_empty_iff_bears_part (p : Core.Prominence.PersonLevel) :

List.isEmpty (Minimalism.CyclicAgree.activeResidue Minimalism.CyclicAgree.partialProbe (Minimalism.CyclicAgree.personSpec Minimalism.CyclicAgree.Geometry.standard p)) = dpBears p PersonFeature.part

Probe satisfaction in @cite{deal-2024}'s sense (SAT:[PART]) corresponds to residue depletion in @cite{bejar-rezac-2009}'s cyclic Agree.

A DP fully checks the partial probe [uπ, uParticipant] iff it bears [PART]. In Deal's terms, such a DP satisfies a SAT:[PART] probe. In B&R's terms, it depletes the active residue to ∅.

This bridges the two frameworks: "the probe is satisfied" (Deal) ↔ "no active residue remains" (B&R).

source

theorem Phenomena.Agreement.Studies.Deal2024.residue_nonempty_iff_lacks_part (p : Core.Prominence.PersonLevel) :

(!List.isEmpty (Minimalism.CyclicAgree.activeResidue Minimalism.CyclicAgree.partialProbe (Minimalism.CyclicAgree.personSpec Minimalism.CyclicAgree.Geometry.standard p))) = !dpBears p PersonFeature.part

The converse direction: a DP that does NOT bear [PART] leaves non-empty residue — the probe continues to the next cycle.

source

theorem Phenomena.Agreement.Studies.Deal2024.sat_part_absorbs_dynint (dyn : DynInteraction) (io do_ : Core.Prominence.PersonLevel) :

isLicit { satisfaction := some PersonFeature.part, dynInteraction := dyn } io do_ = isLicit strong io do_

SAT:[PART] yields the Strong PCC regardless of dynamic interaction.

This is the key insight of Table (53): when DO bears [PART], the probe is satisfied before any dynamic narrowing can take effect. Since [SPKR] and [ADDR] geometrically entail [PART], any DP that would trigger dynamic interaction via [SPKR]↑ or [PART]↑ also satisfies SAT:[PART]. Therefore, dynamic interaction is irrelevant when SAT = [PART].

source

def Phenomena.Agreement.Studies.Deal2024.youFirst :

DealGrammar

You-first PCC (predicted): SAT:[ADDR], no dynamic interaction. 2P DOs satisfy the probe → ⟨IO, 2P DO⟩ is illicit. Predicted by @cite{deal-2024} §6.1 but not yet robustly attested.

Equations

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

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.aDescending :

DealGrammar

A-descending PCC (predicted): SAT:[ADDR], [PART]↑ dynamic interaction. IO must outrank DO on the hierarchy 2 > 1 > 3. @cite{deal-2024} §6.1 notes hints of this pattern in Catalan and Italian speaker variation.

Equations

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

Instances For

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_1_3 :

isLicit youFirst Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_2_3 :

isLicit youFirst Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_3_3 :

isLicit youFirst Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_2_1 :

isLicit youFirst Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_1_1 :

isLicit youFirst Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_3_1 :

isLicit youFirst Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_1_2 :

isLicit youFirst Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_3_2 :

isLicit youFirst Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_2_2 :

isLicit youFirst Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_2_1 :

isLicit aDescending Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_2_3 :

isLicit aDescending Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_1_3 :

isLicit aDescending Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_3_3 :

isLicit aDescending Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.third = true

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_1_1 :

isLicit aDescending Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_1_2 :

isLicit aDescending Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_3_1 :

isLicit aDescending Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = false

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_3_2 :

isLicit aDescending Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_2_2 :

isLicit aDescending Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.yf_licit_count :

licitCount youFirst = 6

source

theorem Phenomena.Agreement.Studies.Deal2024.ad_licit_count :

licitCount aDescending = 5

source

def Phenomena.Agreement.Studies.Deal2024.reverseLicit (g : DealGrammar) (io do_ : Core.Prominence.PersonLevel) :

Bool

Reverse PCC: the probe encounters IO before DO (IO preference).

@cite{deal-2024} §6.2: in structures where IO moves to a position between v and DO, the probe encounters IO first. This reverses the PCC restriction — now IO features can satisfy/narrow the probe, and DO is the argument that may fail to be licensed.

Attested in Shapsug Adyghe, varieties of Swiss German, Czech, and Slovenian.

Equations

Phenomena.Agreement.Studies.Deal2024.reverseLicit g io do_ = Phenomena.Agreement.Studies.Deal2024.isLicit g do_ io

Instances For

source

def Phenomena.Agreement.Studies.Deal2024.reverseSD :

DealGrammar

Reverse strictly descending PCC (Shapsug Adyghe): DO must outrank IO on the hierarchy 1 > 2 > 3 — the mirror image of forward SD.

Equations

Phenomena.Agreement.Studies.Deal2024.reverseSD = Phenomena.Agreement.Studies.Deal2024.strictlyDescending

Instances For

source

theorem Phenomena.Agreement.Studies.Deal2024.rsd_3_1_ok :

reverseLicit reverseSD Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.rsd_3_2_ok :

reverseLicit reverseSD Core.Prominence.PersonLevel.third Core.Prominence.PersonLevel.second = true

source

theorem Phenomena.Agreement.Studies.Deal2024.rsd_2_1_ok :

reverseLicit reverseSD Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.first = true

source

theorem Phenomena.Agreement.Studies.Deal2024.rsd_1_3_bad :

reverseLicit reverseSD Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.third = false

source

theorem Phenomena.Agreement.Studies.Deal2024.rsd_2_3_bad :

reverseLicit reverseSD Core.Prominence.PersonLevel.second Core.Prominence.PersonLevel.third = false

source

theorem Phenomena.Agreement.Studies.Deal2024.rsd_1_2_bad :

reverseLicit reverseSD Core.Prominence.PersonLevel.first Core.Prominence.PersonLevel.second = false

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_iff_3p_do (io do_ : Core.Prominence.PersonLevel) :

isLicit strong io do_ = true ↔ do_ = Core.Prominence.PersonLevel.third

Strong PCC (2a): DO must be 3P. Any IO is licit with a 3P DO; any SAP DO is illicit regardless of IO.

source

theorem Phenomena.Agreement.Studies.Deal2024.weak_illicit_iff (io do_ : Core.Prominence.PersonLevel) :

isLicit weak io do_ = false ↔ io = Core.Prominence.PersonLevel.third ∧ do_.isSAP = true

Weak PCC (2b): if IO is 3P, DO must be 3P. Equivalently: the only illicit cells are ⟨3P IO, SAP DO⟩.

source

theorem Phenomena.Agreement.Studies.Deal2024.mefirst_iff_not_1p_do (io do_ : Core.Prominence.PersonLevel) :

isLicit meFirst io do_ = true ↔ dpBears do_ PersonFeature.spkr = false

Me-first PCC (2c): if 1P is present, it must be IO. Equivalently: DO cannot be 1P.

source

theorem Phenomena.Agreement.Studies.Deal2024.sd_off_diagonal_iff_outranks (io do_ : Core.Prominence.PersonLevel) (h : io ≠ do_) :

isLicit strictlyDescending io do_ = true ↔ io.rank > do_.rank

Strictly descending PCC (2d): IO must outrank DO on 1 > 2 > 3. For the 6 non-diagonal cells, this is exactly the pattern. (Diagonal cells: ⟨3,3⟩ and ⟨2,2⟩ are licit; ⟨1,1⟩ is illicit because SAT:[SPKR] fires.)

source

theorem Phenomena.Agreement.Studies.Deal2024.strong_entails_sd (io do_ : Core.Prominence.PersonLevel) :

isLicit strong io do_ = true → isLicit strictlyDescending io do_ = true

Strong entails strictly descending: anything licit under Strong is licit under SD. (Strong bans all SAP DOs; SD bans only 1P DOs and ⟨3P IO, SAP DO⟩.)

source

theorem Phenomena.Agreement.Studies.Deal2024.dpBears_grounded_in_decomposePerson (p : Core.Prominence.PersonLevel) :

dpBears p PersonFeature.part = (Minimalism.decomposePerson p).hasParticipant ∧ dpBears p PersonFeature.spkr = (Minimalism.decomposePerson p).hasAuthor

dpBears is grounded in the shared feature geometry decomposePerson from PersonGeometry.lean. This makes the connection structural — Deal's person features are not independently stipulated but derived from the same privative geometry used by @cite{pancheva-zubizarreta-2018}'s satisfiesProminence and @cite{bejar-rezac-2009}'s personSpec.

Documentation

Linglib.Phenomena.Agreement.Studies.Deal2024

Interaction, Satisfaction, and the PCC @cite{deal-2024} #

PCC Typology #

Bridge Results #