Interaction, Satisfaction, and the PCC [Dea24]

[Dea24] 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 [Dea24]'s framework to both:

1. [PZ18] (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. [BR09] (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.
3. [CK21] (Studies/CoonKeine2021.lean): strong and weak coincide with gluttony cell-for-cell; Me-First diverges exactly at 1>1 (mefirst_diverges_from_gluttony).

The licitness function is run, not tabulated: runProbe walks the goal sequence with interaction, satisfaction, and dynamic narrowing as state transitions (step), with step_int_mono ("dynamic interaction only narrows"), probe_vis_antitone (its Probe-level form: the state-indexed probe family ProbeState.probe only sees less over time), and step_of_satisfied (a satisfied probe is inert) as the probe-state laws; isLicit and the (1)-table theorems are derived from runs.

inductive Deal2024.PersonFeature : Type

Person features in [Dea24]'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 : Person) (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 == Person.second)

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

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

theorem Deal2024.third_bears : dpBears Person.third PersonFeature.phi = true ∧ dpBears Person.third PersonFeature.part = false ∧ dpBears Person.third PersonFeature.spkr = false ∧ dpBears Person.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 ⋯

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

Equations

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

@[implicit_reducible]

instance Deal2024.instReprDynInteraction : Repr DynInteraction

Equations

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

structure Deal2024.DealGrammar : Type

A grammar in [Dea24]'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.

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

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.PersonFeature.below : PersonFeature → List PersonFeature

Downward closure of a person feature in the (7) geometry (same convention as Segment.below, Phi/Articulation.lean): the features that bearing this one entails.

Equations

• Deal2024.PersonFeature.phi.below = [Deal2024.PersonFeature.phi]
• Deal2024.PersonFeature.part.below = [Deal2024.PersonFeature.phi, Deal2024.PersonFeature.part]
• Deal2024.PersonFeature.spkr.below = [Deal2024.PersonFeature.phi, Deal2024.PersonFeature.part, Deal2024.PersonFeature.spkr]
• Deal2024.PersonFeature.addr.below = [Deal2024.PersonFeature.phi, Deal2024.PersonFeature.part, Deal2024.PersonFeature.addr]

@[implicit_reducible]

instance Deal2024.instPartialOrderPersonFeature : PartialOrder PersonFeature

The entailment order: s ≤ t iff bearing t entails bearing s; [φ] is bottom, [SPKR]/[ADDR] maximal. "More specific" = larger.

Equations

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

@[implicit_reducible]

instance Deal2024.instDecidableRelPersonFeatureLe : DecidableRel fun (x1 x2 : PersonFeature) => x1 ≤ x2

Equations

• Deal2024.instDecidableRelPersonFeatureLe s t = List.instDecidableMemOfLawfulBEq s t.below

structure Deal2024.ProbeState : Type

The probe's state during its walk over the goal sequence (her (8), (44)–(47)): the current interaction condition, the satisfaction flag, and the positions of the goals interacted with.

• int : PersonFeature
• satisfied : Bool
• agreed : List ℕ

def Deal2024.instDecidableEqProbeState.decEq (x✝ x✝¹ : ProbeState) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Deal2024.instDecidableEqProbeState : DecidableEq ProbeState

Equations

• Deal2024.instDecidableEqProbeState = Deal2024.instDecidableEqProbeState.decEq

@[implicit_reducible]

instance Deal2024.instReprProbeState : Repr ProbeState

Equations

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

def Deal2024.instReprProbeState.repr : ProbeState → ℕ → Std.Format

Equations

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

def Deal2024.ProbeState.initial : ProbeState

Initial state: [INT:φ], unsatisfied, nothing agreed.

Equations

• Deal2024.ProbeState.initial = { int := Deal2024.PersonFeature.phi, satisfied := false, agreed := [] }

def Deal2024.ProbeState.probe (st : ProbeState) : Minimalist.Probe Person

The static Probe a state denotes: visibility = bearing the current INT condition. Deal's dynamic probe is a state-indexed family of static probes — step's interaction check is literally st.probe.vis.

Equations

• st.probe = Minimalist.Probe.ofVis fun (p : Person) => Deal2024.dpBears p st.int

def Deal2024.narrowTarget (d : DynInteraction) (p : Person) : Option PersonFeature

The dynamic-interaction target a goal contributes (her §5): [F]↑ narrows INT to [F] when the interacted goal bears [F]; in the combined setting [SPKR]↑ takes priority.

Equations

• One or more equations did not get rendered due to their size.
• Deal2024.narrowTarget Deal2024.DynInteraction.none_ p = none
• Deal2024.narrowTarget Deal2024.DynInteraction.part p = if Deal2024.dpBears p Deal2024.PersonFeature.part = true then some Deal2024.PersonFeature.part else none
• Deal2024.narrowTarget Deal2024.DynInteraction.spkr p = if Deal2024.dpBears p Deal2024.PersonFeature.spkr = true then some Deal2024.PersonFeature.spkr else none

def Deal2024.step (g : DealGrammar) (st : ProbeState) (t : Person × ℕ) : ProbeState

One step of the probe's walk: a satisfied probe is inert (her (8b)); otherwise a goal bearing the current INT is interacted with (its position recorded), satisfaction is checked against the goal, and dynamic interaction narrows INT (her (44)–(47)). The narrowing is guarded to be specificity-increasing — vacuously for every grammar of the paper, where a run has at most one narrowing target; the guard makes step_int_mono true by construction.

Equations

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

def Deal2024.runProbe (g : DealGrammar) (goals : List Person) : ProbeState

Run the probe over a goal sequence, in interaction order.

Equations

• Deal2024.runProbe g goals = List.foldl (Deal2024.step g) Deal2024.ProbeState.initial goals.zipIdx

theorem Deal2024.step_int_mono (g : DealGrammar) (st : ProbeState) (t : Person × ℕ) : st.int ≤ (step g st t).int

"Dynamic interaction only narrows": along any run, the interaction condition only becomes more specific — the probe-state law that makes [Dea24]'s INT a well-behaved object.

theorem Deal2024.dpBears_antitone {f g : PersonFeature} (hfg : f ≤ g) (p : Person) (h : dpBears p g = true) : dpBears p f = true

Bearing a more specific feature entails bearing a less specific one — the (7) geometry, as monotonicity of dpBears.

theorem Deal2024.probe_vis_antitone (g : DealGrammar) (st : ProbeState) (t : Person × ℕ) (a : Person) (h : (step g st t).probe.vis a = true) : st.probe.vis a = true

The state-indexed probe family only narrows: anything visible to a later state's probe was visible to an earlier state's — step_int_mono at the Probe level.

theorem Deal2024.probe_outcome_antitone (g : DealGrammar) (st : ProbeState) (t : Person × ℕ) (goals : List Person) (h : (step g st t).probe.outcome goals = Minimalist.Probe.Outcome.valued) : st.probe.outcome goals = Minimalist.Probe.Outcome.valued

Narrowing the probe cannot gain a goal: if the later (narrower) state's probe still finds one, so did the earlier — the outcome-level form of "interaction only narrows", from the substrate's Probe.outcome_valued_mono fed by probe_vis_antitone.

theorem Deal2024.step_of_satisfied (g : DealGrammar) (st : ProbeState) (t : Person × ℕ) (h : st.satisfied = true) : step g st t = st

A satisfied probe is inert: satisfaction halts all further interaction (her (8b)).

def Deal2024.isLicit (g : DealGrammar) (io do_ : Person) : Bool

Is a clitic combination ⟨IO, DO⟩ licit under a Deal grammar? Cliticization of both objects requires Agree with both (her §4), and the probe interacts with the DO first (DO preference, her (17), on either the high- or the low-probe structure): licit iff the run over ⟨DO, IO⟩ interacts with both goals. The PCC varieties are now derived by running the probe, not read off a table.

Equations

• Deal2024.isLicit g io do_ = ((Deal2024.runProbe g [do_, io]).agreed.length == 2)

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 Person.first Person.third = true

theorem Deal2024.strong_2_3 : isLicit strong Person.second Person.third = true

theorem Deal2024.strong_3_3 : isLicit strong Person.third Person.third = true

theorem Deal2024.strong_1_2 : isLicit strong Person.first Person.second = false

theorem Deal2024.strong_2_1 : isLicit strong Person.second Person.first = false

theorem Deal2024.strong_3_1 : isLicit strong Person.third Person.first = false

theorem Deal2024.strong_3_2 : isLicit strong Person.third Person.second = false

theorem Deal2024.strong_1_1 : isLicit strong Person.first Person.first = false

theorem Deal2024.strong_2_2 : isLicit strong Person.second Person.second = false

theorem Deal2024.mefirst_1_2 : isLicit meFirst Person.first Person.second = true

theorem Deal2024.mefirst_1_3 : isLicit meFirst Person.first Person.third = true

theorem Deal2024.mefirst_2_3 : isLicit meFirst Person.second Person.third = true

theorem Deal2024.mefirst_3_2 : isLicit meFirst Person.third Person.second = true

theorem Deal2024.mefirst_3_3 : isLicit meFirst Person.third Person.third = true

theorem Deal2024.mefirst_2_2 : isLicit meFirst Person.second Person.second = true

theorem Deal2024.mefirst_3_1 : isLicit meFirst Person.third Person.first = false

theorem Deal2024.mefirst_2_1 : isLicit meFirst Person.second Person.first = false

theorem Deal2024.mefirst_1_1 : isLicit meFirst Person.first Person.first = false

theorem Deal2024.weak_1_3 : isLicit weak Person.first Person.third = true

theorem Deal2024.weak_2_3 : isLicit weak Person.second Person.third = true

theorem Deal2024.weak_3_3 : isLicit weak Person.third Person.third = true

theorem Deal2024.weak_1_2 : isLicit weak Person.first Person.second = true

theorem Deal2024.weak_2_1 : isLicit weak Person.second Person.first = true

theorem Deal2024.weak_1_1 : isLicit weak Person.first Person.first = true

theorem Deal2024.weak_2_2 : isLicit weak Person.second Person.second = true

theorem Deal2024.weak_3_1 : isLicit weak Person.third Person.first = false

theorem Deal2024.weak_3_2 : isLicit weak Person.third Person.second = false

theorem Deal2024.sd_1_3 : isLicit strictlyDescending Person.first Person.third = true

theorem Deal2024.sd_2_3 : isLicit strictlyDescending Person.second Person.third = true

theorem Deal2024.sd_3_3 : isLicit strictlyDescending Person.third Person.third = true

theorem Deal2024.sd_1_2 : isLicit strictlyDescending Person.first Person.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 Person.second Person.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 Person.second Person.first = false

theorem Deal2024.sd_1_1 : isLicit strictlyDescending Person.first Person.first = false

theorem Deal2024.sd_3_1 : isLicit strictlyDescending Person.third Person.first = false

theorem Deal2024.sd_3_2 : isLicit strictlyDescending Person.third Person.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_ : Person) : 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_ : Person) : 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_ : Person) : 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_ : Person) : isLicit strong io do_ = true ↔ PCC.IsLicit PCC.strongGrammar io do_

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

theorem Deal2024.weak_matches_pz (io do_ : Person) : isLicit weak io do_ = true ↔ PCC.IsLicit PCC.weakGrammar io do_

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

theorem Deal2024.mefirst_matches_pz (io do_ : Person) : isLicit meFirst io do_ = true ↔ PCC.IsLicit PCC.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 Person.first Person.second = true ↔ PCC.IsLicit PCC.ultraStrongGrammar Person.first Person.second) ∧ (isLicit strictlyDescending Person.first Person.third = true ↔ PCC.IsLicit PCC.ultraStrongGrammar Person.first Person.third) ∧ (isLicit strictlyDescending Person.second Person.first = true ↔ PCC.IsLicit PCC.ultraStrongGrammar Person.second Person.first) ∧ (isLicit strictlyDescending Person.second Person.third = true ↔ PCC.IsLicit PCC.ultraStrongGrammar Person.second Person.third) ∧ (isLicit strictlyDescending Person.third Person.first = true ↔ PCC.IsLicit PCC.ultraStrongGrammar Person.third Person.first) ∧ (isLicit strictlyDescending Person.third Person.second = true ↔ PCC.IsLicit PCC.ultraStrongGrammar Person.third Person.second) ∧ (isLicit strictlyDescending Person.third Person.third = true ↔ PCC.IsLicit PCC.ultraStrongGrammar Person.third Person.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 Person.first Person.first = false ∧ PCC.IsLicit PCC.ultraStrongGrammar Person.first Person.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 Person.second Person.second = true ∧ ¬PCC.IsLicit PCC.ultraStrongGrammar Person.second Person.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 : Person) : List.isEmpty (Minimalist.CyclicAgree.activeResidue Minimalist.CyclicAgree.partialProbe (Minimalist.CyclicAgree.personSpec Minimalist.CyclicAgree.Geometry.standard p)) = dpBears p PersonFeature.part

Probe satisfaction in [Dea24]'s sense (SAT:[PART]) corresponds to residue depletion in [BR09]'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 : Person) : (!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_ : Person) : 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 [Dea24] §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. [Dea24] §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 Person.first Person.third = true

theorem Deal2024.yf_2_3 : isLicit youFirst Person.second Person.third = true

theorem Deal2024.yf_3_3 : isLicit youFirst Person.third Person.third = true

theorem Deal2024.yf_2_1 : isLicit youFirst Person.second Person.first = true

theorem Deal2024.yf_1_1 : isLicit youFirst Person.first Person.first = true

theorem Deal2024.yf_3_1 : isLicit youFirst Person.third Person.first = true

theorem Deal2024.yf_1_2 : isLicit youFirst Person.first Person.second = false

theorem Deal2024.yf_3_2 : isLicit youFirst Person.third Person.second = false

theorem Deal2024.yf_2_2 : isLicit youFirst Person.second Person.second = false

theorem Deal2024.ad_2_1 : isLicit aDescending Person.second Person.first = true

theorem Deal2024.ad_2_3 : isLicit aDescending Person.second Person.third = true

theorem Deal2024.ad_1_3 : isLicit aDescending Person.first Person.third = true

theorem Deal2024.ad_3_3 : isLicit aDescending Person.third Person.third = true

theorem Deal2024.ad_1_1 : isLicit aDescending Person.first Person.first = true

theorem Deal2024.ad_1_2 : isLicit aDescending Person.first Person.second = false

theorem Deal2024.ad_3_1 : isLicit aDescending Person.third Person.first = false

theorem Deal2024.ad_3_2 : isLicit aDescending Person.third Person.second = false

theorem Deal2024.ad_2_2 : isLicit aDescending Person.second Person.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_ : Person) : Bool

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

[Dea24] §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 Person.third Person.first = true

theorem Deal2024.rsd_3_2_ok : reverseLicit reverseSD Person.third Person.second = true

theorem Deal2024.rsd_2_1_ok : reverseLicit reverseSD Person.second Person.first = true

theorem Deal2024.rsd_1_3_bad : reverseLicit reverseSD Person.first Person.third = false

theorem Deal2024.rsd_2_3_bad : reverseLicit reverseSD Person.second Person.third = false

theorem Deal2024.rsd_1_2_bad : reverseLicit reverseSD Person.first Person.second = false

theorem Deal2024.strong_iff_3p_do (io do_ : Person) : isLicit strong io do_ = true ↔ ¬do_.IsSAP

Strong PCC (2a): DO must be 3P — i.e. [−participant], which over the full inventory is exactly non-SAP. Any IO is licit with a non-SAP DO; any SAP DO is illicit regardless of IO.

theorem Deal2024.weak_illicit_iff (io do_ : Person) : isLicit weak io do_ = false ↔ ¬io.IsSAP ∧ do_.IsSAP

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

theorem Deal2024.mefirst_iff_not_1p_do (io do_ : Person) : 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_ : Person) (h : Minimalist.decomposePerson io ≠ Minimalist.decomposePerson do_) : isLicit strictlyDescending io do_ = true ↔ io.prominence > do_.prominence

Strictly descending PCC (2d): IO must outrank DO on 1 > 2 > 3 (prominence). For featurally distinct cells, this is exactly the pattern. (Featurally identical cells — ⟨3,3⟩, ⟨2,2⟩, and the cells the two-feature system conflates — are licit except ⟨1,1⟩, where SAT:[SPKR] fires.)

theorem Deal2024.strong_entails_sd (io do_ : Person) : 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 : Person) : 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 Phi/Geometry.lean. This makes the connection structural — Deal's person features are not independently stipulated but derived from the same privative geometry used by [PZ18]'s satisfiesProminence and [BR09]'s personSpec.

Bridge: feature gluttony ([CK21])

The paper engages [CK21] directly (PF ramifications of Agree "per Coon and Keine (2021)"; both are responses to the same PCC typology). The two mechanisms — a probe that stops too early (satisfaction) vs. a probe that agrees too much (gluttony) — coincide on the strong and weak varieties cell-for-cell, and part ways exactly on Me-First's 1>1 cell: Deal's [SAT:SPKR] probe is satisfied by a first-person DO regardless of the IO (illicit), while a gluttony probe fully matched by a first-person IO cannot glutton (licit). [PZ18]'s me-first grammar sides with Deal on that cell.

theorem Deal2024.strong_weak_match_gluttony : (∀ io ∈ Deal2024.grid3✝, ∀ do_ ∈ Deal2024.grid3✝, isLicit strong io do_ = true ↔ ¬CoonKeine2021.pccViolation CoonKeine2021.weakProbe true io do_) ∧ ∀ io ∈ Deal2024.grid3✝, ∀ do_ ∈ Deal2024.grid3✝, isLicit weak io do_ = true ↔ ¬CoonKeine2021.pccViolation CoonKeine2021.weakProbe false io do_

Strong and weak coincide with gluttony cell-for-cell: Deal's strong = K-opaque-dative gluttony; Deal's weak = transparent weak-probe gluttony.

theorem Deal2024.mefirst_diverges_from_gluttony : (∀ io ∈ Deal2024.grid3✝, ∀ do_ ∈ Deal2024.grid3✝, (io, do_) ≠ (Person.first, Person.first) → (isLicit meFirst io do_ = true ↔ ¬CoonKeine2021.pccViolation CoonKeine2021.meFirstProbe false io do_)) ∧ isLicit meFirst Person.first Person.first = false ∧ ¬CoonKeine2021.pccViolation CoonKeine2021.meFirstProbe false Person.first Person.first

Me-First diverges from gluttony exactly at 1>1: satisfaction bans it, gluttony permits it. All other cells agree.