Stassen 1985: Comparison and Universal Grammar

@cite{stassen-1985}

Stassen's central claim is that the typology of comparative constructions is determined by the typology of temporal chaining constructions. Comparatives are not autonomous constructions but are "modelled upon" or "borrowed from" temporal chains (p. 105). The link runs through a diachronic pathway: "X is tall; Y is not tall" → "X is taller than Y".

Stassen 1985's six-way typology vs WALS 2013's five-way

The 1985 book (110-language sample) classifies comparatives into six types: separative, allative, locative (the three adverbial subtypes collectively making up the "locational" category in WALS 2013), plus exceed, conjoined, and particle. The WALS 2013 typology (@cite{stassen-2013}, in the substrate Linglib/Typology/Comparison.lean) collapses the spatial triad into single locational, dropping the spatial- relation distinction that drives Stassen's explanatory universals connecting comparison to temporal chaining.

This file holds the 1985-specific apparatus: the six-way ComparativeType1985 inductive, the case-assignment + fixed-encoding + spatial-case projections, per-language 1985 type assignments, and the universal verifications.

Chaining strategies (Ch 4)

Languages encode temporal chains using one of two basic strategies (§4.3.1, p. 76):

• Balancing: both predicates retain the same structural rank.
• Deranking: one predicate is structurally reduced.

Deranking subdivides into conditional (only same-subject chains) and absolute (regardless of subject identity).

The Principle of Parallel Chaining (p. 99): a language selects parallel options for consecutive and simultaneous chains.

The seven chaining-based universals (§5.2, pp. 106-108)

Universal	Comparative type	→ Chaining type
1A	derived-case	balancing
1B	fixed-case	deranking
2A	exceed	conditional deranking
2B	adverbial (sep/all/loc)	absolute deranking
3A	separative	abs. deranked anterior consecutive
3B	allative	abs. deranked posterior consecutive
3C	locative	abs. deranked simultaneous
4	conjoined	balanced simultaneous

Particle comparatives are modelled on balanced chains (either simultaneous or consecutive), confirming Universal 1A (p. 108).

inductive Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985 : Type

The six comparative construction types of @cite{stassen-1985} Ch 2.

Finer than the WALS 2013 types (Typology.Comparison.ComparativeType): the three adverbial subtypes (separative, allative, locative) are collapsed into a single "locational" category in WALS. The six types form a hierarchy based on case assignment and syntactic encoding:

                    Comparative
                   /            \
            Derived case    Fixed case
           /        \       /        \
      Conjoined  Particle  Exceed  Adverbial
                                  /    |    \
                               Sep   All   Loc

• separative : ComparativeType1985
• allative : ComparativeType1985
• locative : ComparativeType1985
• exceed : ComparativeType1985
• conjoined : ComparativeType1985
• particle : ComparativeType1985

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instDecidableEqComparativeType1985 : DecidableEq ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.instDecidableEqComparativeType1985 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instBEqComparativeType1985 : BEq ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.instBEqComparativeType1985 = { beq := Phenomena.Comparison.Studies.Stassen1985.instBEqComparativeType1985.beq }

def Phenomena.Comparison.Studies.Stassen1985.instBEqComparativeType1985.beq : ComparativeType1985 → ComparativeType1985 → Bool

Equations

• Phenomena.Comparison.Studies.Stassen1985.instBEqComparativeType1985.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Comparison.Studies.Stassen1985.instReprComparativeType1985.repr : ComparativeType1985 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instReprComparativeType1985 : Repr ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.instReprComparativeType1985 = { reprPrec := Phenomena.Comparison.Studies.Stassen1985.instReprComparativeType1985.repr }

def Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.toWALS : ComparativeType1985 → Typology.Comparison.ComparativeType

Map @cite{stassen-1985} types to the coarser WALS 2013 types (Typology.Comparison.ComparativeType).

Equations

• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative.toWALS = Typology.Comparison.ComparativeType.locational
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.allative.toWALS = Typology.Comparison.ComparativeType.locational
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.locative.toWALS = Typology.Comparison.ComparativeType.locational
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.exceed.toWALS = Typology.Comparison.ComparativeType.exceed
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.conjoined.toWALS = Typology.Comparison.ComparativeType.conjoined
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle.toWALS = Typology.Comparison.ComparativeType.particle

def Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.caseAssignment : ComparativeType1985 → Core.CaseAssignment

Case assignment for each 1985 type.

Equations

• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.conjoined.caseAssignment = Core.CaseAssignment.derived
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle.caseAssignment = Core.CaseAssignment.derived
• x✝.caseAssignment = Core.CaseAssignment.fixed

def Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.fixedEncoding : ComparativeType1985 → Option Core.FixedCaseEncoding

Fixed-case encoding (only meaningful for fixed-case types).

Equations

• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.exceed.fixedEncoding = some Core.FixedCaseEncoding.directObject
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative.fixedEncoding = some Core.FixedCaseEncoding.adverbial
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.allative.fixedEncoding = some Core.FixedCaseEncoding.adverbial
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.locative.fixedEncoding = some Core.FixedCaseEncoding.adverbial
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.conjoined.fixedEncoding = none
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle.fixedEncoding = none

def Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.spatialCase : ComparativeType1985 → Option Core.Case

Spatial case of the standard marker (only meaningful for adverbial types).

Equations

• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative.spatialCase = some UD.Case.abl
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.allative.spatialCase = some UD.Case.all
• Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.locative.spatialCase = some UD.Case.loc
• x✝.spatialCase = none

inductive Phenomena.Comparison.Studies.Stassen1985.ChainingStrategy : Type

Basic structural strategy for encoding temporal chains (§4.3.1, p. 76).

• balancing : ChainingStrategy
• deranking : ChainingStrategy

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instDecidableEqChainingStrategy : DecidableEq ChainingStrategy

Equations

• Phenomena.Comparison.Studies.Stassen1985.instDecidableEqChainingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Comparison.Studies.Stassen1985.instReprChainingStrategy.repr : ChainingStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instReprChainingStrategy : Repr ChainingStrategy

Equations

• Phenomena.Comparison.Studies.Stassen1985.instReprChainingStrategy = { reprPrec := Phenomena.Comparison.Studies.Stassen1985.instReprChainingStrategy.repr }

inductive Phenomena.Comparison.Studies.Stassen1985.DerankedConditionality : Type

For deranking languages: same-subject restriction or unconditional.

• conditional : DerankedConditionality
• absolute : DerankedConditionality

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instDecidableEqDerankedConditionality : DecidableEq DerankedConditionality

Equations

• Phenomena.Comparison.Studies.Stassen1985.instDecidableEqDerankedConditionality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Comparison.Studies.Stassen1985.instReprDerankedConditionality.repr : DerankedConditionality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instReprDerankedConditionality : Repr DerankedConditionality

Equations

• Phenomena.Comparison.Studies.Stassen1985.instReprDerankedConditionality = { reprPrec := Phenomena.Comparison.Studies.Stassen1985.instReprDerankedConditionality.repr }

inductive Phenomena.Comparison.Studies.Stassen1985.DerankedDirection : Type

For absolutely deranked consecutive chains: which predicate is deranked.

• anterior : DerankedDirection
• posterior : DerankedDirection

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instDecidableEqDerankedDirection : DecidableEq DerankedDirection

Equations

• Phenomena.Comparison.Studies.Stassen1985.instDecidableEqDerankedDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Comparison.Studies.Stassen1985.instReprDerankedDirection.repr : DerankedDirection → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instReprDerankedDirection : Repr DerankedDirection

Equations

• Phenomena.Comparison.Studies.Stassen1985.instReprDerankedDirection = { reprPrec := Phenomena.Comparison.Studies.Stassen1985.instReprDerankedDirection.repr }

inductive Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType : Type

Stassen's language type in temporal chaining (§4.7, pp. 98-101).

• balancing : ChainingLanguageType
• conditionalDeranking : ChainingLanguageType
• absoluteDeranking : ChainingLanguageType

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instDecidableEqChainingLanguageType : DecidableEq ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.instDecidableEqChainingLanguageType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Comparison.Studies.Stassen1985.instReprChainingLanguageType.repr : ChainingLanguageType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Comparison.Studies.Stassen1985.instReprChainingLanguageType : Repr ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.instReprChainingLanguageType = { reprPrec := Phenomena.Comparison.Studies.Stassen1985.instReprChainingLanguageType.repr }

def Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.strategy : ChainingLanguageType → ChainingStrategy

The chaining strategy for a language type.

Equations

• Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.balancing.strategy = Phenomena.Comparison.Studies.Stassen1985.ChainingStrategy.balancing
• Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.conditionalDeranking.strategy = Phenomena.Comparison.Studies.Stassen1985.ChainingStrategy.deranking
• Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.absoluteDeranking.strategy = Phenomena.Comparison.Studies.Stassen1985.ChainingStrategy.deranking

def Phenomena.Comparison.Studies.Stassen1985.japanese1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.japanese1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative

def Phenomena.Comparison.Studies.Stassen1985.korean1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.korean1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative

def Phenomena.Comparison.Studies.Stassen1985.turkish1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.turkish1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative

def Phenomena.Comparison.Studies.Stassen1985.hindiUrdu1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.hindiUrdu1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative

def Phenomena.Comparison.Studies.Stassen1985.arabic1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.arabic1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.separative

def Phenomena.Comparison.Studies.Stassen1985.navajo1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.navajo1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.locative

def Phenomena.Comparison.Studies.Stassen1985.mandarin1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.mandarin1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.exceed

def Phenomena.Comparison.Studies.Stassen1985.yoruba1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.yoruba1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.exceed

def Phenomena.Comparison.Studies.Stassen1985.swahili1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.swahili1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.exceed

def Phenomena.Comparison.Studies.Stassen1985.thai1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.thai1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.exceed

def Phenomena.Comparison.Studies.Stassen1985.english1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.english1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle

def Phenomena.Comparison.Studies.Stassen1985.russian1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.russian1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle

def Phenomena.Comparison.Studies.Stassen1985.finnish1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.finnish1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle

def Phenomena.Comparison.Studies.Stassen1985.latin1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.latin1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle

def Phenomena.Comparison.Studies.Stassen1985.french1985 : ComparativeType1985

Equations

• Phenomena.Comparison.Studies.Stassen1985.french1985 = Phenomena.Comparison.Studies.Stassen1985.ComparativeType1985.particle

def Phenomena.Comparison.Studies.Stassen1985.japaneseCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.japaneseCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.absoluteDeranking

def Phenomena.Comparison.Studies.Stassen1985.koreanCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.koreanCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.absoluteDeranking

def Phenomena.Comparison.Studies.Stassen1985.turkishCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.turkishCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.absoluteDeranking

def Phenomena.Comparison.Studies.Stassen1985.hindiUrduCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.hindiUrduCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.absoluteDeranking

def Phenomena.Comparison.Studies.Stassen1985.arabicCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.arabicCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.absoluteDeranking

def Phenomena.Comparison.Studies.Stassen1985.mandarinCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.mandarinCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.conditionalDeranking

def Phenomena.Comparison.Studies.Stassen1985.yorubaCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.yorubaCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.conditionalDeranking

def Phenomena.Comparison.Studies.Stassen1985.swahiliCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.swahiliCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.conditionalDeranking

def Phenomena.Comparison.Studies.Stassen1985.thaiCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.thaiCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.conditionalDeranking

def Phenomena.Comparison.Studies.Stassen1985.englishCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.englishCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.balancing

def Phenomena.Comparison.Studies.Stassen1985.russianCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.russianCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.balancing

def Phenomena.Comparison.Studies.Stassen1985.finnishCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.finnishCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.balancing

def Phenomena.Comparison.Studies.Stassen1985.latinCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.latinCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.balancing

def Phenomena.Comparison.Studies.Stassen1985.frenchCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.frenchCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.balancing

def Phenomena.Comparison.Studies.Stassen1985.navajoCT : ChainingLanguageType

Equations

• Phenomena.Comparison.Studies.Stassen1985.navajoCT = Phenomena.Comparison.Studies.Stassen1985.ChainingLanguageType.balancing

def Phenomena.Comparison.Studies.Stassen1985.universal1A (compType : ComparativeType1985) (ct : ChainingLanguageType) : Prop

Universal 1A: derived-case comparative implies balancing chaining.

Equations

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

def Phenomena.Comparison.Studies.Stassen1985.universal1B (compType : ComparativeType1985) (ct : ChainingLanguageType) : Prop

Universal 1B: fixed-case comparative implies deranking.

Equations

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

def Phenomena.Comparison.Studies.Stassen1985.universal2A (compType : ComparativeType1985) (ct : ChainingLanguageType) : Prop

Universal 2A: exceed comparative implies conditional deranking.

Equations

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

def Phenomena.Comparison.Studies.Stassen1985.universal2B (compType : ComparativeType1985) (ct : ChainingLanguageType) : Prop

Universal 2B: adverbial comparative implies absolute deranking.

Equations

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

theorem Phenomena.Comparison.Studies.Stassen1985.u1a_english : universal1A english1985 englishCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1a_russian : universal1A russian1985 russianCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1a_french : universal1A french1985 frenchCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1a_navajo : universal1A navajo1985 navajoCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_japanese : universal1B japanese1985 japaneseCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_korean : universal1B korean1985 koreanCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_turkish : universal1B turkish1985 turkishCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_hindiUrdu : universal1B hindiUrdu1985 hindiUrduCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_arabic : universal1B arabic1985 arabicCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_mandarin : universal1B mandarin1985 mandarinCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_yoruba : universal1B yoruba1985 yorubaCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_swahili : universal1B swahili1985 swahiliCT

theorem Phenomena.Comparison.Studies.Stassen1985.u1b_thai : universal1B thai1985 thaiCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2a_mandarin : universal2A mandarin1985 mandarinCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2a_yoruba : universal2A yoruba1985 yorubaCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2a_swahili : universal2A swahili1985 swahiliCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2a_thai : universal2A thai1985 thaiCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2b_japanese : universal2B japanese1985 japaneseCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2b_korean : universal2B korean1985 koreanCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2b_turkish : universal2B turkish1985 turkishCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2b_hindiUrdu : universal2B hindiUrdu1985 hindiUrduCT

theorem Phenomena.Comparison.Studies.Stassen1985.u2b_arabic : universal2B arabic1985 arabicCT

theorem Phenomena.Comparison.Studies.Stassen1985.case_assignment_exhaustive (t : ComparativeType1985) : t.caseAssignment = Core.CaseAssignment.derived ∨ t.caseAssignment = Core.CaseAssignment.fixed

Universal 1A and 1B partition the case-assignment space.

theorem Phenomena.Comparison.Studies.Stassen1985.derived_iff_particle_or_conjoined (t : ComparativeType1985) : t.caseAssignment = Core.CaseAssignment.derived ↔ t = ComparativeType1985.particle ∨ t = ComparativeType1985.conjoined

Particle and conjoined are the only derived-case types.

theorem Phenomena.Comparison.Studies.Stassen1985.adverbial_iff_spatial (t : ComparativeType1985) : t.fixedEncoding = some Core.FixedCaseEncoding.adverbial ↔ t = ComparativeType1985.separative ∨ t = ComparativeType1985.allative ∨ t = ComparativeType1985.locative

Adverbial types are exactly the spatial triad.

theorem Phenomena.Comparison.Studies.Stassen1985.adverbial_collapse : ComparativeType1985.separative.toWALS = Typology.Comparison.ComparativeType.locational ∧ ComparativeType1985.allative.toWALS = Typology.Comparison.ComparativeType.locational ∧ ComparativeType1985.locative.toWALS = Typology.Comparison.ComparativeType.locational

The three adverbial types all collapse to locational under WALS.

theorem Phenomena.Comparison.Studies.Stassen1985.derived_case_not_locational (t : ComparativeType1985) (h : t.caseAssignment = Core.CaseAssignment.derived) : t.toWALS ≠ Typology.Comparison.ComparativeType.locational

Derived-case types never map to locational.

theorem Phenomena.Comparison.Studies.Stassen1985.fixed_case_not_particle (t : ComparativeType1985) (h : t.caseAssignment = Core.CaseAssignment.fixed) : t.toWALS ≠ Typology.Comparison.ComparativeType.particle

Fixed-case types never map to particle.

theorem Phenomena.Comparison.Studies.Stassen1985.adverbial_is_fixed (t : ComparativeType1985) (h : t.fixedEncoding = some Core.FixedCaseEncoding.adverbial) : t.caseAssignment = Core.CaseAssignment.fixed

Every adverbial type is fixed-case (by construction).

theorem Phenomena.Comparison.Studies.Stassen1985.separative_uses_ablative : ComparativeType1985.separative.spatialCase = some UD.Case.abl

theorem Phenomena.Comparison.Studies.Stassen1985.allative_uses_allative : ComparativeType1985.allative.spatialCase = some UD.Case.all

theorem Phenomena.Comparison.Studies.Stassen1985.locative_uses_locative : ComparativeType1985.locative.spatialCase = some UD.Case.loc

theorem Phenomena.Comparison.Studies.Stassen1985.exceed_no_spatial : ComparativeType1985.exceed.spatialCase = none

theorem Phenomena.Comparison.Studies.Stassen1985.conjoined_no_spatial : ComparativeType1985.conjoined.spatialCase = none

theorem Phenomena.Comparison.Studies.Stassen1985.particle_no_spatial : ComparativeType1985.particle.spatialCase = none

theorem Phenomena.Comparison.Studies.Stassen1985.japanese_fragment_case : some Fragments.Japanese.Comparison.entry.standardCase = japanese1985.spatialCase

Japanese Fragment standard case matches 1985 spatial case prediction.

theorem Phenomena.Comparison.Studies.Stassen1985.korean_fragment_case : some Fragments.Korean.Comparison.entry.standardCase = korean1985.spatialCase

Korean Fragment standard case matches 1985 spatial case prediction.

theorem Phenomena.Comparison.Studies.Stassen1985.turkish_fragment_case : some Fragments.Turkish.Comparison.entry.standardCase = turkish1985.spatialCase

Turkish Fragment standard case matches 1985 spatial case prediction.

theorem Phenomena.Comparison.Studies.Stassen1985.japanese_marker_match : Fragments.Japanese.Comparison.entry.standardMarker = Fragments.Japanese.Comparison.comparison.standardMarker

Japanese Fragment standard marker matches the Fragment profile.

theorem Phenomena.Comparison.Studies.Stassen1985.korean_marker_match : Fragments.Korean.Comparison.entry.standardMarker = Fragments.Korean.Comparison.comparison.standardMarker

Korean Fragment standard marker matches the Fragment profile.

theorem Phenomena.Comparison.Studies.Stassen1985.turkish_marker_match : Fragments.Turkish.Comparison.entry.standardMarker = Fragments.Turkish.Comparison.comparison.standardMarker

Turkish Fragment standard marker matches the Fragment profile.

theorem Phenomena.Comparison.Studies.Stassen1985.all_separative_fixed_case : Fragments.Japanese.Comparison.entry.caseAssignment = Core.CaseAssignment.fixed ∧ Fragments.Korean.Comparison.entry.caseAssignment = Core.CaseAssignment.fixed ∧ Fragments.Turkish.Comparison.entry.caseAssignment = Core.CaseAssignment.fixed

All three separative Fragment entries use fixed case assignment.

theorem Phenomena.Comparison.Studies.Stassen1985.all_separative_adverbial : Fragments.Japanese.Comparison.entry.fixedEncoding = some Core.FixedCaseEncoding.adverbial ∧ Fragments.Korean.Comparison.entry.fixedEncoding = some Core.FixedCaseEncoding.adverbial ∧ Fragments.Turkish.Comparison.entry.fixedEncoding = some Core.FixedCaseEncoding.adverbial

All three separative Fragment entries use adverbial encoding.

theorem Phenomena.Comparison.Studies.Stassen1985.separative_no_degree_morphology : Fragments.Japanese.Comparison.entry.hasDegreeMorphology = false ∧ Fragments.Korean.Comparison.entry.hasDegreeMorphology = false ∧ Fragments.Turkish.Comparison.entry.hasDegreeMorphology = false

Separative languages lack degree morphology (p. 28).

theorem Phenomena.Comparison.Studies.Stassen1985.japanese_three_layer : some Fragments.Japanese.Comparison.entry.standardCase = japanese1985.spatialCase ∧ japanese1985.toWALS = Fragments.Japanese.Comparison.comparison.comparativeType ∧ japaneseCT = ChainingLanguageType.absoluteDeranking ∧ universal2B japanese1985 japaneseCT

Japanese: Fragment (ablative) ↔ 1985 type (separative) ↔ chaining type (absolute deranking). All three layers agree.

theorem Phenomena.Comparison.Studies.Stassen1985.korean_three_layer : some Fragments.Korean.Comparison.entry.standardCase = korean1985.spatialCase ∧ korean1985.toWALS = Fragments.Korean.Comparison.comparison.comparativeType ∧ koreanCT = ChainingLanguageType.absoluteDeranking ∧ universal2B korean1985 koreanCT

Korean: three-layer consistency.

theorem Phenomena.Comparison.Studies.Stassen1985.turkish_three_layer : some Fragments.Turkish.Comparison.entry.standardCase = turkish1985.spatialCase ∧ turkish1985.toWALS = Fragments.Turkish.Comparison.comparison.comparativeType ∧ turkishCT = ChainingLanguageType.absoluteDeranking ∧ universal2B turkish1985 turkishCT

Turkish: three-layer consistency.

theorem Phenomena.Comparison.Studies.Stassen1985.korean_deranking_consistent : koreanCT = ChainingLanguageType.absoluteDeranking ∧ ClauseChaining.korean.medialVerbForm = UD.VerbForm.Conv

Korean: absolute deranking predicts non-finite medial verbs.

theorem Phenomena.Comparison.Studies.Stassen1985.turkish_deranking_consistent : turkishCT = ChainingLanguageType.absoluteDeranking ∧ ClauseChaining.turkish.medialVerbForm = UD.VerbForm.Conv