Agreement profiles — the descriptive fact layer

[Cor98] [Cor06] [Nor19]

Agreement in the wide, descriptive sense of reference grammars ("the adjective agrees in number, gender, and case"): systematic covariance of a target's form with properties of another element ([Cor98] §1's definition). A grammar records, per target category, the feature dimensions in which forms covary; [Nor19]'s 174-language concord survey ranges over exactly the dimensions below (number concord most common, case concord rare and almost never alone).

Which covariances count as agreement in the NARROW, theoretical sense is the contested analytical layer, kept out of this file: [Cor98] §2.4 excludes case and definiteness by the asymmetry criterion (Studies/Corbett1998.lean), while [AZ25d] carry κ through the nominal projection alongside φ (Studies/AlexeyenkoZeijlstra2025.lean). Both analyses consume these facts; neither is baked into them.

Main declarations

• Agreement.Dimension: a feature dimension in which forms may covary
• Agreement.Profile: one language's per-target agreement dimensions

inductive Agreement.Dimension : Type

A feature dimension in which a target's form may covary with another element: [Cor98] §2's indisputable three plus §2.4's contested pair ([Cor06] "less clear" features), the space [Nor19]'s concord survey ranges over. Whether a given dimension's covariance is agreement proper, government, or feature percolation is an analysis, not a fact of this type.

• person : Dimension
• number : Dimension
• gender : Dimension
• case : Dimension
• definiteness : Dimension

@[implicit_reducible]

instance Agreement.instDecidableEqDimension : DecidableEq Dimension

Equations

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

@[implicit_reducible]

instance Agreement.instReprDimension : Repr Dimension

Equations

• Agreement.instReprDimension = { reprPrec := Agreement.instReprDimension.repr }

def Agreement.instReprDimension.repr : Dimension → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Agreement.instReprDimension.repr Agreement.Dimension.person prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.person")).group prec✝
• Agreement.instReprDimension.repr Agreement.Dimension.number prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.number")).group prec✝
• Agreement.instReprDimension.repr Agreement.Dimension.gender prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.gender")).group prec✝
• Agreement.instReprDimension.repr Agreement.Dimension.case prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Agreement.Dimension.case")).group prec✝

@[implicit_reducible]

instance Agreement.instFintypeDimension : Fintype Dimension

Equations

• Agreement.instFintypeDimension = { elems := { val := ↑Agreement.Dimension.enumList, nodup := Agreement.Dimension.enumList_nodup }, complete := Agreement.instFintypeDimension._proof_1 }

@[reducible, inline]

abbrev Agreement.Profile : Type

A language's agreement profile (wide sense): for each target category, the dimensions in which that target's form covaries. ∅ = invariant (bare) forms. Conditioned splits (e.g. Russian verbs: person/number in nonpast, gender/number in past) are unioned, not modeled.

Equations

• Agreement.Profile = (Agreement.Target → Finset Agreement.Dimension)