Degree Containment — Substrate

@cite{bobaljik-2012}

Framework-neutral substrate for the three-grade degree hierarchy (positive, comparative, superlative) and the *ABA generalization that applies to it. Mirrors the structure of Core.Case.Allomorphy for case morphology: an AllomorphyPattern-style record + decidable contiguity predicates derived from the generic Morphology.Containment substrate.

The empirical generalization @cite{bobaljik-2012} surveys: across languages, suppletion in adjectival comparison patterns as tall– taller–tallest (AAA), good–better–best (ABB), or bonus–melior– optimus (ABC); the configuration *good–better–goodest (ABA) is unattested. This file supplies the pattern type and the *ABA detector. What explains the generalization (Containment Hypothesis + late insertion + Elsewhere ordering) is theory-laden and lives elsewhere — see Theories/Morphology/DM/ContainmentVI.lean for the DM-flavored VI account and Phenomena/Comparison/Studies/Bobaljik2012.lean for the bundle of CSG predictions and attested-pattern theorems.

Scope restriction (cf. @cite{bobaljik-2012} on relative vs. absolute superlatives): the contiguity claim concerns relative superlatives. Absolute / elatival superlatives (e.g., Italian bellissimo) are a distinct morphological category whose internal structure need not contain CMPR.

inductive Core.Morphology.DegreeContainment.DegreeGrade : Type

The three morphological grades of adjectival degree. Structural layers: each higher grade's morphosyntactic representation contains the lower ones.

• pos : DegreeGrade
• cmpr : DegreeGrade
• sprl : DegreeGrade

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instDecidableEqDegreeGrade : DecidableEq DegreeGrade

Equations

• Core.Morphology.DegreeContainment.instDecidableEqDegreeGrade x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.DegreeContainment.instReprDegreeGrade.repr : DegreeGrade → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instReprDegreeGrade : Repr DegreeGrade

Equations

• Core.Morphology.DegreeContainment.instReprDegreeGrade = { reprPrec := Core.Morphology.DegreeContainment.instReprDegreeGrade.repr }

def Core.Morphology.DegreeContainment.DegreeGrade.rank : DegreeGrade → Nat

Containment rank: POS < CMPR < SPRL. The "containment" relation reduces to rank ≤ rank on DegreeGrade; we don't introduce a named containedIn wrapper, since Nat.le_refl and Nat.le_trans already provide the algebraic content.

Equations

• Core.Morphology.DegreeContainment.DegreeGrade.pos.rank = 0
• Core.Morphology.DegreeContainment.DegreeGrade.cmpr.rank = 1
• Core.Morphology.DegreeContainment.DegreeGrade.sprl.rank = 2

def Core.Morphology.DegreeContainment.DegreeGrade.toFin : DegreeGrade → Fin 3

The degree grade as a position index in the 3-cell hierarchy. Sibling of rank for callers that need a Fin 3 directly (e.g. indexing into Theories.Morphology.DM.ContainmentVI's n-parametric machinery at n = 3).

Equations

• Core.Morphology.DegreeContainment.DegreeGrade.pos.toFin = 0
• Core.Morphology.DegreeContainment.DegreeGrade.cmpr.toFin = 1
• Core.Morphology.DegreeContainment.DegreeGrade.sprl.toFin = 2

structure Core.Morphology.DegreeContainment.DegreePattern : Type

A suppletive pattern over the three grades, indexed by form-class. Two grades share a root iff they have the same index.

Examples:

• AAA (0,0,0): tall – taller – tallest
• ABB (0,1,1): good – better – best
• ABC (0,1,2): bonus – melior – optimus
• *ABA (0,1,0): unattested.

• pos : Nat
• cmpr : Nat
• sprl : Nat

def Core.Morphology.DegreeContainment.instDecidableEqDegreePattern.decEq (x✝ x✝¹ : DegreePattern) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instDecidableEqDegreePattern : DecidableEq DegreePattern

Equations

• Core.Morphology.DegreeContainment.instDecidableEqDegreePattern = Core.Morphology.DegreeContainment.instDecidableEqDegreePattern.decEq

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instReprDegreePattern : Repr DegreePattern

Equations

• Core.Morphology.DegreeContainment.instReprDegreePattern = { reprPrec := Core.Morphology.DegreeContainment.instReprDegreePattern.repr }

def Core.Morphology.DegreeContainment.instReprDegreePattern.repr : DegreePattern → Nat → Std.Format

Equations

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

def Core.Morphology.DegreeContainment.DegreePattern.ViolatesABA (p : DegreePattern) : Prop

A pattern violates the *ABA constraint. By construction the case-projection of the generic predicate Morphology.Containment.ViolatesABA.

Equations

• p.ViolatesABA = Morphology.Containment.ViolatesABA [p.pos, p.cmpr, p.sprl]

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instDecidableViolatesABA (p : DegreePattern) : Decidable p.ViolatesABA

Equations

• Core.Morphology.DegreeContainment.instDecidableViolatesABA p = Core.Morphology.DegreeContainment.instDecidableViolatesABA._aux_1 p

def Core.Morphology.DegreeContainment.DegreePattern.IsContiguous (p : DegreePattern) : Prop

A pattern is contiguous: each form class occupies a contiguous span on the hierarchy. Equivalent to ¬ ViolatesABA.

Equations

• p.IsContiguous = ¬p.ViolatesABA

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instDecidableIsContiguous (p : DegreePattern) : Decidable p.IsContiguous

Equations

• Core.Morphology.DegreeContainment.instDecidableIsContiguous p = Core.Morphology.DegreeContainment.instDecidableIsContiguous._aux_1 p

def Core.Morphology.DegreeContainment.DegreePattern.IsRegular (p : DegreePattern) : Prop

All three grades share the same root (regular paradigm).

Equations

• p.IsRegular = (p.pos = p.cmpr ∧ p.cmpr = p.sprl)

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instDecidableIsRegular (p : DegreePattern) : Decidable p.IsRegular

Equations

• Core.Morphology.DegreeContainment.instDecidableIsRegular p = Core.Morphology.DegreeContainment.instDecidableIsRegular._aux_1 p

def Core.Morphology.DegreeContainment.DegreePattern.CmprSuppletive (p : DegreePattern) : Prop

Comparative is suppletive (root differs from positive).

Equations

• p.CmprSuppletive = (p.pos ≠ p.cmpr)

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instDecidableCmprSuppletive (p : DegreePattern) : Decidable p.CmprSuppletive

Equations

• Core.Morphology.DegreeContainment.instDecidableCmprSuppletive p = Core.Morphology.DegreeContainment.instDecidableCmprSuppletive._aux_1 p

def Core.Morphology.DegreeContainment.DegreePattern.SprlSuppletive (p : DegreePattern) : Prop

Superlative is suppletive (root differs from positive).

Equations

• p.SprlSuppletive = (p.pos ≠ p.sprl)

@[implicit_reducible]

instance Core.Morphology.DegreeContainment.instDecidableSprlSuppletive (p : DegreePattern) : Decidable p.SprlSuppletive

Equations

• Core.Morphology.DegreeContainment.instDecidableSprlSuppletive p = Core.Morphology.DegreeContainment.instDecidableSprlSuppletive._aux_1 p

def Core.Morphology.DegreeContainment.aaa : DegreePattern

AAA: regular throughout.

Equations

• Core.Morphology.DegreeContainment.aaa = { pos := 0, cmpr := 0, sprl := 0 }

def Core.Morphology.DegreeContainment.abb : DegreePattern

ABB: suppletive comparative; superlative shares comparative root. English good – better – best.

Equations

• Core.Morphology.DegreeContainment.abb = { pos := 0, cmpr := 1, sprl := 1 }

def Core.Morphology.DegreeContainment.abc : DegreePattern

ABC: three distinct roots. Latin bonus – melior – optimus.

Equations

• Core.Morphology.DegreeContainment.abc = { pos := 0, cmpr := 1, sprl := 2 }

def Core.Morphology.DegreeContainment.aba : DegreePattern

*ABA: the unattested pattern (*good – better – goodest).

Equations

• Core.Morphology.DegreeContainment.aba = { pos := 0, cmpr := 1, sprl := 0 }

def Core.Morphology.DegreeContainment.aab : DegreePattern

*AAB: contiguous by the generic ABA checker, but excluded by VI locality in the DM analysis (see Theories/Morphology/DM/ContainmentVI.lean).

Equations

• Core.Morphology.DegreeContainment.aab = { pos := 0, cmpr := 0, sprl := 1 }

Smoke tests confirming each named pattern resolves correctly. Demoted from theorem to example because nothing in the codebase references them by name.

theorem Core.Morphology.DegreeContainment.csg_part1 (p : DegreePattern) (h_contig : p.IsContiguous) (h_cmpr_suppl : p.CmprSuppletive) : p.SprlSuppletive

Comparative-Superlative Generalization, Part I (@cite{bobaljik-2012}): if the comparative is suppletive, then the superlative is also suppletive (with respect to the positive). Follows from contiguity alone — if POS ≠ CMPR, then a contiguous pattern cannot have POS = SPRL (that would be ABA).

def Core.Morphology.DegreeContainment.patternFromForms (pos cmpr sprl : String) : DegreePattern

Derive a DegreePattern from three surface forms by grouping identical strings. Convention: positive root gets index 0; new roots get fresh indices.

Equations

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

Smoke tests for patternFromForms covering the three attested pattern types.