Deal (2026): Clausal complementation as relativization, revisited

@cite{deal-2026}

Paper's central claims

In Nez Perce, some but not all notional complement clauses show the characteristic morphology of relativization. @cite{deal-2026} 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 @cite{kayne-2008}, @cite{kayne-2014}, @cite{arsenijevic-2009}).
2. Relative-like notional complement clauses vary across languages in nominal superstructure (@cite{deal-2026} 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 (@cite{deal-2015a-nels}, @cite{deal-2024} framework; bridge to Theories/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 (@cite{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/Core/RelativeClauses.lean to parameterise its currently-hardcoded MOD NP analysis.
• A commentative-emitting fix to deriveCTPClass in Phenomena/Complementation/Studies/Noonan2007.lean:570: blocked on VerbEntry schema (regret and know have identical features in Fragments/English/Predicates/Verbal.lean).

Disagreements documented but not formalised

@cite{kayne-2008}, @cite{kayne-2014}, @cite{arsenijevic-2009}: universalist position (all complementation = relativization). Deal 2026 §7 refutes by exhibiting barePropositionalCP cells.

@cite{decuba-2017}: opposing position — complement clauses are never relatives. Compatible with Deal 2026 for English simplex; incompatible with Deal for Adyghe/Bulgarian/Nez Perce REs.

@cite{hanink-bochnak-2017}, @cite{bochnak-hanink-2021}: 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.

@cite{moulton-2015}: 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 Phenomena.Complementation.Studies.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, CPShellInventory, AbarDep) for non-Deal accounts.

The three axes are independent in @cite{deal-2026} 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 : Typology.Complementation.CPShellInventory

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

• hasInternalAbar : Bool

  Whether the embedded CP contains an internal Ā-dependency.

@[implicit_reducible]

instance Phenomena.Complementation.Studies.Deal2026.instReprNotionalComplementShape : Repr NotionalComplementShape

Equations

• Phenomena.Complementation.Studies.Deal2026.instReprNotionalComplementShape = { reprPrec := Phenomena.Complementation.Studies.Deal2026.instReprNotionalComplementShape.repr }

def Phenomena.Complementation.Studies.Deal2026.instReprNotionalComplementShape.repr : NotionalComplementShape → ℕ → Std.Format

Equations

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

def Phenomena.Complementation.Studies.Deal2026.nezPerceREShape : NotionalComplementShape

The two Nez Perce shapes from @cite{deal-2026} §3 vs §6.

Equations

• Phenomena.Complementation.Studies.Deal2026.nezPerceREShape = { internal := Minimalist.ClauseSpine.cP, external := Typology.Complementation.bareCP, hasInternalAbar := true }

def Phenomena.Complementation.Studies.Deal2026.nezPerceSimplexShape : NotionalComplementShape

Equations

• Phenomena.Complementation.Studies.Deal2026.nezPerceSimplexShape = { internal := Minimalist.ClauseSpine.cP, external := Typology.Complementation.bareCP, hasInternalAbar := false }

def Phenomena.Complementation.Studies.Deal2026.adygheREShape : NotionalComplementShape

The Adyghe RE shape from @cite{caponigro-polinsky-2011}, exhibited at @cite{deal-2026} §4 (43): V D N CP with internal Ā.

Equations

• Phenomena.Complementation.Studies.Deal2026.adygheREShape = { internal := Minimalist.ClauseSpine.cP, external := Typology.Complementation.dnCP, hasInternalAbar := true }

def Phenomena.Complementation.Studies.Deal2026.bulgarianREShape : NotionalComplementShape

The Bulgarian RE shape from @cite{krapova-2010}, exhibited at @cite{deal-2026} §4 (49): V P D CP with internal Ā.

Equations

• Phenomena.Complementation.Studies.Deal2026.bulgarianREShape = { internal := Minimalist.ClauseSpine.cP, external := Typology.Complementation.pdCP, hasInternalAbar := true }

def Phenomena.Complementation.Studies.Deal2026.ndebeleShape : NotionalComplementShape

The Ndebele simplex shape from @cite{pietraszko-2019}, exhibited at @cite{deal-2026} §7 (78): V P D CP with no Ā-dependency.

Equations

• Phenomena.Complementation.Studies.Deal2026.ndebeleShape = { internal := Minimalist.ClauseSpine.cP, external := Typology.Complementation.pdCP, hasInternalAbar := false }

def Phenomena.Complementation.Studies.Deal2026.washoShape : NotionalComplementShape

The Washo factive shape from @cite{bochnak-hanink-2021}, @cite{hanink-bochnak-2017}: V D CP (D wraps CP, no intervening N). @cite{deal-2026} 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

• Phenomena.Complementation.Studies.Deal2026.washoShape = { internal := Minimalist.ClauseSpine.cP, external := Typology.Complementation.dCP, hasInternalAbar := false }

structure Phenomena.Complementation.Studies.Deal2026.Table79Cell : Type

An entry in @cite{deal-2026} Table 79: a language × construction with its NotionalComplementShape.

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

@[implicit_reducible]

instance Phenomena.Complementation.Studies.Deal2026.instReprTable79Cell : Repr Table79Cell

Equations

• Phenomena.Complementation.Studies.Deal2026.instReprTable79Cell = { reprPrec := Phenomena.Complementation.Studies.Deal2026.instReprTable79Cell.repr }

def Phenomena.Complementation.Studies.Deal2026.instReprTable79Cell.repr : Table79Cell → ℕ → Std.Format

Equations

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

def Phenomena.Complementation.Studies.Deal2026.table79 : List Table79Cell

The seven attested Table-79 cells (Deal 2026 main Table 79 + Washo cell from footnote 33 per @cite{bochnak-hanink-2021}).

Equations

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

theorem Phenomena.Complementation.Studies.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.

def Phenomena.Complementation.Studies.Deal2026.NotionalComplementShape.surfacePattern (s : NotionalComplementShape) : Typology.Complementation.ComplementClauseStructure

Project a NotionalComplementShape onto the theory-neutral ComplementClauseStructure enum from Typology/Complementation.lean. The mapping is determined by the internal Ā-flag and the external shell: bare CP + Ā = abarInternalCP; bare CP without Ā = barePropositionalCP; any non-bare external shell = nominalization (subsumes V D CP, V D N CP, V P D CP — they differ only in the depth of the nominal/prepositional wrapper, not in the surface phenomenon being a nominalization).

Equations

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

def Phenomena.Complementation.Studies.Deal2026.Table79Cell.surfacePattern (c : Table79Cell) : Typology.Complementation.ComplementClauseStructure

A Table79 cell's surface pattern, derived from its shape.

Equations

• c.surfacePattern = c.shape.surfacePattern

theorem Phenomena.Complementation.Studies.Deal2026.nezPerceRE_surface : nezPerceREShape.surfacePattern = Typology.Complementation.ComplementClauseStructure.abarInternalCP

Nez Perce REs project as abarInternalCP (bare CP + Ā).

theorem Phenomena.Complementation.Studies.Deal2026.nezPerceSimplex_surface : nezPerceSimplexShape.surfacePattern = Typology.Complementation.ComplementClauseStructure.barePropositionalCP

Nez Perce simplex (and English think) project as barePropositionalCP.

theorem Phenomena.Complementation.Studies.Deal2026.adygheRE_surface : adygheREShape.surfacePattern = Typology.Complementation.ComplementClauseStructure.nominalization

Adyghe REs project as nominalization (V D N CP).

theorem Phenomena.Complementation.Studies.Deal2026.bulgarianRE_surface : bulgarianREShape.surfacePattern = Typology.Complementation.ComplementClauseStructure.nominalization

Bulgarian REs project as nominalization (V P D CP).

theorem Phenomena.Complementation.Studies.Deal2026.ndebele_surface : ndebeleShape.surfacePattern = Typology.Complementation.ComplementClauseStructure.nominalization

Ndebele embedding projects as nominalization (V P D CP).

theorem Phenomena.Complementation.Studies.Deal2026.washo_surface : washoShape.surfacePattern = Typology.Complementation.ComplementClauseStructure.nominalization

Washo factive embedding projects as nominalization (V D CP, no Ā).

theorem Phenomena.Complementation.Studies.Deal2026.kayne_universalism_refuted : ¬(table79.all fun (x : Table79Cell) => x.surfacePattern == Typology.Complementation.ComplementClauseStructure.abarInternalCP) = true

The Kayne-Arsenij'evi'c universalist hypothesis — that all clausal complementation is relativization — is decidable on the Table 79 sample as ∀ c ∈ table79, c.surfacePattern = .abarInternalCP. Deal 2026 refutes it: only one of six cells (Nez Perce REs) projects as abarInternalCP.

theorem Phenomena.Complementation.Studies.Deal2026.table79_three_surface_patterns_attested : (table79.any fun (x : Table79Cell) => x.surfacePattern == Typology.Complementation.ComplementClauseStructure.abarInternalCP) = true ∧ (table79.any fun (x : Table79Cell) => x.surfacePattern == Typology.Complementation.ComplementClauseStructure.barePropositionalCP) = true ∧ (table79.any fun (x : Table79Cell) => x.surfacePattern == Typology.Complementation.ComplementClauseStructure.nominalization) = true

Deal 2026's positive contribution: at least one cell projects as abarInternalCP (so REs are real); at least one cell projects as barePropositionalCP (so not all complementation is relativization); at least one cell projects as nominalization (consistent with prior nominalization analyses for some languages).

def Phenomena.Complementation.Studies.Deal2026.greekPuComplementShape : NotionalComplementShape

Greek pu-complement shape per @cite{angelopoulos-2026}: bare CP with no internal Ā-dependency — projects as barePropositionalCP, not nominalization (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.

Equations

• Phenomena.Complementation.Studies.Deal2026.greekPuComplementShape = { internal := Minimalist.ClauseSpine.cP, external := Typology.Complementation.bareCP, hasInternalAbar := false }

theorem Phenomena.Complementation.Studies.Deal2026.greekPu_surface : greekPuComplementShape.surfacePattern = Typology.Complementation.ComplementClauseStructure.barePropositionalCP

Greek pu-complement projects as barePropositionalCP — a bare-CP cell consistent with Deal's typology, witnessing that the (factive, bare-CP) combination is attested.

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 @cite{caponigro-polinsky-2011}).
• Non-factive + simplex: Nez Perce neki/hi; English think.

theorem Phenomena.Complementation.Studies.Deal2026.factivity_perp_re_structure : Fragments.NezPerce.ClausalEmbedding.liloy.factive = true ∧ nezPerceREShape.hasInternalAbar = true ∧ Fragments.NezPerce.ClausalEmbedding.cuukwe.factive = true ∧ nezPerceSimplexShape.hasInternalAbar = false ∧ Fragments.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 @cite{deal-2026} §3 projection-test diagnoses. The Adyghe non-factive RE judgement is attributed to @cite{caponigro-polinsky-2011} via @cite{deal-2026} §7 Table 80.

The fourth cell (non-factive + RE)

Documented by @cite{deal-2026} §7 (Table 80) as instantiated by Adyghe per @cite{caponigro-polinsky-2011}. 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 @cite{hanink-bochnak-2017}).
• Factive + no nominalization: Nez Perce REs (the headline Deal-2026 finding, refuting the @cite{hanink-bochnak-2017} universal extension).
• Non-factive + nominalization: Turkish düşün- 'think' (per @cite{deal-2026} §7 citing Özyıldız 2017).
• Non-factive + no nominalization: Washo, Nez Perce 'think'.

theorem Phenomena.Complementation.Studies.Deal2026.nezPerce_re_factive_no_nominalization : Fragments.NezPerce.ClausalEmbedding.liloy.factive = true ∧ nezPerceREShape.external = Typology.Complementation.bareCP

Nez Perce REs are factive without external nominal shell.

theorem Phenomena.Complementation.Studies.Deal2026.bareCP_no_d_no_n : Typology.Complementation.CPShell.d ∉ Typology.Complementation.bareCP ∧ Typology.Complementation.CPShell.n ∉ Typology.Complementation.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 @cite{deal-2026} §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 Phenomena.Complementation.Studies.Deal2026.EmbeddingStrategy : Type

The two embedding strategies @cite{deal-2026} distinguishes.

• re : EmbeddingStrategy
• simplex : EmbeddingStrategy

@[implicit_reducible]

instance Phenomena.Complementation.Studies.Deal2026.instDecidableEqEmbeddingStrategy : DecidableEq EmbeddingStrategy

Equations

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

def Phenomena.Complementation.Studies.Deal2026.instReprEmbeddingStrategy.repr : EmbeddingStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Complementation.Studies.Deal2026.instReprEmbeddingStrategy : Repr EmbeddingStrategy

Equations

• Phenomena.Complementation.Studies.Deal2026.instReprEmbeddingStrategy = { reprPrec := Phenomena.Complementation.Studies.Deal2026.instReprEmbeddingStrategy.repr }

def Phenomena.Complementation.Studies.Deal2026.nezPerceEmbedStrategy (v : Fragments.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

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

structure Phenomena.Complementation.Studies.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 Phenomena.Complementation.Studies.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 Phenomena.Complementation.Studies.Deal2026.instDecidableEqDealSelectionalProfile : DecidableEq DealSelectionalProfile

Equations

• Phenomena.Complementation.Studies.Deal2026.instDecidableEqDealSelectionalProfile = Phenomena.Complementation.Studies.Deal2026.instDecidableEqDealSelectionalProfile.decEq

def Phenomena.Complementation.Studies.Deal2026.instReprDealSelectionalProfile.repr : DealSelectionalProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Complementation.Studies.Deal2026.instReprDealSelectionalProfile : Repr DealSelectionalProfile

Equations

• Phenomena.Complementation.Studies.Deal2026.instReprDealSelectionalProfile = { reprPrec := Phenomena.Complementation.Studies.Deal2026.instReprDealSelectionalProfile.repr }

def Phenomena.Complementation.Studies.Deal2026.dealSelectionalProfile (v : Fragments.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

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

theorem Phenomena.Complementation.Studies.Deal2026.strategy_iff_yoxKe (v : Fragments.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 Phenomena.Complementation.Studies.Deal2026.requiresInternalAbar_iff_yoxKe (v : Fragments.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 Phenomena.Complementation.Studies.Deal2026.all_embedders_select_C (v : Fragments.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 Phenomena.Complementation.Studies.Deal2026.liloy_strategy : nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.liloy = EmbeddingStrategy.re

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

theorem Phenomena.Complementation.Studies.Deal2026.timiipni_strategy : nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.timiipni = EmbeddingStrategy.re

theorem Phenomena.Complementation.Studies.Deal2026.qeciyeewyew_strategy : nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.qeciyeewyew = EmbeddingStrategy.re

theorem Phenomena.Complementation.Studies.Deal2026.neki_strategy : nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.neki = EmbeddingStrategy.simplex

theorem Phenomena.Complementation.Studies.Deal2026.hi_strategy : nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.hi = EmbeddingStrategy.simplex

theorem Phenomena.Complementation.Studies.Deal2026.cuukwe_strategy : nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.cuukwe = EmbeddingStrategy.simplex

theorem Phenomena.Complementation.Studies.Deal2026.liloy_selProfile : dealSelectionalProfile Fragments.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 Phenomena.Complementation.Studies.Deal2026.neki_selProfile : dealSelectionalProfile Fragments.NezPerce.ClausalEmbedding.neki = { outerCat := Minimalist.Cat.C, requiresInternalAbar := false }

theorem Phenomena.Complementation.Studies.Deal2026.reCanonical_strategy (v : Fragments.NezPerce.ClausalEmbedding.NezPerceEmbedder) : v ∈ Fragments.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 @cite{tonhauser-beaver-roberts-simons-2013} taxonomy

The Tonhauser et al. classes are formalised in Phenomena/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 Phenomena.Complementation.Studies.Deal2026.derivedProjectiveClass (v : Fragments.NezPerce.ClausalEmbedding.NezPerceEmbedder) : Option 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

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

theorem Phenomena.Complementation.Studies.Deal2026.reCanonical_projects_classC : (Fragments.NezPerce.ClausalEmbedding.reCanonical.all fun (v : Fragments.NezPerce.ClausalEmbedding.NezPerceEmbedder) => decide (derivedProjectiveClass v = some 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 @cite{tonhauser-beaver-roberts-simons-2013} taxonomy.

theorem Phenomena.Complementation.Studies.Deal2026.cuukwe_projects_classC : derivedProjectiveClass Fragments.NezPerce.ClausalEmbedding.cuukwe = some 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 Phenomena.Complementation.Studies.Deal2026.neki_no_projection : derivedProjectiveClass Fragments.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 (Phenomena/Presupposition/)
• Deal-internal: EmbeddingStrategy + NotionalComplementShape
• Typology: ComplementClauseStructure surface enum

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

def Phenomena.Complementation.Studies.Deal2026.EmbeddingStrategy.shape : EmbeddingStrategy → NotionalComplementShape

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

Equations

• Phenomena.Complementation.Studies.Deal2026.EmbeddingStrategy.re.shape = Phenomena.Complementation.Studies.Deal2026.nezPerceREShape
• Phenomena.Complementation.Studies.Deal2026.EmbeddingStrategy.simplex.shape = Phenomena.Complementation.Studies.Deal2026.nezPerceSimplexShape

theorem Phenomena.Complementation.Studies.Deal2026.strategy_shape_surface (v : Fragments.NezPerce.ClausalEmbedding.NezPerceEmbedder) : (nezPerceEmbedStrategy v).shape.surfacePattern = if nezPerceEmbedStrategy v = EmbeddingStrategy.re then Typology.Complementation.ComplementClauseStructure.abarInternalCP else Typology.Complementation.ComplementClauseStructure.barePropositionalCP

Strategy-shape correspondence: every embedder's strategy projects to the right shape, preserving the abarInternalCP / barePropositionalCP distinction at the surface-pattern level.

theorem Phenomena.Complementation.Studies.Deal2026.reCanonical_surfacePattern_abar (v : Fragments.NezPerce.ClausalEmbedding.NezPerceEmbedder) : v ∈ Fragments.NezPerce.ClausalEmbedding.reCanonical → (nezPerceEmbedStrategy v).shape.surfacePattern = Typology.Complementation.ComplementClauseStructure.abarInternalCP

Every RE-canonical predicate projects via shape to abarInternalCP.

theorem Phenomena.Complementation.Studies.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 Phenomena.Complementation.Studies.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 Phenomena.Complementation.Studies.Deal2026.table79_bipartite (c : Table79Cell) : c ∈ table79 → c.shape.hasInternalAbar = true ∨ c.shape.hasInternalAbar = false

Table-79 cells partition into ±Ā: every cell either has it or lacks it (a tautology over Bool, but documents the bipartition exhaustiveness of the hasInternalAbar dimension).

theorem Phenomena.Complementation.Studies.Deal2026.cross_classification_populated : (Fragments.NezPerce.ClausalEmbedding.liloy.factive = true ∧ nezPerceREShape.hasInternalAbar = true) ∧ (Fragments.NezPerce.ClausalEmbedding.cuukwe.factive = true ∧ nezPerceSimplexShape.hasInternalAbar = false) ∧ adygheREShape.hasInternalAbar = true ∧ Fragments.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 @cite{caponigro-polinsky-2011}'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 Phenomena.Complementation.Studies.Deal2026.tonhauser_fails_to_distinguish_cuukwe_liloy : derivedProjectiveClass Fragments.NezPerce.ClausalEmbedding.cuukwe = derivedProjectiveClass Fragments.NezPerce.ClausalEmbedding.liloy

Tonhauser projective class does not distinguish cuukwe from liloy.

theorem Phenomena.Complementation.Studies.Deal2026.strategy_distinguishes_cuukwe_liloy : nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.cuukwe ≠ nezPerceEmbedStrategy Fragments.NezPerce.ClausalEmbedding.liloy

But the embedding-strategy projection DOES distinguish them.

ke as a φ-probe on C (@cite{deal-2015a-nels})

@cite{deal-2026} §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 @cite{deal-2015a-nels} 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 @cite{deal-2024}'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 Phenomena.Complementation.Studies.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 Phenomena.Complementation.Studies.Deal2026.ke_satisfied_by_phi : keSatisfaction.isSatisfied [Minimalist.GramFeature.valued (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person Features.Prominence.PersonLevel.first))] none = true

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

theorem Phenomena.Complementation.Studies.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 Phenomena.Complementation.Studies.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 (@cite{deal-2026} §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 Phenomena.Complementation.Studies.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

• Phenomena.Complementation.Studies.Deal2026.reInternalAbar = Minimalist.keineĀDep

theorem Phenomena.Complementation.Studies.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

Theories/Syntax/HPSG/Core/RelativeClauses.lean:87-93 hard-codes RC = modifier (isMod = true, theorem relClause_is_modifier). @cite{deal-2026}'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

Phenomena/Complementation/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 @cite{deal-2026}'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

@cite{caponigro-polinsky-2011}'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

@cite{deal-2026} §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 @cite{deal-2020}'s A Theory of Indexical Shift book; that substrate is not yet implemented in linglib (no Theories/Semantics/IndexicalShift/ directory exists; existing Theories/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.