Clause-token axes

Theory-neutral axes of an embedded clause token, consumed by the complementation and particle APIs.

Main definitions

• Clause.EmbeddedSubject — the subject-requirement axis complement frames record (Syntax/Category/Verb/Complement/Basic.lean)
• Clause.EmbeddingContext — where a clause token occurs, the [BD20] embedding cells

inductive Clause.EmbeddedSubject : Type

Subject requirement of a clause: obligatorily null (as in control complements) or overt, optionally with a fixed case. Genitive marking on the subject is [Noo07]'s criterion for the nominalization coding (§1.3.5); [Bon22] ch. 4 is the modern instance (Buryat genitive subjects of nominalized clauses).

• obligatorilyNull : EmbeddedSubject
• overt (subjCase : Option Case) : EmbeddedSubject

def Clause.instDecidableEqEmbeddedSubject.decEq (x✝ x✝¹ : EmbeddedSubject) : Decidable (x✝ = x✝¹)

Equations

• Clause.instDecidableEqEmbeddedSubject.decEq Clause.EmbeddedSubject.obligatorilyNull Clause.EmbeddedSubject.obligatorilyNull = isTrue ⋯
• Clause.instDecidableEqEmbeddedSubject.decEq Clause.EmbeddedSubject.obligatorilyNull (Clause.EmbeddedSubject.overt subjCase) = isFalse ⋯
• Clause.instDecidableEqEmbeddedSubject.decEq (Clause.EmbeddedSubject.overt subjCase) Clause.EmbeddedSubject.obligatorilyNull = isFalse ⋯
• Clause.instDecidableEqEmbeddedSubject.decEq (Clause.EmbeddedSubject.overt a) (Clause.EmbeddedSubject.overt b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Clause.instDecidableEqEmbeddedSubject : DecidableEq EmbeddedSubject

Equations

• Clause.instDecidableEqEmbeddedSubject = Clause.instDecidableEqEmbeddedSubject.decEq

@[instance_reducible]

instance Clause.instReprEmbeddedSubject : Repr EmbeddedSubject

Equations

• Clause.instReprEmbeddedSubject = { reprPrec := Clause.instReprEmbeddedSubject.repr }

def Clause.instReprEmbeddedSubject.repr : EmbeddedSubject → ℕ → Std.Format

Equations

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

inductive Clause.EmbeddingContext : Type

A [BD20] / [Day25] interrogative-embedding context: where the clause token occurs, not a property of the clause object. A particle's left-periphery layer (Features.QParticleLayer) is derivable from its distribution over these cells (Studies/Dayal2025).

• matrix : EmbeddingContext
• subordinated : EmbeddingContext
• quasiSubordinated : EmbeddingContext

  Embedded root-like interrogatives (Hindi-Urdu kya:).

• quotation : EmbeddingContext

@[instance_reducible]

instance Clause.instDecidableEqEmbeddingContext : DecidableEq EmbeddingContext

Equations

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

@[instance_reducible]

instance Clause.instReprEmbeddingContext : Repr EmbeddingContext

Equations

• Clause.instReprEmbeddingContext = { reprPrec := Clause.instReprEmbeddingContext.repr }

def Clause.instReprEmbeddingContext.repr : EmbeddingContext → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.instFintypeEmbeddingContext : Fintype EmbeddingContext

Equations

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