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:

1. @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).
2. @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.

inductive Deal2024.PersonFeature : Type

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

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

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

• phi : PersonFeature
• part : PersonFeature
• spkr : PersonFeature
• addr : PersonFeature

@[implicit_reducible]

instance Deal2024.instDecidableEqPersonFeature : DecidableEq PersonFeature

Equations

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

@[implicit_reducible]

instance Deal2024.instReprPersonFeature : Repr PersonFeature

Equations

• Deal2024.instReprPersonFeature = { reprPrec := Deal2024.instReprPersonFeature.repr }

def Deal2024.instReprPersonFeature.repr : PersonFeature → ℕ → Std.Format

Equations

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

def Deal2024.dpBears (p : Features.Prominence.PersonLevel) (f : PersonFeature) : Bool

Does a DP of person level p bear feature f?

Equations

• Deal2024.dpBears p Deal2024.PersonFeature.phi = true
• Deal2024.dpBears p Deal2024.PersonFeature.part = (Minimalist.decomposePerson p).hasParticipant
• Deal2024.dpBears p Deal2024.PersonFeature.spkr = (Minimalist.decomposePerson p).hasAuthor
• Deal2024.dpBears p Deal2024.PersonFeature.addr = (p == Features.Prominence.PersonLevel.second)

theorem Deal2024.first_bears : dpBears Features.Prominence.PersonLevel.first PersonFeature.phi = true ∧ dpBears Features.Prominence.PersonLevel.first PersonFeature.part = true ∧ dpBears Features.Prominence.PersonLevel.first PersonFeature.spkr = true ∧ dpBears Features.Prominence.PersonLevel.first PersonFeature.addr = false

theorem Deal2024.second_bears : dpBears Features.Prominence.PersonLevel.second PersonFeature.phi = true ∧ dpBears Features.Prominence.PersonLevel.second PersonFeature.part = true ∧ dpBears Features.Prominence.PersonLevel.second PersonFeature.spkr = false ∧ dpBears Features.Prominence.PersonLevel.second PersonFeature.addr = true

theorem Deal2024.third_bears : dpBears Features.Prominence.PersonLevel.third PersonFeature.phi = true ∧ dpBears Features.Prominence.PersonLevel.third PersonFeature.part = false ∧ dpBears Features.Prominence.PersonLevel.third PersonFeature.spkr = false ∧ dpBears Features.Prominence.PersonLevel.third PersonFeature.addr = false

inductive 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

@[implicit_reducible]

instance Deal2024.instDecidableEqDynInteraction : DecidableEq DynInteraction

Equations

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

@[implicit_reducible]

instance Deal2024.instReprDynInteraction : Repr DynInteraction

Equations

• Deal2024.instReprDynInteraction = { reprPrec := Deal2024.instReprDynInteraction.repr }

def Deal2024.instReprDynInteraction.repr : DynInteraction → ℕ → Std.Format

Equations

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

structure 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

@[implicit_reducible]

instance Deal2024.instDecidableEqDealGrammar : DecidableEq DealGrammar

Equations

• Deal2024.instDecidableEqDealGrammar = Deal2024.instDecidableEqDealGrammar.decEq

def Deal2024.instDecidableEqDealGrammar.decEq (x✝ x✝¹ : DealGrammar) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Deal2024.instReprDealGrammar : Repr DealGrammar

Equations

• Deal2024.instReprDealGrammar = { reprPrec := Deal2024.instReprDealGrammar.repr }

def Deal2024.instReprDealGrammar.repr : DealGrammar → ℕ → Std.Format

Equations

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

def Deal2024.isLicit (g : DealGrammar) (io do_ : Features.Prominence.PersonLevel) : Bool

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

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

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

Equations

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

def Deal2024.strong : DealGrammar

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

Equations

• Deal2024.strong = { satisfaction := some Deal2024.PersonFeature.part, dynInteraction := Deal2024.DynInteraction.none_ }

def Deal2024.meFirst : DealGrammar

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

Equations

• Deal2024.meFirst = { satisfaction := some Deal2024.PersonFeature.spkr, dynInteraction := Deal2024.DynInteraction.none_ }

def 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

• Deal2024.weak = { satisfaction := none, dynInteraction := Deal2024.DynInteraction.part }

def 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

• Deal2024.strictlyDescending = { satisfaction := some Deal2024.PersonFeature.spkr, dynInteraction := Deal2024.DynInteraction.part }

def Deal2024.noPCC : DealGrammar

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

Equations

• Deal2024.noPCC = { satisfaction := none, dynInteraction := Deal2024.DynInteraction.none_ }

theorem Deal2024.strong_1_3 : isLicit strong Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = true

theorem Deal2024.strong_2_3 : isLicit strong Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = true

theorem Deal2024.strong_3_3 : isLicit strong Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third = true

theorem Deal2024.strong_1_2 : isLicit strong Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second = false

theorem Deal2024.strong_2_1 : isLicit strong Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = false

theorem Deal2024.strong_3_1 : isLicit strong Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = false

theorem Deal2024.strong_3_2 : isLicit strong Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = false

theorem Deal2024.strong_1_1 : isLicit strong Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first = false

theorem Deal2024.strong_2_2 : isLicit strong Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second = false

theorem Deal2024.mefirst_1_2 : isLicit meFirst Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second = true

theorem Deal2024.mefirst_1_3 : isLicit meFirst Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = true

theorem Deal2024.mefirst_2_3 : isLicit meFirst Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = true

theorem Deal2024.mefirst_3_2 : isLicit meFirst Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = true

theorem Deal2024.mefirst_3_3 : isLicit meFirst Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third = true

theorem Deal2024.mefirst_2_2 : isLicit meFirst Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second = true

theorem Deal2024.mefirst_3_1 : isLicit meFirst Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = false

theorem Deal2024.mefirst_2_1 : isLicit meFirst Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = false

theorem Deal2024.mefirst_1_1 : isLicit meFirst Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first = false

theorem Deal2024.weak_1_3 : isLicit weak Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = true

theorem Deal2024.weak_2_3 : isLicit weak Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = true

theorem Deal2024.weak_3_3 : isLicit weak Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third = true

theorem Deal2024.weak_1_2 : isLicit weak Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second = true

theorem Deal2024.weak_2_1 : isLicit weak Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = true

theorem Deal2024.weak_1_1 : isLicit weak Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first = true

theorem Deal2024.weak_2_2 : isLicit weak Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second = true

theorem Deal2024.weak_3_1 : isLicit weak Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = false

theorem Deal2024.weak_3_2 : isLicit weak Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = false

theorem Deal2024.sd_1_3 : isLicit strictlyDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = true

theorem Deal2024.sd_2_3 : isLicit strictlyDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = true

theorem Deal2024.sd_3_3 : isLicit strictlyDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third = true

theorem Deal2024.sd_1_2 : isLicit strictlyDescending Features.Prominence.PersonLevel.first Features.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].

theorem Deal2024.sd_2_2 : isLicit strictlyDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second = true

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

theorem Deal2024.sd_2_1 : isLicit strictlyDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = false

theorem Deal2024.sd_1_1 : isLicit strictlyDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first = false

theorem Deal2024.sd_3_1 : isLicit strictlyDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = false

theorem Deal2024.sd_3_2 : isLicit strictlyDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = false

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

theorem Deal2024.nopcc_all_licit (io do_ : Features.Prominence.PersonLevel) : isLicit noPCC io do_ = true

def Deal2024.licitCount (g : DealGrammar) : ℕ

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

Equations

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

theorem Deal2024.strong_licit_count : licitCount strong = 3

theorem Deal2024.mefirst_licit_count : licitCount meFirst = 6

theorem Deal2024.weak_licit_count : licitCount weak = 7

theorem Deal2024.sd_licit_count : licitCount strictlyDescending = 5

theorem Deal2024.nopcc_licit_count : licitCount noPCC = 9

theorem Deal2024.strong_entails_mefirst (io do_ : Features.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].)

theorem Deal2024.strong_entails_weak (io do_ : Features.Prominence.PersonLevel) : isLicit strong io do_ = true → isLicit weak io do_ = true

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

theorem Deal2024.strong_matches_pz (io do_ : Features.Prominence.PersonLevel) : isLicit strong io do_ = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.strongGrammar io do_

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

theorem Deal2024.weak_matches_pz (io do_ : Features.Prominence.PersonLevel) : isLicit weak io do_ = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.weakGrammar io do_

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

theorem Deal2024.mefirst_matches_pz (io do_ : Features.Prominence.PersonLevel) : isLicit meFirst io do_ = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.meFirstGrammar io do_

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

theorem Deal2024.sd_matches_ultra_non_reflexive : (isLicit strictlyDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second) ∧ (isLicit strictlyDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third) ∧ (isLicit strictlyDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first) ∧ (isLicit strictlyDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third) ∧ (isLicit strictlyDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first) ∧ (isLicit strictlyDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second) ∧ (isLicit strictlyDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third = true ↔ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third)

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

theorem Deal2024.sd_ultra_discrepancy_1_1 : isLicit strictlyDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first = false ∧ Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first

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]).

theorem Deal2024.sd_ultra_discrepancy_2_2 : isLicit strictlyDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second = true ∧ ¬Minimalist.PConstraint.IsLicit Minimalist.PConstraint.ultraStrongGrammar Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second

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).

theorem Deal2024.residue_empty_iff_bears_part (p : Features.Prominence.PersonLevel) : List.isEmpty (Minimalist.CyclicAgree.activeResidue Minimalist.CyclicAgree.partialProbe (Minimalist.CyclicAgree.personSpec Minimalist.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).

theorem Deal2024.residue_nonempty_iff_lacks_part (p : Features.Prominence.PersonLevel) : (!List.isEmpty (Minimalist.CyclicAgree.activeResidue Minimalist.CyclicAgree.partialProbe (Minimalist.CyclicAgree.personSpec Minimalist.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.

theorem Deal2024.sat_part_absorbs_dynint (dyn : DynInteraction) (io do_ : Features.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].

def 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

• Deal2024.youFirst = { satisfaction := some Deal2024.PersonFeature.addr, dynInteraction := Deal2024.DynInteraction.none_ }

def 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

• Deal2024.aDescending = { satisfaction := some Deal2024.PersonFeature.addr, dynInteraction := Deal2024.DynInteraction.part }

theorem Deal2024.yf_1_3 : isLicit youFirst Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = true

theorem Deal2024.yf_2_3 : isLicit youFirst Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = true

theorem Deal2024.yf_3_3 : isLicit youFirst Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third = true

theorem Deal2024.yf_2_1 : isLicit youFirst Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = true

theorem Deal2024.yf_1_1 : isLicit youFirst Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first = true

theorem Deal2024.yf_3_1 : isLicit youFirst Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = true

theorem Deal2024.yf_1_2 : isLicit youFirst Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second = false

theorem Deal2024.yf_3_2 : isLicit youFirst Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = false

theorem Deal2024.yf_2_2 : isLicit youFirst Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second = false

theorem Deal2024.ad_2_1 : isLicit aDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = true

theorem Deal2024.ad_2_3 : isLicit aDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = true

theorem Deal2024.ad_1_3 : isLicit aDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = true

theorem Deal2024.ad_3_3 : isLicit aDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.third = true

theorem Deal2024.ad_1_1 : isLicit aDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.first = true

theorem Deal2024.ad_1_2 : isLicit aDescending Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second = false

theorem Deal2024.ad_3_1 : isLicit aDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = false

theorem Deal2024.ad_3_2 : isLicit aDescending Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = false

theorem Deal2024.ad_2_2 : isLicit aDescending Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.second = false

theorem Deal2024.yf_licit_count : licitCount youFirst = 6

theorem Deal2024.ad_licit_count : licitCount aDescending = 5

def Deal2024.reverseLicit (g : DealGrammar) (io do_ : Features.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

• Deal2024.reverseLicit g io do_ = Deal2024.isLicit g do_ io

def 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

• Deal2024.reverseSD = Deal2024.strictlyDescending

theorem Deal2024.rsd_3_1_ok : reverseLicit reverseSD Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.first = true

theorem Deal2024.rsd_3_2_ok : reverseLicit reverseSD Features.Prominence.PersonLevel.third Features.Prominence.PersonLevel.second = true

theorem Deal2024.rsd_2_1_ok : reverseLicit reverseSD Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.first = true

theorem Deal2024.rsd_1_3_bad : reverseLicit reverseSD Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.third = false

theorem Deal2024.rsd_2_3_bad : reverseLicit reverseSD Features.Prominence.PersonLevel.second Features.Prominence.PersonLevel.third = false

theorem Deal2024.rsd_1_2_bad : reverseLicit reverseSD Features.Prominence.PersonLevel.first Features.Prominence.PersonLevel.second = false

theorem Deal2024.strong_iff_3p_do (io do_ : Features.Prominence.PersonLevel) : isLicit strong io do_ = true ↔ do_ = Features.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.

theorem Deal2024.weak_illicit_iff (io do_ : Features.Prominence.PersonLevel) : isLicit weak io do_ = false ↔ io = Features.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⟩.

theorem Deal2024.mefirst_iff_not_1p_do (io do_ : Features.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.

theorem Deal2024.sd_off_diagonal_iff_outranks (io do_ : Features.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.)

theorem Deal2024.strong_entails_sd (io do_ : Features.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⟩.)

theorem Deal2024.dpBears_grounded_in_decomposePerson (p : Features.Prominence.PersonLevel) : dpBears p PersonFeature.part = (Minimalist.decomposePerson p).hasParticipant ∧ dpBears p PersonFeature.spkr = (Minimalist.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.