Case assignment provenance — the neutral source ontology

[Mar91] [Kal18] [Woo06]

Case.Source is the coarsened provenance of an assigned case — the dimension on which the formalized assignment accounts agree that a case "comes from" somewhere. It is not a theory-neutral universal: it is the common quotient that Marantz dependent case (Syntax/Case/Dependent.lean's CaseSource) and Kalin hybrid licensing (Syntax/Case/Licensing.lean's LicensingOutcome) both map into (toNeutral), so a cross-theory comparison can ask whether two accounts agree on provenance, not merely on the surface case. Each account keeps its own finer source enum; Source is where they become commensurable.

Living in Features/ — below the assignment theories — lets both theories project into it (and lets a future pooled comparison name it). The structural-vs-inherent split lives here, on the provenance, not on the inventory cell (Features/Case/Basic.lean): whether a given case, e.g. ergative, is "structural" is a contested claim about its source ([Woo06]), which different accounts answer differently — so it is not a property of the Case value.

inductive Case.Source : Type

The provenance of an assigned case, coarsened across the formalized accounts:

• structural — valued by configuration or Agree (Marantz dependent, Chomskyan agree, Kalin primary/secondary licensing);
• inherent — lexical/quirky, θ-associated (Marantz lexical, Kalin byLexical);
• default — elsewhere / last-resort unmarked case;
• uncased — no source valued the nominal: the crash (Kalin unlicensed, a Case-Filter violation).

A total assignment account never produces uncased; a licensing account can.

• structural : Source
• inherent : Source
• default : Source
• uncased : Source

@[implicit_reducible]

instance Case.instDecidableEqSource : DecidableEq Source

Equations

• Case.instDecidableEqSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Case.instReprSource : Repr Source

Equations

• Case.instReprSource = { reprPrec := Case.instReprSource.repr }

def Case.instReprSource.repr : Source → ℕ → Std.Format

Equations

• Case.instReprSource.repr Case.Source.structural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Source.structural")).group prec✝
• Case.instReprSource.repr Case.Source.inherent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Source.inherent")).group prec✝
• Case.instReprSource.repr Case.Source.default prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Source.default")).group prec✝
• Case.instReprSource.repr Case.Source.uncased prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Source.uncased")).group prec✝

@[implicit_reducible]

instance Case.instInhabitedSource : Inhabited Source

Equations

• Case.instInhabitedSource = { default := Case.instInhabitedSource.default }

def Case.Source.IsStructural (s : Source) : Prop

The case was valued by configuration or Agree. The structural-vs-inherent distinction is a property of the source, not of the Case cell.

Equations

• s.IsStructural = (s = Case.Source.structural)

@[implicit_reducible]

instance Case.instDecidableIsStructural (s : Source) : Decidable s.IsStructural

Equations

• Case.instDecidableIsStructural s = Case.instDecidableIsStructural._aux_1 s

def Case.Source.IsCrash (s : Source) : Prop

The derivation crashed: no source valued the nominal. Distinguishes a licensing account (which can fail) from a total assignment account.

Equations

• s.IsCrash = (s = Case.Source.uncased)

@[implicit_reducible]

instance Case.instDecidableIsCrash (s : Source) : Decidable s.IsCrash

Equations

• Case.instDecidableIsCrash s = Case.instDecidableIsCrash._aux_1 s