Verb ↔ root content accessors

The integration seam (P-HUB) between a Verb and the (total) root it carries (Verb.root : Verb.Root): a verb's [Bha24] outcome cardinality and change-entailment type are read off its own root. The coarse Levin-class view of the kind signature (Verb.classKinds) is kept as a separate, named provenance — the realization label's prediction, not the source of truth (Verb.kinds); the two agree only by theorem, never by construction.

RootType and Verb.Root.changeType live in Morphology/RootTypology.lean, so these accessors (which mention them) live here rather than in Verb/Basic.lean.

Main definitions

• Verb.classKinds — the class-derived kind signature (the coarse Levin view)
• Verb.outcomes — the verb's outcome-set cardinality
• Verb.changeType — the verb's change-entailment type (derived from its root)

Main results

• Verb.classKinds_wellFormed — the class view, when present, is a well-formed signature (grounded in rootEntailments_wellFormed)

(Verb.kinds, the root-sourced source-of-truth signature, lives in Verb/Basic.lean.)

def Verb.classKinds (v : Verb) : Option Root.Kinds

The kind signature [Lev93] attributes to the verb via its class (LevinClass.rootEntailments) — the coarse REALIZATION-layer view, distinct from the root's own kinds. They are independent provenances; a classKinds = kinds agreement is a theorem, not a default.

Equations

• v.classKinds = Option.map Semantics.Lexical.LevinClass.rootEntailments v.levinClass

theorem Verb.classKinds_wellFormed (v : Verb) (s : Root.Kinds) : s ∈ v.classKinds → s.WellFormed

The class-derived signature, when present, is well-formed (collocationally closed) — classKinds's grounding, inherited from rootEntailments_wellFormed. The stronger classKinds ⊆ Verb.kinds is deliberately not a theorem: classKinds (the Levin label's prediction) and Verb.kinds (the verb's own root) are independent provenances, so they coincide only for a faithfully classified verb — a per-verb hypothesis the type does not enforce.

def Verb.outcomes (v : Verb) : Option OutcomeCardinality

The verb's outcome-set cardinality ([Bha24]), read off its root (none where the root is not annotated for outcomes).

Equations

• v.outcomes = v.root.outcomes

def Verb.changeType (v : Verb) : RootType

The verb's change-entailment type ([BEJ+21]), derived from its root's kind signature.

Equations

• v.changeType = v.root.changeType

theorem Verb.changeType_ignores_outcomes {v v' : Verb} (h : v.root.entailments = v'.root.entailments) : v.changeType = v'.changeType

A verb's changeType is blind to its root's outcome axis (it factors through Verb.Root.changeType): verbs whose roots share entailments share a changeType whatever their outcomes — why outcome cardinality is an independent dimension.