Deal (2026): Clausal complementation as relativization, revisited

[Dea26]

Paper's central claims

In Nez Perce, some but not all notional complement clauses show the characteristic morphology of relativization. [Dea26] argues that the relative-like notional complement clauses ("relative embeddings", REs) are CPs — not DPs/PPs — containing an internal Ā-dependency from a high functional projection above TP. Three primary conclusions:

1. Not all clausal complementation is relativization (refuting [Kay08], [Kay14], [Ars09]).
2. Relative-like notional complement clauses vary across languages in nominal superstructure ([Dea26] Table 79: V CP / V D N CP / V P D CP) and in factive inferences (Tables 80–81).
3. Factivity, RE-syntax, and nominalization are three orthogonal axes — no one entails another.

What this file contributes

• The bundled NotionalComplementShape analytical record (Deal-specific apparatus per CLAUDE.md "paper-specific apparatus stays in Studies").
• Table 79 sample: V CP / V D N CP / V P D CP cells for five languages.
• The nezPerceEmbedStrategy projection: derives RE-vs-simplex from Fragment-level Noonan/factivity data plus the Deal-analytical Ā-dep presence flag.
• ke-agreement as Minimalist.SatisfactionCond.disjunctive ([Dea15], [Dea24] framework; bridge to Syntax/Minimalist/Agree.lean §14).
• Cross-classification theorems: factivity ⊥ RE-structure; factivity ⊥ nominalization.
• Cross-framework comparison notes (HPSG modifier-only RC; Cacchioli 2025 Tigrinya in-system counterargument).

What this file does NOT contribute

• §6 indexical-shift / sequence-of-tense formal predictions: deferred pending a Kaplanian-context-shifting substrate ([deal-2020] book is the reference theory). Existing deal-2020 bib entry but no implementation module.
• A full HPSG-side bridge theorem: documented as silent divergence; formalisation requires updating HPSG/RelativeClauses.lean to parameterise its currently-hardcoded MOD NP analysis.
• A commentative-emitting fix to deriveCTPClass in Studies/Noonan2007.lean: blocked on VerbEntry schema (regret and know have identical features in Fragments/English/Predicates/Verbal.lean).

Disagreements documented but not formalised

[Kay08], [Kay14], [Ars09]: universalist position (all complementation = relativization). Deal 2026 §7 refutes by exhibiting bare-CP cells with no internal Ā-dependency.

[dC17]: opposing position — complement clauses are never relatives. Compatible with Deal 2026 for English simplex; incompatible with Deal for Adyghe/Bulgarian/Nez Perce REs.

[HB17], [BH21]: Washo factive complementation as nominalization (V D CP). Deal 2026 §7 accepts this for Washo but refutes the universal extension to all factives — Nez Perce REs are factive without nominal superstructure.

[Mou15]: CPs are predicates (type ⟨e, t⟩), not propositions (type t), composing with attitude verbs via predicate modification. This analysis is orthogonal to Deal 2026's typology — it concerns the semantic type of the embedded CP, not its external syntactic shell. The two analyses intersect on barePropositionalCP cells (Moulton's CP-predicate semantics applies most directly there) but Deal's nominalization cells (V D N CP, V P D CP) shift composition into the nominal layer where Moulton's predicate-modification mechanism may not directly apply.

structure Deal2026.NotionalComplementShape : Type

The full Deal-2026 description of a notional complement clause: internal spine + external shell + presence of internal Ā-dependency. Bundled here rather than in substrate to keep the per-axis primitives reusable (ClauseSpine, Slot.ShellInventory, AbarDep) for non-Deal accounts.

The three axes are independent in [Dea26] Table 79: each cell in the 4×2 cross-classification (CP-superstructure × ±Ā) is filled or explicitly noted as predicted-but-unattested.

• internal : Minimalist.ClauseSpine

  Internal spine of the embedded clause (typically ClauseSpine.cP).

• external : Slot.ShellInventory

  External wrapping shells from C outward (bareCP / dCP / dnCP / pdCP).

• hasInternalAbar : Bool

  Whether the embedded CP contains an internal Ā-dependency.

@[implicit_reducible]

instance Deal2026.instReprNotionalComplementShape : Repr NotionalComplementShape

Equations

• Deal2026.instReprNotionalComplementShape = { reprPrec := Deal2026.instReprNotionalComplementShape.repr }

def Deal2026.instReprNotionalComplementShape.repr : NotionalComplementShape → ℕ → Std.Format

Equations

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

def Deal2026.nezPerceREShape : NotionalComplementShape

The two Nez Perce shapes from [Dea26] §3 vs §6.

Equations

• Deal2026.nezPerceREShape = { internal := Minimalist.ClauseSpine.cP, external := Slot.ShellInventory.bareCP, hasInternalAbar := true }

def Deal2026.nezPerceSimplexShape : NotionalComplementShape

Equations

• Deal2026.nezPerceSimplexShape = { internal := Minimalist.ClauseSpine.cP, external := Slot.ShellInventory.bareCP, hasInternalAbar := false }

def Deal2026.adygheREShape : NotionalComplementShape

The Adyghe RE shape from [CP11a], exhibited at [Dea26] §4 (43): V D N CP with internal Ā.

Equations

• Deal2026.adygheREShape = { internal := Minimalist.ClauseSpine.cP, external := Slot.ShellInventory.dnCP, hasInternalAbar := true }

def Deal2026.bulgarianREShape : NotionalComplementShape

The Bulgarian RE shape from [Kra10], exhibited at [Dea26] §4 (49): V P D CP with internal Ā.

Equations

• Deal2026.bulgarianREShape = { internal := Minimalist.ClauseSpine.cP, external := Slot.ShellInventory.pdCP, hasInternalAbar := true }

def Deal2026.ndebeleShape : NotionalComplementShape

The Ndebele simplex shape from [Pie19], exhibited at [Dea26] §7 (78): V P D CP with no Ā-dependency.

Equations

• Deal2026.ndebeleShape = { internal := Minimalist.ClauseSpine.cP, external := Slot.ShellInventory.pdCP, hasInternalAbar := false }

def Deal2026.washoShape : NotionalComplementShape

The Washo factive shape from [BH21], [HB17]: V D CP (D wraps CP, no intervening N). [Dea26] footnote 33 explicitly notes this cell as attested "for example, for Washo (Bochnak & Hanink 2021)" but absent from the main Table 79 because no example language combines V D CP with an internal Ā-dependency. We include the no-Ā version.

Equations

• Deal2026.washoShape = { internal := Minimalist.ClauseSpine.cP, external := Slot.ShellInventory.dCP, hasInternalAbar := false }

structure Deal2026.Table79Cell : Type

An entry in [Dea26] Table 79: a language × construction with its NotionalComplementShape.

• language : String
• construction : String
• shape : NotionalComplementShape

@[implicit_reducible]

instance Deal2026.instReprTable79Cell : Repr Table79Cell

Equations

• Deal2026.instReprTable79Cell = { reprPrec := Deal2026.instReprTable79Cell.repr }

def Deal2026.instReprTable79Cell.repr : Table79Cell → ℕ → Std.Format

Equations

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

def Deal2026.table79 : List Table79Cell

The seven attested Table-79 cells (Deal 2026 main Table 79 + Washo cell from footnote 33 per [BH21]).

Equations

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

theorem Deal2026.table79_membership : List.map (fun (c : Table79Cell) => (c.language, c.construction)) table79 = [("Nez Perce", "RE"), ("Nez Perce", "simplex"), ("English", "think-complement"), ("Adyghe", "RE"), ("Bulgarian", "RE"), ("Ndebele", "embedding"), ("Washo", "factive")]

Drift sentry: table79 covers exactly the seven (language, construction) pairs Deal lists in §7 main Table 79 plus the Washo cell from footnote 33.

theorem Deal2026.kayne_universalism_refuted : ¬∀ c ∈ table79, c.shape.hasInternalAbar = true

The Kayne-Arsenij'evi'c universalist hypothesis — that all clausal complementation is relativization — stated on the Ā-axis: not every Table 79 cell carries an internal Ā-dependency. (The retired surface-enum version undercounted — Adyghe/Bulgarian REs DO relativize, inside a nominal shell, and are not counterexamples; the counterexamples are the no-Ā cells: Nez Perce simplex, English think, Ndebele, Washo.)

theorem Deal2026.table79_axes_attested : (∃ c ∈ table79, c.shape.external = Slot.ShellInventory.bareCP ∧ c.shape.hasInternalAbar = true) ∧ (∃ c ∈ table79, c.shape.external = Slot.ShellInventory.bareCP ∧ c.shape.hasInternalAbar = false) ∧ ∃ c ∈ table79, c.shape.external.hasNominalShell

Deal 2026's positive contribution, on the two axes: bare CP + Ā attested (REs are real); bare CP without Ā attested (not all complementation is relativization); a nominal shell attested (consistent with prior nominalization analyses for some languages).

theorem Deal2026.shelled_REs_attested : ∃ c ∈ table79, c.shape.external.hasNominalShell ∧ c.shape.hasInternalAbar = true

The combination the surface enum could not express — claim 2: REs vary in nominal superstructure (Adyghe V D N CP, Bulgarian V P D CP carry Ā inside a nominal shell).

def Deal2026.greekPuComplementShape : NotionalComplementShape

Greek pu-complement shape per [Ang26]: bare CP with no internal Ā-dependency and no nominal shell (Greek lacks a silent situation noun, so pu cannot nominalize per paper §5). The categorial [n]-feature on C is checked structurally (light noun in Spec) rather than by a nominal shell — witnessing that the (factive, bare-CP) combination is attested.

Equations

• Deal2026.greekPuComplementShape = { internal := Minimalist.ClauseSpine.cP, external := Slot.ShellInventory.bareCP, hasInternalAbar := false }

Headline orthogonality (Deal 2026 Tables 80–81)

The central typological discovery: factivity does not predict RE-structure in either direction.

• Factive + RE-structure: Nez Perce REs (e.g. liloy 'be happy').
• Factive + simplex: Nez Perce cuukwe 'know'.
• Non-factive + RE-structure: Adyghe REs (per [CP11a]).
• Non-factive + simplex: Nez Perce neki/hi; English think.

theorem Deal2026.factivity_perp_re_structure : NezPerce.ClausalEmbedding.liloy.factive = true ∧ nezPerceREShape.hasInternalAbar = true ∧ NezPerce.ClausalEmbedding.cuukwe.factive = true ∧ nezPerceSimplexShape.hasInternalAbar = false ∧ NezPerce.ClausalEmbedding.neki.factive = false ∧ nezPerceSimplexShape.hasInternalAbar = false

All four cells are attested: factivity neither necessitates nor precludes RE-syntax. The factive flag is per [Dea26] §3 projection-test diagnoses. The Adyghe non-factive RE judgement is attributed to [CP11a] via [Dea26] §7 Table 80.

The fourth cell (non-factive + RE)

Documented by [Dea26] §7 (Table 80) as instantiated by Adyghe per [CP11a]. Absent a formalised Adyghe Fragment, this is recorded as an unproven Lean claim: in linglib Adyghe is not yet present at Fragment level.

TODO(adyghe-fragment): once Fragments/Adyghe/ClausalEmbedding.lean lands, replace this prose with a theorem adyghe_re_nonfactive.

Deal 2026 Table 81

• Factive + nominalization: Washo forget (per [HB17]).
• Factive + no nominalization: Nez Perce REs (the headline Deal-2026 finding, refuting the [HB17] universal extension).
• Non-factive + nominalization: Turkish düşün- 'think' (per [Dea26] §7 citing Özyıldız 2017).
• Non-factive + no nominalization: Washo, Nez Perce 'think'.

theorem Deal2026.nezPerce_re_factive_no_nominalization : NezPerce.ClausalEmbedding.liloy.factive = true ∧ nezPerceREShape.external = Slot.ShellInventory.bareCP

Nez Perce REs are factive without external nominal shell.

theorem Deal2026.bareCP_no_d_no_n : Slot.Shell.d ∉ Slot.ShellInventory.bareCP ∧ Slot.Shell.n ∉ Slot.ShellInventory.bareCP

The bare-CP shell contains neither D nor N.

Observable-driven derivation (Pattern B architecture)

The Fragment carries a single morphological observable (requiresYoxKeEdge : Bool) per [Dea26] §3 (28). Deal's two analytical commitments — the embedding-strategy classification and the selectional-feature stack — are derived from this observable, not stipulated alongside it. The derivation is the theory; the observable is the data.

This pattern lets alternative theories provide alternative derivation functions over the same Fragment observable, making cross-theory divergence theorems expressible (currently only Deal's derivation is supplied; an Adyghe-style or Krapova-style derivation would be a straightforward sibling Studies file).

inductive Deal2026.EmbeddingStrategy : Type

The two embedding strategies [Dea26] distinguishes.

• re : EmbeddingStrategy
• simplex : EmbeddingStrategy

@[implicit_reducible]

instance Deal2026.instDecidableEqEmbeddingStrategy : DecidableEq EmbeddingStrategy

Equations

• Deal2026.instDecidableEqEmbeddingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Deal2026.instReprEmbeddingStrategy.repr : EmbeddingStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Deal2026.instReprEmbeddingStrategy : Repr EmbeddingStrategy

Equations

• Deal2026.instReprEmbeddingStrategy = { reprPrec := Deal2026.instReprEmbeddingStrategy.repr }

def Deal2026.nezPerceEmbedStrategy (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : EmbeddingStrategy

Deal 2026's per-verb embedding-strategy classification, derived from the Fragment-level observable requiresYoxKeEdge. The interpretation is Deal's: morphological obligation of yox̂ ke on the complement edge ↔ syntactic Ā-dependency above TP. The bi-conditional is strategy_iff_yoxKe below — was previously trivially rfl over a list-membership check, now expresses the genuine theory commitment.

Equations

• Deal2026.nezPerceEmbedStrategy v = if v.requiresYoxKeEdge = true then Deal2026.EmbeddingStrategy.re else Deal2026.EmbeddingStrategy.simplex

structure Deal2026.DealSelectionalProfile : Type

Deal's selectional commitment for a Nez Perce embedder: the verb c-selects a CP, and (for RE-takers) requires that CP to contain an internal Ā-dependency above TP.

Note that Deal's analysis is not standard c-selection: c-selection only sees the outer category of the complement, and both RE-takers and simplex-takers c-select uniformly for .C (a CP). The RE-vs-simplex distinction is in the internal structure of the selected CP — whether its head bears the [+Ā] feature triggering operator movement above TP. We separate the two by storing both the c-selectional outer category and a Boolean flag for the internal-Ā requirement.

• outerCat : Minimalist.Cat

  Outer category the verb c-selects for (always .C for embedders).

• requiresInternalAbar : Bool

  Whether the selected CP must contain an internal Ā-dependency. Maps to Deal's [+Ā] feature on the C head of the embedded clause.

def Deal2026.instDecidableEqDealSelectionalProfile.decEq (x✝ x✝¹ : DealSelectionalProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Deal2026.instDecidableEqDealSelectionalProfile : DecidableEq DealSelectionalProfile

Equations

• Deal2026.instDecidableEqDealSelectionalProfile = Deal2026.instDecidableEqDealSelectionalProfile.decEq

def Deal2026.instReprDealSelectionalProfile.repr : DealSelectionalProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Deal2026.instReprDealSelectionalProfile : Repr DealSelectionalProfile

Equations

• Deal2026.instReprDealSelectionalProfile = { reprPrec := Deal2026.instReprDealSelectionalProfile.repr }

def Deal2026.dealSelectionalProfile (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : DealSelectionalProfile

Deal 2026's selectional analysis: derived entirely from the Fragment observable requiresYoxKeEdge. The verb uniformly c-selects for a CP; only the internal-Ā requirement varies between RE-takers and simplex-takers.

Equations

• Deal2026.dealSelectionalProfile v = { outerCat := Minimalist.Cat.C, requiresInternalAbar := v.requiresYoxKeEdge }

theorem Deal2026.strategy_iff_yoxKe (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : nezPerceEmbedStrategy v = EmbeddingStrategy.re ↔ v.requiresYoxKeEdge = true

The headline derivation theorem: a Nez Perce embedder is RE-canonical in Deal's analysis iff its complement obligatorily carries the yox̂ ke edge morphology. Replaces what was previously a trivial rfl over membership in a hand-curated list.

theorem Deal2026.requiresInternalAbar_iff_yoxKe (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : (dealSelectionalProfile v).requiresInternalAbar = v.requiresYoxKeEdge

Deal's selectional analysis: an embedder selects for a CP with internal Ā-dependency iff it requires yox̂ ke edge marking.

theorem Deal2026.all_embedders_select_C (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : (dealSelectionalProfile v).outerCat = Minimalist.Cat.C

Every Nez Perce embedder uniformly c-selects for .C. The RE-vs-simplex contrast is not a c-selectional difference — it lives in the internal structure of the selected CP.

theorem Deal2026.liloy_strategy : nezPerceEmbedStrategy NezPerce.ClausalEmbedding.liloy = EmbeddingStrategy.re

Per-verb sanity checks (decidable lookup of the observable).

theorem Deal2026.timiipni_strategy : nezPerceEmbedStrategy NezPerce.ClausalEmbedding.timiipni = EmbeddingStrategy.re

theorem Deal2026.qeciyeewyew_strategy : nezPerceEmbedStrategy NezPerce.ClausalEmbedding.qeciyeewyew = EmbeddingStrategy.re

theorem Deal2026.neki_strategy : nezPerceEmbedStrategy NezPerce.ClausalEmbedding.neki = EmbeddingStrategy.simplex

theorem Deal2026.hi_strategy : nezPerceEmbedStrategy NezPerce.ClausalEmbedding.hi = EmbeddingStrategy.simplex

theorem Deal2026.cuukwe_strategy : nezPerceEmbedStrategy NezPerce.ClausalEmbedding.cuukwe = EmbeddingStrategy.simplex

theorem Deal2026.liloy_selProfile : dealSelectionalProfile NezPerce.ClausalEmbedding.liloy = { outerCat := Minimalist.Cat.C, requiresInternalAbar := true }

Per-verb selectional sanity. liloy selects a CP requiring internal Ā; neki selects a bare CP.

theorem Deal2026.neki_selProfile : dealSelectionalProfile NezPerce.ClausalEmbedding.neki = { outerCat := Minimalist.Cat.C, requiresInternalAbar := false }

theorem Deal2026.reCanonical_strategy (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : v ∈ NezPerce.ClausalEmbedding.reCanonical → nezPerceEmbedStrategy v = EmbeddingStrategy.re

Every RE-canonical embedder gets EmbeddingStrategy.re (now follows from the Fragment observable, not from list-membership).

Bridge to [TBRS13] taxonomy

The Tonhauser et al. classes are formalised in Semantics/Presupposition/ProjectiveContent.lean (ProjectiveClass.classA– classD). Factive predicates project as Class C (SCF=no, OLE=yes — the same class as English know). The Class C trigger know_complement is one of the listed examples (see ProjectiveTrigger.know_complement).

Non-factive predicates introduce no projective content and so map to none.

def Deal2026.derivedProjectiveClass (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : Option Semantics.Presupposition.ProjectiveContent.ProjectiveClass

Project a Nez Perce embedder onto the Tonhauser projective-content taxonomy. Factive predicates map to Class C (the know-class); non-factives have no projective content.

Equations

• Deal2026.derivedProjectiveClass v = if v.factive = true then some Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC else none

theorem Deal2026.reCanonical_projects_classC : (NezPerce.ClausalEmbedding.reCanonical.all fun (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) => decide (derivedProjectiveClass v = some Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC)) = true

All RE-canonical predicates project as Tonhauser Class C. This bridges Deal's empirical Nez Perce data to the typed [TBRS13] taxonomy.

theorem Deal2026.cuukwe_projects_classC : derivedProjectiveClass NezPerce.ClausalEmbedding.cuukwe = some Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC

cuukwe 'know' projects as Class C — same projective class as Deal-RE-canonical predicates, despite cuukwe being simplex-canonical. Confirms factivity ⊥ RE-structure at the Tonhauser-substrate level.

theorem Deal2026.neki_no_projection : derivedProjectiveClass NezPerce.ClausalEmbedding.neki = none

neki 'think' has no projective content (non-factive).

Bridges between four substrate layers

The Studies file integrates four independent substrate layers:

• Fragment: per-verb consensus typology (CTPClass, factive)
• Tonhauser projective content: ProjectiveClass (Semantics/Presupposition/)
• Deal-internal: EmbeddingStrategy + NotionalComplementShape
• Shell/Ā axes: Slot.ShellInventory + hasNominalShell (Syntax/Clause/Frame.lean)

The bridge theorems below derive load-bearing predictions across these layers rather than stipulating them.

def Deal2026.EmbeddingStrategy.shape : EmbeddingStrategy → NotionalComplementShape

The analytical shape associated with each embedding strategy. re predicates select nezPerceREShape; simplex predicates select nezPerceSimplexShape.

Equations

• Deal2026.EmbeddingStrategy.re.shape = Deal2026.nezPerceREShape
• Deal2026.EmbeddingStrategy.simplex.shape = Deal2026.nezPerceSimplexShape

theorem Deal2026.strategy_shape_abar (v : NezPerce.ClausalEmbedding.NezPerceEmbedder) : (nezPerceEmbedStrategy v).shape.hasInternalAbar = v.requiresYoxKeEdge

Strategy-shape correspondence on the Ā-axis: the shape an embedder's strategy selects carries an internal Ā-dependency exactly when the Fragment observable holds.

theorem Deal2026.all_REs_have_internal_abar : nezPerceREShape.hasInternalAbar = true ∧ adygheREShape.hasInternalAbar = true ∧ bulgarianREShape.hasInternalAbar = true

All three Table-79 RE cells (Nez Perce, Adyghe, Bulgarian) carry an internal Ā-dependency. The shared hasInternalAbar = true is the universal property of REs that survives Deal's typological dissolution.

theorem Deal2026.all_simplex_lack_internal_abar : nezPerceSimplexShape.hasInternalAbar = false ∧ ndebeleShape.hasInternalAbar = false ∧ washoShape.hasInternalAbar = false

All three Table-79 simplex/embedding cells (Nez Perce simplex, English think, Ndebele, Washo factive) lack internal Ā.

theorem Deal2026.cross_classification_populated : (NezPerce.ClausalEmbedding.liloy.factive = true ∧ nezPerceREShape.hasInternalAbar = true) ∧ (NezPerce.ClausalEmbedding.cuukwe.factive = true ∧ nezPerceSimplexShape.hasInternalAbar = false) ∧ adygheREShape.hasInternalAbar = true ∧ NezPerce.ClausalEmbedding.neki.factive = false ∧ nezPerceSimplexShape.hasInternalAbar = false

The four-cell cross-classification of Tables 80–81 is exhaustively populated: every combination of (factive, hasInternalAbar) is attested by at least one (verb, shape) pair. The fourth cell (non-factive + Ā) is documented from [CP11a]'s Adyghe REs as cited by Deal — Adyghe REs combine adygheREShape (hasInternalAbar=true) with predicates that are not factive in Caponigro & Polinsky's analysis (Deal §7 p. 53).

What Tonhauser substrate alone CANNOT see

The headline cross-classification's fourth cell (factive + simplex, Nez Perce cuukwe) and first cell (factive + RE, Nez Perce liloy) both project to Tonhauser Class C. The Tonhauser substrate alone cannot distinguish them — the distinction lives at the EmbeddingStrategy / NotionalComplementShape layer, not at the projective-content layer.

This is informative: it shows that Deal's typology is strictly finer- grained than Tonhauser's, and motivates the need for substrate at the Probe / ClauseSpine layer (where the Ā-dep distinction is visible).

theorem Deal2026.tonhauser_fails_to_distinguish_cuukwe_liloy : derivedProjectiveClass NezPerce.ClausalEmbedding.cuukwe = derivedProjectiveClass NezPerce.ClausalEmbedding.liloy

Tonhauser projective class does not distinguish cuukwe from liloy.

theorem Deal2026.strategy_distinguishes_cuukwe_liloy : nezPerceEmbedStrategy NezPerce.ClausalEmbedding.cuukwe ≠ nezPerceEmbedStrategy NezPerce.ClausalEmbedding.liloy

But the embedding-strategy projection DOES distinguish them.

ke as a φ-probe on C ([Dea15])

[Dea26] §2 argues ke is a C-head with a φ-probe rather than a relative pronoun. The argument: ke's φ-features track the embedded subject (sometimes plus object), starting from the highest argument and proceeding down — exactly the [Dea15] interaction-satisfaction algorithm probing into c-command domain.

The C-probe is satisfied either by feature-match (yielding overt person agreement) or by encountering the TP boundary (yielding null surface agreement). We model this with [Dea24]'s SatisfactionCond.disjunctive.

Caveat: the existing Agree.lean featuresMatch uses sameType matching (see Agree.lean:234), which collapses 1st/2nd/3rd person into a single "person feature type." A finer-grained valueMatch substrate would be needed to formalise Deal's 1st vs 3rd person split. The disjunctive shape here is faithful to the framework but currently distinguishes only "person-feature-present" vs "no-feature-encountered-T."

def Deal2026.keSatisfaction : Minimalist.SatisfactionCond

ke's satisfaction condition: matched by any φ-feature (collapsed by sameType regardless of person value), or by encountering the TP head.

Equations

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

theorem Deal2026.ke_satisfied_by_phi : keSatisfaction.isSatisfied (Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person Person.first))]) none = true

ke is satisfied by a subject bearing person features (any person, due to sameType matching in Agree.lean).

theorem Deal2026.ke_satisfied_by_head_encounter : keSatisfaction.isSatisfied ⊥ (some Minimalist.Cat.T) = true

ke is satisfied by encountering the TP boundary even with no φ-features on the goal — the disjunctive escape that yields null surface agreement.

theorem Deal2026.ke_head_encounter_no_copy : keSatisfaction.copiedFeatures ⊥ (some Minimalist.Cat.T) = false

The head-encounter satisfaction copies no features (default null surface agreement when subject lacks φ).

REs contain a high Ā-dependency ([Dea26] §5)

Deal §5 argues the relative operator originates above TP — a high functional projection — based on absence of low-position cyclic effects and the always-nominative form of the relative pronoun. We attach the existing keineĀDep (Ā-probe on C, fValue 6) as the substrate witness; the alternative low analysis (Aboh's Gungbe lexical-Ā) is documented but not formalised.

@[reducible, inline]

abbrev Deal2026.reInternalAbar : Minimalist.AbarDep

A Nez Perce RE's internal Ā-dependency is — in Probe-substrate terms — Minimalist.keineĀDep (the substrate witness defined in Probe.lean §4b). Deal's "high functional projection above TP" claim falls out of Minimalist.keineĀDep_isHigh without re-stipulation here.

Equations

• Deal2026.reInternalAbar = Minimalist.keineĀDep

theorem Deal2026.reInternalAbar_isHigh : reInternalAbar.isHigh = true

The Nez Perce RE Ā-dependency is "high" in Deal's sense: above TP. Inherited directly from the substrate theorem, no re-proof.

Silent divergence with HPSG

Syntax/HPSG/RelativeClauses.lean:87-93 hard-codes RC = modifier (isMod = true, theorem relClause_is_modifier). [Dea26]'s analysis of Nez Perce REs as complement CPs (not modifier RCs) sits incompatibly with this Minimalist-only framing: HPSG would either need to recognise REs as a third structural type (not modifier, not bare complementation), or accept that the RE-vs-RC distinction is a Minimalist-internal one with no HPSG analogue. The bridge theorem HPSG.isMod ↔ ¬ Minimalist.cp_complementation_via_re is filed as future work — promoted from "implicit assumption" to a substrate question.

Healthy convergence with Cacchioli 2025

Studies/Cacchioli2025.lean independently establishes that Tigrinya distinguishes kemzi (factive complementizer) from zi (relativizer/general subordinator) without syncretism. This is a language-internal counterargument to the universalist "complementation = relativization" claim, parallel to [Dea26]'s Nez Perce-internal contrast between simplex (no yox̂ ke) and RE (with yox̂ ke) embeddings. The two papers reinforce each other across distinct language families.

Convergence with Caponigro & Polinsky 2011

[CP11a]'s Adyghe analysis shares Deal's "high Ā origin" claim while diverging on the V D N CP shell shape. Deal 2026 §5 explicitly cites Caponigro & Polinsky as theoretical kin.

§6 indexical shift / SoT formalisation deferred

[Dea26] §6 establishes that REs block shifty pronouns and require matching tense (vs. simplex embeddings where shift and relative-tense are both available). The semantic substrate for these claims is [Dea20]'s A Theory of Indexical Shift book; that substrate is not yet implemented in linglib (no Semantics/IndexicalShift/ directory exists; existing Semantics/Reference/{ShiftedIndexicals, Monsters,Kaplan}.lean cover Kaplanian framing but not Deal's Σ-monsters specifically).

Until the substrate lands, the §6 contrasts can only be documented in prose. Decide-checking a shiftedReading? : Sentence → Bool = false predicate would be the "encoding conclusions as definitions" anti-pattern.

Future work: import deal-2020 substrate (when implemented) and prove re_blocks_shift : ∀ p ∈ reCanonical, p.allowsShift = false against actual indexical-shift semantics.