Adjective

The syntactic core of the adjective as a grammatical object, modeled on Syntax/Pronoun/: surface form, the scalar dimension key it measures + the lexicalized pole, comparison morphology, and lexical antonymy. The dimension is carried as a key (cf. Pronoun importing Person/Number), not interpreted here.

Gradability is not a type split — it is the derived predicate IsGradable (dimension.isSome); a non-gradable adjective (wooden, former, medical) is the same type with dimension = none.

The degree-semantic layer lives one layer up, in Semantics/Gradability, where the scale's boundedness, positive standard, and Kennedy class become relevant: the GradableAdjective refinement there extends Adjective with the standardOverride and derives scaleType/standard/adjectiveClass from the (shape, pole, override). This file deliberately does not depend on the Degree/Kennedy semantics.

Deferred (earn their consumers, cf. Pronoun's deferred capability tower)

• Agreement φ-features + toWord realization — added when an agreeing-language fragment sets them (φ with no setter would be dead fields).
• Dixon PCClass view (Dimension.pcClass) — waits on a lightweight PCClass home (it currently sits in the heavy Morphology/RootTypology.lean).
• The Modifier/Gradable capability classes — built at the second-carrier trigger (an Adverb/degree-word struct), exactly as Pronoun deferred Proform.

This is the adjectival realization of a property concept; when a verb- or noun-strategy fragment lands, factor a PropertyConcept superclass.

Comparison morphology

inductive Adjective.ComparisonStrategy : Type

How a comparative/superlative grade is formed.

• synthetic : ComparisonStrategy
• periphrastic : ComparisonStrategy
• suppletive : ComparisonStrategy

@[implicit_reducible]

instance Adjective.instDecidableEqComparisonStrategy : DecidableEq ComparisonStrategy

Equations

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

def Adjective.instReprComparisonStrategy.repr : ComparisonStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Adjective.instReprComparisonStrategy : Repr ComparisonStrategy

Equations

• Adjective.instReprComparisonStrategy = { reprPrec := Adjective.instReprComparisonStrategy.repr }

@[implicit_reducible]

instance Adjective.instBEqComparisonStrategy : BEq ComparisonStrategy

Equations

• Adjective.instBEqComparisonStrategy = { beq := Adjective.instBEqComparisonStrategy.beq }

def Adjective.instBEqComparisonStrategy.beq : ComparisonStrategy → ComparisonStrategy → Bool

Equations

• Adjective.instBEqComparisonStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Adjective.ComparisonFacet : Type

Grade-level comparison morphology: the cross-linguistic structure (per-grade formation strategy + the suppletion pattern, whose *ABA constraint lives in Morphology/DegreeContainment, [Bob12]) plus the surface comparative and superlative forms.

• formComp : Option String
• formSuper : Option String
• comparativeStrategy : ComparisonStrategy
• superlativeStrategy : ComparisonStrategy
• suppletion : Morphology.DegreeContainment.DegreePattern
• equative : Option ComparisonStrategy

  Equative strategy, if the language marks it morphologically (not under the comparative/superlative containment).

@[implicit_reducible]

instance Adjective.instDecidableEqComparisonFacet : DecidableEq ComparisonFacet

Equations

• Adjective.instDecidableEqComparisonFacet = Adjective.instDecidableEqComparisonFacet.decEq

def Adjective.instDecidableEqComparisonFacet.decEq (x✝ x✝¹ : ComparisonFacet) : Decidable (x✝ = x✝¹)

Equations

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

def Adjective.instReprComparisonFacet.repr : ComparisonFacet → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Adjective.instReprComparisonFacet : Repr ComparisonFacet

Equations

• Adjective.instReprComparisonFacet = { reprPrec := Adjective.instReprComparisonFacet.repr }

def Adjective.instBEqComparisonFacet.beq : ComparisonFacet → ComparisonFacet → Bool

Equations

• One or more equations did not get rendered due to their size.
• Adjective.instBEqComparisonFacet.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Adjective.instBEqComparisonFacet : BEq ComparisonFacet

Equations

• Adjective.instBEqComparisonFacet = { beq := Adjective.instBEqComparisonFacet.beq }

def Adjective.ComparisonFacet.regular : ComparisonFacet

No comparison marking (the default).

Equations

• Adjective.ComparisonFacet.regular = { }

The adjective object

structure Adjective : Type

The adjective lexeme: the syntactic core every adjective shares — surface form, the scalar dimension key + lexicalized pole, comparison morphology, and lexical antonymy. Carries no denotation of its own (cf. Pronoun); the degree-semantic interpretation of dimension/pole is derived one layer up, on GradableAdjective in Semantics/Gradability.

Gradability is not a type split: it is the derived predicate IsGradable (dimension.isSome); a non-gradable adjective is the same type with dimension = none. Coexists with namespace Adjective (a type and a namespace may share a name).

• form : String

  Surface form (citation/positive-grade).

• script : Option String

  Native script form, when distinct.

• dimension : Option Semantics.Gradability.Dimension

  The scalar dimension measured, as a Semantics.Gradability.Dimension key. none for classifying/relational adjectives (wooden, former, medical) and other non-gradables.

• isLowerEndpoint : Bool

  Which pole of the scale the adjective lexicalizes (short, empty, wet): the only thing distinguishing polar scale-mates that share one dimension.

• comparison : ComparisonFacet

  Comparative/superlative morphology.

• antonymForm : Option String

  Lexical antonym's surface form, when it has a stable one.

def instReprAdjective.repr : Adjective → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprAdjective : Repr Adjective

Equations

• instReprAdjective = { reprPrec := instReprAdjective.repr }

def instDecidableEqAdjective.decEq (x✝ x✝¹ : Adjective) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqAdjective : DecidableEq Adjective

Equations

• instDecidableEqAdjective = instDecidableEqAdjective.decEq

@[implicit_reducible]

instance instBEqAdjective : BEq Adjective

Equations

• instBEqAdjective = { beq := instBEqAdjective.beq }

def instBEqAdjective.beq : Adjective → Adjective → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqAdjective.beq x✝¹ x✝ = false

def Adjective.IsGradable (a : Adjective) : Prop

Gradable iff it carries a scalar dimension — derived (cf. Pronoun.category).

Equations

• a.IsGradable = (a.dimension.isSome = true)

@[implicit_reducible]

instance Adjective.instDecidableIsGradable (a : Adjective) : Decidable a.IsGradable

Equations

• a.instDecidableIsGradable = id inferInstance

def Adjective.suppletion (a : Adjective) : Morphology.DegreeContainment.DegreePattern

The suppletion pattern of the comparison paradigm — a convenience read of comparison.suppletion (the field consumers most often want).

Equations

• a.suppletion = a.comparison.suppletion