Deal (2026): Clausal complementation as relativization, revisited

[Dea26] argues that the relative-like notional complement clauses of Nez Perce ("relative embeddings") are CPs containing an Ā-dependency launched above TP — not DPs or PPs. Clausal complementation is therefore not uniformly relativization ([Kay08], [Kay14], [Ars09]), and factivity, relative-embedding syntax, and nominalization dissociate cross-linguistically ((79)–(81)), though within Nez Perce all relative embeddings are factive. Formalized here: the (79) typology as extended clause spines (Minimalist.ClauseSpine), with shell superstructure, bare-CP status, nominal-shell status, and the selected category all derived from each row's spine; the per-predicate embedding strategy derived from the Fragment's yox̂ ke edge observable; the factivity dissociations; and the case-inflection half of the yox̂-is-D diagnostic. Deal's c-selection point — relative-embedding takers and simplex-takers alike select a CP, the contrast being CP-internal — awaits LI-level Nez Perce entries (Minimalist.SimpleLI selection stacks).

TODO

• ke-agreement ([Dea26] §2, after [Dea15]): the φ-probe on C interacts with all φ-features, probing from the subject downward until [addr] (second person) satisfies it; 1st/2nd but not 3rd person agreement is overt. Needs value-sensitive satisfaction and ordered-goal probing — Minimalist.SatisfactionCond matches feature types only.
• §6 shift/tense: relative embeddings block indexical shift and take matrix-matching tense as temporal de re; simplex embeddings allow shift and relative tense. Rests on [Dea25]'s clause-type semantics (world-set vs perspectival-tuple denotations), not yet implemented.

Embedding strategy from the yox̂ ke edge

The Fragment carries the morphological observable (yoxKeEdge); Deal's analytical classification is derived from it: obligatory yox̂ ke on the complement edge ↔ a syntactic Ā-dependency above TP inside the embedded CP. Both classes c-select a CP — the relative-vs-simplex contrast is internal to the selected clause, not a c-selectional difference.

inductive Deal2026.EmbeddingStrategy : Type

The two embedding strategies [Dea26] distinguishes.

• relative : EmbeddingStrategy
• simplex : EmbeddingStrategy

@[instance_reducible]

instance Deal2026.instDecidableEqEmbeddingStrategy : DecidableEq EmbeddingStrategy

Equations

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

@[instance_reducible]

instance Deal2026.instReprEmbeddingStrategy : Repr EmbeddingStrategy

Equations

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

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

Equations

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

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

Deal's per-predicate embedding-strategy classification, derived from the Fragment observable.

Equations

• Deal2026.nezPerceEmbedStrategy v = if v.yoxKeEdge = NezPerce.Clause.EdgeRequirement.obligatory then Deal2026.EmbeddingStrategy.relative else Deal2026.EmbeddingStrategy.simplex

theorem Deal2026.strategy_iff_yoxKe (v : NezPerce.Clause.NezPerceEmbedder) : nezPerceEmbedStrategy v = EmbeddingStrategy.relative ↔ v.yoxKeEdge = NezPerce.Clause.EdgeRequirement.obligatory

A predicate is relative-canonical in Deal's analysis iff its complement obligatorily carries the yox̂ ke edge morphology.

theorem Deal2026.relativeCanonical_strategy (v : NezPerce.Clause.NezPerceEmbedder) : v ∈ NezPerce.Clause.relativeCanonical → nezPerceEmbedStrategy v = EmbeddingStrategy.relative

theorem Deal2026.simplexCanonical_strategy (v : NezPerce.Clause.NezPerceEmbedder) : v ∈ NezPerce.Clause.simplexCanonical → nezPerceEmbedStrategy v = EmbeddingStrategy.simplex

The cross-linguistic shell typology

[Dea26]'s (79) describes each notional complement by its extended spine — the projected heads from V upward, including any nominal or adpositional superstructure over C. The shell vocabulary is derived: the shells are spine.above .C, bare-CP-hood is highestHead = .C, a nominal shell is a [+N] head above C ([Cho70] features via catFeatures), and the category the matrix predicate selects is the spine's highest head. The internal-Ā axis remains a recorded datum (probe-bearing structure is not yet represented).

structure Deal2026.ShellTypologyCell : Type

A row of [Dea26]'s (79): a language × construction with its extended spine and internal-Ā status.

• language : String
• construction : String
• spine : Minimalist.ClauseSpine

  Projected heads of the notional complement, V up through any CP-external shells.

• hasInternalAbar : Bool

  Whether the embedded CP contains an internal Ā-dependency.

@[instance_reducible]

instance Deal2026.instReprShellTypologyCell : Repr ShellTypologyCell

Equations

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

def Deal2026.instReprShellTypologyCell.repr : ShellTypologyCell → ℕ → Std.Format

Equations

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

def Deal2026.ShellTypologyCell.IsBareCP (c : ShellTypologyCell) : Prop

Nothing projects above C ((79)'s V CP row).

Equations

• c.IsBareCP = (c.spine.highestHead = Minimalist.Cat.C)

@[instance_reducible]

instance Deal2026.instDecidableIsBareCP (c : ShellTypologyCell) : Decidable c.IsBareCP

Equations

• Deal2026.instDecidableIsBareCP c = Deal2026.instDecidableIsBareCP._aux_1 c

def Deal2026.ShellTypologyCell.HasNominalShell (c : ShellTypologyCell) : Prop

The clause complex is wrapped in a nominal projection: some head above C is [+N].

Equations

• c.HasNominalShell = ∃ h ∈ c.spine.above Minimalist.Cat.C, (Minimalist.catFeatures h).plusN = true

@[instance_reducible]

instance Deal2026.instDecidableHasNominalShell (c : ShellTypologyCell) : Decidable c.HasNominalShell

Equations

• Deal2026.instDecidableHasNominalShell c = Deal2026.instDecidableHasNominalShell._aux_1 c

def Deal2026.nezPerceCell (construction : String) (v : NezPerce.Clause.NezPerceEmbedder) : ShellTypologyCell

A Nez Perce row, derived from the Fragment's edge observable: a bare finite CP whose internal Ā-dependency is Deal's interpretation of obligatory yox̂ ke edge morphology.

Equations

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

def Deal2026.nezPerceRelative : ShellTypologyCell

The Nez Perce relative-embedding row ([Dea26] §3, §5).

Equations

• Deal2026.nezPerceRelative = Deal2026.nezPerceCell "relative embedding" NezPerce.Clause.liloy

def Deal2026.nezPerceSimplex : ShellTypologyCell

The Nez Perce simplex row ([Dea26] §6).

Equations

• Deal2026.nezPerceSimplex = Deal2026.nezPerceCell "simplex" NezPerce.Clause.neki

def Deal2026.englishThink : ShellTypologyCell

English simplex V complementation (think): bare CP, no Ā ((79)'s V CP row).

Equations

• Deal2026.englishThink = { language := "English", construction := "think-complement", spine := Minimalist.ClauseSpine.cP, hasInternalAbar := false }

def Deal2026.adygheRelative : ShellTypologyCell

The Adyghe relative-embedding row from [CP11a], exhibited at [Dea26] §4 (43): V D N CP with internal Ā. The Ā-flag is derived from the Fragment observable — 'think' requires the relativizer + high-applicative ze-re- on its tensed complement. Deal cites Caponigro & Polinsky as theoretical kin on the high origin of the operator while diverging on the external shell.

Equations

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

def Deal2026.englishNComplementation : ShellTypologyCell

The English N-complementation row of (79)'s V D N CP / no-Ā cell (the fact that S) — the DP shell with an N co-argument envisioned by [HM21], as Deal notes in §7.

Equations

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

def Deal2026.bulgarianRelative : ShellTypologyCell

The Bulgarian relative-embedding row from [Kra10], exhibited at [Dea26] §4 (49): V P D CP (za over demonstrative tova over the deto-CP; both heads can be null) with internal Ā. The Ā-flag is derived from the Fragment observable — săžaljavam 'regret' takes the deto-complement Krapova analyzes as a hidden relative.

Equations

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

def Deal2026.ndebeleEmbedding : ShellTypologyCell

The Ndebele row, exhibited at [Dea26] §7 (78): V P D CP with no Ā-dependency. [Pie19]'s general claim is a direct DP shell over the CP (class-15 augment = D over kuthi); the P here is the independent preposition nga 'about' of the (78) exhibit (her (20b), khuluma nga), so this row records the attested P-over-DP combination, not the language's only shape.

Equations

• Deal2026.ndebeleEmbedding = { language := "Ndebele", construction := "embedding", spine := Minimalist.ClauseSpine.cP.extend [Minimalist.Cat.D, Minimalist.Cat.P], hasInternalAbar := false }

def Deal2026.washoFactive : ShellTypologyCell

The Washo factive row from [BH21], [HB17]: V D CP, no Ā — not a row of (79); [Dea26] fn. 33 notes the structure as "defended in the literature" for Washo, with no known relative-embedding instance. The D is silent, with the nominalizer -gi ~ -ge spelling out a separate idx head, and no intervening N ('fact'-nouns are unattested in the language); the Fragment observable (Washo.Clause.hamupay.edge = .nominalized) records the nominalization this cell rests on.

Equations

• Deal2026.washoFactive = { language := "Washo", construction := "factive", spine := Minimalist.ClauseSpine.cP.extend [Minimalist.Cat.D], hasInternalAbar := false }

def Deal2026.shellTypology : List ShellTypologyCell

The rows of [Dea26]'s (79) — all six cells of the 3×2 table are filled, with V CP / no-Ā doubly witnessed — plus the Washo V D CP structure from footnote 33.

Equations

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

theorem Deal2026.not_all_rows_abar : ¬∀ c ∈ shellTypology, c.hasInternalAbar = true

Not every row of (79) carries an internal Ā-dependency: the universalist position that all clausal complementation is relativization ([Kay08], [Ars09]) fails on the no-Ā rows (Nez Perce simplex, English think, Ndebele, Washo).

theorem Deal2026.bareCP_abar_dissociates : (∃ c ∈ shellTypology, c.IsBareCP ∧ c.hasInternalAbar = true) ∧ ∃ c ∈ shellTypology, c.IsBareCP ∧ c.hasInternalAbar = false

Bare CPs occur with and without an internal Ā-dependency: relative embeddings are real, and not all complementation is relativization.

theorem Deal2026.shelled_RE_attested : ∃ c ∈ shellTypology, c.HasNominalShell ∧ c.hasInternalAbar = true

relative embeddings vary in nominal superstructure: some carry their Ā-dependency inside a nominal shell (Adyghe V D N CP, Bulgarian V P D CP).

theorem Deal2026.shared_cP_core (c : ShellTypologyCell) : c ∈ shellTypology → Minimalist.ClauseSpine.cP.projectedHeads <+: c.spine.projectedHeads

Every row's spine extends the same finite-CP core: the rows differ only above C.

theorem Deal2026.selected_category_varies : ∃ c₁ ∈ shellTypology, ∃ c₂ ∈ shellTypology, ∃ c₃ ∈ shellTypology, c₁.spine.highestHead = Minimalist.Cat.C ∧ c₂.spine.highestHead = Minimalist.Cat.D ∧ c₃.spine.highestHead = Minimalist.Cat.P

The category the matrix predicate selects — the spine's highest head — nonetheless varies across the rows: C, D, and P are all attested. With shared_cP_core, this derives [Dea26] §7's moral: the internal syntax of a clause does not predict its external syntax.

Factivity and relative-embedding syntax vary independently

[Dea26] (80): factivity and relative-embedding syntax dissociate — cross-linguistically the axes vary "independently to at least some extent", while within Nez Perce the entailment holds one way only (all relative embeddings are factive, relativeCanonical_all_factive; not all factives are relative embeddings). The fourth cell (non-factive + Ā) is Adyghe, where the relative strategy is required for all tensed notional complementation regardless of factivity ([CP11a] §6.5, as Deal reports) — now witnessed from Fragment data (nonfactive_relative_attested). Bulgarian dissociates in the same direction as Nez Perce: Bulgarian.Clause.factivity_not_sufficient_for_deto.

theorem Deal2026.factivity_not_strategy : ¬∀ v ∈ NezPerce.Clause.allEmbedders, v.factive = true ↔ nezPerceEmbedStrategy v = EmbeddingStrategy.relative

Factivity does not coincide with the embedding strategy across the Fragment inventory.

theorem Deal2026.factive_simplex_attested : ∃ v ∈ NezPerce.Clause.allEmbedders, v.factive = true ∧ nezPerceEmbedStrategy v = EmbeddingStrategy.simplex

The dissociating witness: a factive simplex-taker (cuukwe 'know').

theorem Deal2026.factive_relative_attested : ∃ v ∈ NezPerce.Clause.allEmbedders, v.factive = true ∧ nezPerceEmbedStrategy v = EmbeddingStrategy.relative

The co-occurring cell: a factive relative-embedding taker (lilooy 'be happy').

theorem Deal2026.nonfactive_relative_attested : ∃ v ∈ Adyghe.Clause.relativeTakers, v.factive = some false

The fourth cell of (80) — non-factive + Ā — witnessed from Fragment data: Adyghe 'think' is consensus-non-factive and requires ze-re- on its tensed complement ([CP11a] (96) vs (98)).

Projection does not distinguish relative from simplex

Deal's factivity trials assess projection only — "in claiming that RE verbs are factive, what I claim is that their complement clause content is projective" (§3), in the [TBRS13] sense. On that dimension cuukwe and lilooy are indistinguishable; the relative-vs-simplex split lives at the embedding-strategy layer.

theorem Deal2026.projective_cuukwe_eq_liloy : NezPerce.Clause.cuukwe.factive = NezPerce.Clause.liloy.factive

The projection dimension does not distinguish cuukwe from lilooy: both are factive.

theorem Deal2026.strategy_cuukwe_ne_liloy : nezPerceEmbedStrategy NezPerce.Clause.cuukwe ≠ nezPerceEmbedStrategy NezPerce.Clause.liloy

The embedding-strategy layer does distinguish them.

The D-inflection diagnostic

theorem Deal2026.paradigm_case_discriminates (p : NezPerce.Clause.RelativePronoun) : p ∈ NezPerce.Clause.relativePronounParadigm → ∀ q ∈ NezPerce.Clause.relativePronounParadigm, p.case ≠ q.case → ∀ f ∈ p.forms, f ∉ q.forms

The relative pronoun yox̂/ko inflects for case: cells with distinct cases share no forms. This is the case-inflection half of [Dea26] §2's diagnostic ((21)) that yox̂/ko is a D while invariant ke is a C — the D half of the yox̂ ke edge whose obligatoriness yoxKeEdge records.