Complement frames — typed complement positions

A predicate's complement frame as a list of typed Complement.Positions: nominal, adpositional, or clausal, the clausal case carrying the axes the predicate selects for. The flat ComplementType enum survives as a round-trip view (ComplementType.toFrame / Frame.toComplementType).

Main definitions

• Complement.Position — one complement position; a clausal position carries its selectional axes by construction
• Frame + Frame.np, Frame.finiteClause, … — a frame is a list of complement positions; the flat enum cells as smart constructors
• ComplementType + toFrame / Frame.toComplementType — the flat enum and its round-trip view
• ComplementType.toCoding + codings_toFrame — the enum's [Noo07] coding and its agreement with the typed frames

Implementation notes

Complement-taking is cross-categorial ([Noo07]'s CTPs include adjectives and nouns), so the position record lives in the Complement namespace beside Complement.Coding, not under Verb; Adposition.Complement is the P-specific counterpart of the position categories. Frame-conditioned readings (attitude, opacity, control) are not per-position data — they live on Verb.Reading (Syntax/Category/Verb/Defs.lean), keyed to the verb's frames. The selection relation between verb frames and clause-typers (Verb.takes) lives in Syntax/Category/Verb/Complement/Takes.lean. [Dea26]'s CP-external shell inventory lives with its consumer in Studies/Deal2026.lean.

inductive Complement.Position : Type

One complement position of a predicate's frame: nominal, adpositional, or clausal with the axes the predicate selects for — [Noo07] coding, illocutionary force, and subject requirement, none = unselective. Non-clausal positions carry no clausal axes by construction.

• nominal : Position
• adpositional : Position
• clausal (coding : Option Coding := none) (force : Option Mood.Illocutionary := none) (embeddedSubject : Option Clause.EmbeddedSubject := none) : Position

def Complement.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complement.instDecidableEqPosition.decEq Complement.Position.nominal Complement.Position.nominal = isTrue ⋯
• Complement.instDecidableEqPosition.decEq Complement.Position.nominal Complement.Position.adpositional = isFalse Complement.instDecidableEqPosition.decEq._proof_1
• Complement.instDecidableEqPosition.decEq Complement.Position.nominal (Complement.Position.clausal coding force embeddedSubject) = isFalse ⋯
• Complement.instDecidableEqPosition.decEq Complement.Position.adpositional Complement.Position.nominal = isFalse Complement.instDecidableEqPosition.decEq._proof_3
• Complement.instDecidableEqPosition.decEq Complement.Position.adpositional Complement.Position.adpositional = isTrue ⋯
• Complement.instDecidableEqPosition.decEq Complement.Position.adpositional (Complement.Position.clausal coding force embeddedSubject) = isFalse ⋯
• Complement.instDecidableEqPosition.decEq (Complement.Position.clausal coding force embeddedSubject) Complement.Position.nominal = isFalse ⋯
• Complement.instDecidableEqPosition.decEq (Complement.Position.clausal coding force embeddedSubject) Complement.Position.adpositional = isFalse ⋯

@[instance_reducible]

instance Complement.instDecidableEqPosition : DecidableEq Position

Equations

• Complement.instDecidableEqPosition = Complement.instDecidableEqPosition.decEq

def Complement.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Complement.instReprPosition : Repr Position

Equations

• Complement.instReprPosition = { reprPrec := Complement.instReprPosition.repr }

def Complement.Position.coding? : Position → Option Coding

The position's recorded [Noo07] coding, if clausal.

Equations

• (Complement.Position.clausal c force embeddedSubject).coding? = c
• x✝.coding? = none

def Complement.Position.force? : Position → Option Mood.Illocutionary

The position's recorded force, if clausal.

Equations

• (Complement.Position.clausal c force embeddedSubject).force? = force
• x✝.force? = none

def Complement.Position.embeddedSubject? : Position → Option Clause.EmbeddedSubject

The position's recorded subject requirement, if clausal.

Equations

• (Complement.Position.clausal c force embeddedSubject).embeddedSubject? = embeddedSubject
• x✝.embeddedSubject? = none

@[reducible, inline]

abbrev Frame : Type

A complement frame: the predicate's selected complement positions in order. Intransitive = []; double object = two positions. The external argument is not a frame position — it lives on Verb.voiceType.

Equations

• Frame = List Complement.Position

def Frame.codings (fr : Frame) : List Complement.Coding

The [Noo07] codings recorded across the frame's positions.

Equations

• fr.codings = List.filterMap (fun (x : Complement.Position) => x.coding?) fr

def Frame.hasForce (fr : Frame) (f : Mood.Illocutionary) : Prop

Some position of the frame records force f.

Equations

• fr.hasForce f = ∃ p ∈ fr, p.force? = some f

@[instance_reducible]

instance Frame.instDecidableHasForce (fr : Frame) (f : Mood.Illocutionary) : Decidable (fr.hasForce f)

Equations

• fr.instDecidableHasForce f = Frame.instDecidableHasForce._aux_1 fr f

Smart constructors — the flat ComplementType cells

def Frame.np : Frame

Transitive: one nominal position.

Equations

• Frame.np = [Complement.Position.nominal]

def Frame.np_np : Frame

Double object: two nominal positions.

Equations

• Frame.np_np = [Complement.Position.nominal, Complement.Position.nominal]

def Frame.np_pp : Frame

NP + PP: a nominal plus an adpositional position.

Equations

• Frame.np_pp = [Complement.Position.nominal, Complement.Position.adpositional]

def Frame.finiteClause : Frame

Finite declarative clause.

Equations

• Frame.finiteClause = [Complement.Position.clausal (some Complement.Coding.indicative) (some Mood.Illocutionary.declarative)]

def Frame.infinitival : Frame

Infinitival clause. The embedded-subject requirement varies by verb (equi-deletion, raising, or adposition-marked overt subjects, [Noo07] §1.3.4), so it lives on the verb's reading, not here.

Equations

• Frame.infinitival = [Complement.Position.clausal (some Complement.Coding.infinitive)]

def Frame.gerund : Frame

Gerund / nominalized clause.

Equations

• Frame.gerund = [Complement.Position.clausal (some Complement.Coding.nominalized)]

def Frame.smallClause : Frame

Small clause (consider X happy; causative make X leave). Outside [Noo07]'s coding inventory, which classifies complements by the part of speech of their predicate, so the position records nothing.

Equations

• Frame.smallClause = [Complement.Position.clausal]

def Frame.question : Frame

Embedded question. Interrogativity is a force distinction orthogonal to [Noo07] coding, so coding stays none.

Equations

• Frame.question = [Complement.Position.clausal none (some Mood.Illocutionary.interrogative)]

The flat enum view

inductive ComplementType : Type

Complement type that the verb selects — the flat view over the typed Frame.

• Finite: "that" clauses ("John knows that Mary left")
• Infinitival: "to" complements ("John managed to leave")
• Gerund: "-ing" complements ("John stopped smoking")
• NP: Direct object ("John kicked the ball")
• None: Intransitive ("John slept")

• none : ComplementType
• np : ComplementType
• np_np : ComplementType
• np_pp : ComplementType
• finiteClause : ComplementType
• infinitival : ComplementType
• gerund : ComplementType
• smallClause : ComplementType
• question : ComplementType

@[instance_reducible]

instance instDecidableEqComplementType : DecidableEq ComplementType

Equations

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

def instReprComplementType.repr : ComplementType → ℕ → Std.Format

Equations

• instReprComplementType.repr ComplementType.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.none")).group prec✝
• instReprComplementType.repr ComplementType.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.np")).group prec✝
• instReprComplementType.repr ComplementType.np_np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.np_np")).group prec✝
• instReprComplementType.repr ComplementType.np_pp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.np_pp")).group prec✝
• instReprComplementType.repr ComplementType.finiteClause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.finiteClause")).group prec✝
• instReprComplementType.repr ComplementType.infinitival prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.infinitival")).group prec✝
• instReprComplementType.repr ComplementType.gerund prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.gerund")).group prec✝
• instReprComplementType.repr ComplementType.smallClause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.smallClause")).group prec✝
• instReprComplementType.repr ComplementType.question prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ComplementType.question")).group prec✝

@[instance_reducible]

instance instReprComplementType : Repr ComplementType

Equations

• instReprComplementType = { reprPrec := instReprComplementType.repr }

def ComplementType.isFinite : ComplementType → Bool

Is this complement type finite (i.e., does it contain a tense head)?

Finite complements (.finiteClause,.question) have independent tense morphology; non-finite complements (.infinitival,.gerund,.smallClause) do not.

Equations

• ComplementType.finiteClause.isFinite = true
• ComplementType.question.isFinite = true
• x✝.isFinite = false

def ComplementType.isNominal : ComplementType → Bool

Is this complement type a nominal (DP) argument?

Nominal complements project DP: the verb selects a noun phrase in object position. Relevant to c-selection in coordination: a verb that only selects nominal complements cannot independently license a CP conjunct ([Sch26]).

Equations

• ComplementType.np.isNominal = true
• ComplementType.np_np.isNominal = true
• ComplementType.np_pp.isNominal = true
• x✝.isNominal = false

def ComplementType.isClausal : ComplementType → Bool

Is this complement type a clausal (CP) argument?

Clausal complements project CP or reduced clausal structure. This covers finite clauses (dass-clauses), infinitivals, gerunds, small clauses, and embedded questions.

Equations

• ComplementType.finiteClause.isClausal = true
• ComplementType.infinitival.isClausal = true
• ComplementType.gerund.isClausal = true
• ComplementType.smallClause.isClausal = true
• ComplementType.question.isClausal = true
• x✝.isClausal = false

def ComplementType.toFrame : ComplementType → Frame

The Frame cell of a flat ComplementType (.none ↦ []).

Equations

• ComplementType.none.toFrame = []
• ComplementType.np.toFrame = Frame.np
• ComplementType.np_np.toFrame = Frame.np_np
• ComplementType.np_pp.toFrame = Frame.np_pp
• ComplementType.finiteClause.toFrame = Frame.finiteClause
• ComplementType.infinitival.toFrame = Frame.infinitival
• ComplementType.gerund.toFrame = Frame.gerund
• ComplementType.smallClause.toFrame = Frame.smallClause
• ComplementType.question.toFrame = Frame.question

def Frame.toComplementType (fr : Frame) : Option ComplementType

Partial inverse of ComplementType.toFrame: the flat enum cell a frame instantiates, none on frames richer than any cell.

Equations

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

@[simp]

theorem toComplementType_toFrame (ct : ComplementType) : ct.toFrame.toComplementType = some ct

The enum view round-trips over the smart-constructor cells.

theorem ComplementType.toFrame_injective : Function.Injective toFrame

def ComplementType.toCoding : ComplementType → Option Complement.Coding

The [Noo07] coding of a complement frame: none for non-clausal frames, for small clauses (outside the coding inventory), and for embedded questions (interrogativity is a clause-form axis, not a coding).

Equations

• ComplementType.finiteClause.toCoding = some Complement.Coding.indicative
• ComplementType.infinitival.toCoding = some Complement.Coding.infinitive
• ComplementType.gerund.toCoding = some Complement.Coding.nominalized
• ComplementType.smallClause.toCoding = none
• ComplementType.none.toCoding = none
• ComplementType.np.toCoding = none
• ComplementType.np_np.toCoding = none
• ComplementType.np_pp.toCoding = none
• ComplementType.question.toCoding = none

theorem ComplementType.codings_toFrame (ct : ComplementType) : ct.toFrame.codings = ct.toCoding.toList

The enum view and the typed frames record the same coding: a cell's frame carries exactly the codings toCoding assigns it.