Aspect Heads (Outer / Inner Split)

@cite{travis-2010} @cite{macdonald-2008} @cite{tsai-2008} @cite{sybesma-2017}

Substrate types for the bipartite split-aspect cartography that has emerged from work on Mandarin and Cantonese (and before them, English event-structure decomposition). Following the convention that .Voice is a single Cat constructor distinguished by VoiceFlavor (Theories/Syntax/Minimalist/Voice.lean), we keep Cat.Asp as a single F2 constructor and represent the AspP_outer / AspP_inner distinction as AspFlavor on an AspHead record. This avoids a new constructor (no fValue collision below v at F1) and keeps Cat consumers — the 30+ files that pattern-match on Cat — unchanged.

What lives here

• AspFlavor — outer / inner.
• AspHead — the analytical record (flavor + selectional spec + optional Probe + feature stack), parallel to VoiceHead.
• A small number of substrate predicates (isOuter, isInner, defaultFLevel).

What does NOT live here

• The viewpoint-aspect denotation (Theories/Semantics/Tense/Aspect/Core.lean ViewpointType). Travis, MacDonald, Tsai disagree on AspO denotation, so "AspP_outer hosts viewpoint aspect" is not a uniform substrate identity. Per-morpheme bridges live in the relevant Fragment files (e.g., -le ↦ ViewpointType.perfective in Fragments/Mandarin/Aspect.lean); the substrate stays neutral.

• The [±D] dynamic feature analysis (@cite{lin-liu-2009}; @cite{shen-2004}). [+D] does two distinct jobs: (a) a property of the predicate (Aktionsart-derived), (b) a selectional requirement on AspO to combine with a dynamic complement. We model only (b) here, by exposing selectsDynamicity : Option Features.Dynamicity. The predicate-side property already lives in Features/Aktionsart.lean (Dynamicity); this field on AspHead encodes which value (if any) the head requires.

• @cite{liu-yip-2026}'s Cantonese -faan does NOT carry the dynamicity restriction (it composes with stative jau 'have'). Encoded by leaving selectsDynamicity = none on -faan's AspHead; encoding it as some .dynamic would over-predict.

• Per-morpheme syntactic typing (Mandarin you, zai, -le, -guo, -zhe; Cantonese -faan, -gwo, jau, zoi) lives in the per-language Fragment files.

• The "split aspect" framework as a named theory (the cluster of @cite{travis-2010}, @cite{macdonald-2008}, @cite{tsai-2008}, @cite{sybesma-2017}) — its analytical claims live in Phenomena/Complementation/Studies/LiuYip2026.lean, which is the first paper-anchored consumer of this substrate. Promotion to a separate SplitAspect.lean theory file would follow when a second study consumes the same primitives.

inductive Minimalist.AspFlavor : Type

Flavor of an aspect head.

The outer/inner cut is the binary simplification (@cite{travis-2010}, @cite{macdonald-2008}, @cite{tsai-2008}, @cite{sybesma-2017}) of @cite{cinque-1999}'s finer-grained adverbial sequence. Outer aspect sits above vP (and is what viewpoint morphemes like Mandarin -le, -guo, -zhe and Cantonese -zo, -gwo, -gan, -faan canonically associate with); inner aspect sits inside the v-shell (and is what Aktionsart morphemes like phase complements -dao, -hao, -wan, -diao or Cantonese -dim, -dou, -zoek, -jyun, -hou canonically associate with).

This file does NOT take a position on whether the cut is binary cross-linguistically; languages with finer cartographies (e.g., @cite{cinque-1999}'s 30+ adverbial heads) would need a richer flavor type.

• outer : AspFlavor

  Outer aspect: above vP, viewpoint-host position.

• inner : AspFlavor

  Inner aspect: inside the v-shell, Aktionsart-host position.

@[implicit_reducible]

instance Minimalist.instDecidableEqAspFlavor : DecidableEq AspFlavor

Equations

• Minimalist.instDecidableEqAspFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.instReprAspFlavor : Repr AspFlavor

Equations

• Minimalist.instReprAspFlavor = { reprPrec := Minimalist.instReprAspFlavor.repr }

def Minimalist.instReprAspFlavor.repr : AspFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instInhabitedAspFlavor : Inhabited AspFlavor

Equations

• Minimalist.instInhabitedAspFlavor = { default := Minimalist.instInhabitedAspFlavor.default }

def Minimalist.instInhabitedAspFlavor.default : AspFlavor

Equations

• Minimalist.instInhabitedAspFlavor.default = Minimalist.AspFlavor.outer

def Minimalist.AspFlavor.isOuter : AspFlavor → Bool

Predicate: this flavor is outer aspect.

Equations

• Minimalist.AspFlavor.outer.isOuter = true
• Minimalist.AspFlavor.inner.isOuter = false

def Minimalist.AspFlavor.isInner : AspFlavor → Bool

Predicate: this flavor is inner aspect.

Equations

• Minimalist.AspFlavor.outer.isInner = false
• Minimalist.AspFlavor.inner.isInner = true

theorem Minimalist.AspFlavor.outer_xor_inner (f : AspFlavor) : f.isOuter = true ↔ f.isInner = false

The two flavors partition AspFlavor.

def Minimalist.AspFlavor.defaultFLevel : AspFlavor → ℕ

The fValue "slot" an aspect head conventionally occupies, given its flavor.

Outer aspect lives at fValue 2 (alongside T, Mod, Neg, Pol, Evid, Q, Path) — the specification domain. Inner aspect lives inside the v-shell, structurally below v (fValue 1) but above V (fValue 0). The current fValue : Cat → Nat scheme has no integer slot between F0 and F1; we report the v-shell parent's level (1) as a conservative approximation. The semantics-audit-flagged refactor to a finer fValue (e.g., Rat-valued, or sub-ranks) would let .inner return a value strictly between 0 and 1; until that lands, downstream consumers should not rely on inner-vs-outer ordering at the fValue level and should consult flavor directly.

Equations

• Minimalist.AspFlavor.outer.defaultFLevel = 2
• Minimalist.AspFlavor.inner.defaultFLevel = 1

structure Minimalist.AspHead : Type

An aspect head, parallel to VoiceHead.

Carries: (a) which flavor (outer/inner), (b) optional selectional requirement on the complement's dynamicity, (c) optional ProbeProfile when the head is itself an Agree probe (@cite{liu-yip-2026} analyzes Mandarin you and Cantonese -faan as probe-bearing AspO heads), (d) any Agree-relevant features (e.g., [+EXP] on the experiential AspO that licenses -guo).

The selectsDynamicity field separates selectional dynamicity (head-borne) from predicate dynamicity (Features.Dynamicity, Aktionsart-derived). A head with selectsDynamicity := some .dynamic requires its complement to be a dynamic predicate; a head with selectsDynamicity := none is indifferent.

• flavor : AspFlavor

  The flavor (outer or inner).

• selectsDynamicity : Option Features.Dynamicity

  Selectional requirement on the complement's dynamicity, if any. none = no requirement (compatible with stative or dynamic complements); some .dynamic = requires dynamic complement (@cite{lin-liu-2009}'s [+D]); some .stative = requires stative complement (rare; defensive default).

• probe : Option ProbeProfile

  Optional probe profile: populated when the head triggers Agree. The probe's probeHead is conventionally .Asp; the flavor field on AspHead disambiguates outer-vs-inner at the analytical level.

• features : FeatureBundle

  Agree-relevant features on the head (e.g., [+EXP] for experiential AspO, [uD] for the AspO that triggers you-movement).

def Minimalist.instReprAspHead.repr : AspHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprAspHead : Repr AspHead

Equations

• Minimalist.instReprAspHead = { reprPrec := Minimalist.instReprAspHead.repr }

def Minimalist.AspHead.bareOuter : AspHead

Convenience constructor: a bare outer-aspect head with no selectional or featural commitments. Used for AspO heads whose only role is to project the position (e.g., when a moved adverb lands in Spec,AspP_outer without the head itself imposing constraints).

Equations

• Minimalist.AspHead.bareOuter = { flavor := Minimalist.AspFlavor.outer }

def Minimalist.AspHead.bareInner : AspHead

Convenience constructor: a bare inner-aspect head.

Equations

• Minimalist.AspHead.bareInner = { flavor := Minimalist.AspFlavor.inner }

def Minimalist.AspHead.outerDynamic : AspHead

Outer-aspect head with a [+D] dynamic-complement selectional requirement (@cite{lin-liu-2009}). Used to type Mandarin's matrix Asp_outer when it needs to license you via Agree.

Equations

• Minimalist.AspHead.outerDynamic = { flavor := Minimalist.AspFlavor.outer, selectsDynamicity := some Features.Dynamicity.dynamic }

def Minimalist.AspHead.isOuter (h : AspHead) : Bool

A head is outer iff its flavor is .outer.

Equations

• h.isOuter = h.flavor.isOuter

def Minimalist.AspHead.isInner (h : AspHead) : Bool

A head is inner iff its flavor is .inner.

Equations

• h.isInner = h.flavor.isInner

def Minimalist.AspHead.isProbeBearing (h : AspHead) : Bool

A head carries a probe iff probe.isSome.

Equations

• h.isProbeBearing = h.probe.isSome

def Minimalist.AspHead.licensesDynamicity (h : AspHead) (d : Features.Dynamicity) : Bool

Dynamicity-licensing: this head licenses a complement of the given dynamicity. A head with no requirement (selectsDynamicity = none) licenses any complement; otherwise the complement's dynamicity must match.

Equations

• h.licensesDynamicity d = match h.selectsDynamicity with | none => true | some required => decide (required = d)

theorem Minimalist.bareOuter_no_dyn_req : AspHead.bareOuter.selectsDynamicity = none

A bareOuter head has no selectional requirement.

theorem Minimalist.bareInner_no_dyn_req : AspHead.bareInner.selectsDynamicity = none

A bareInner head has no selectional requirement.

theorem Minimalist.bareOuter_licenses_all (d : Features.Dynamicity) : AspHead.bareOuter.licensesDynamicity d = true

A bareOuter head licenses both dynamic and stative complements.

theorem Minimalist.outerDynamic_licenses_dynamic_only : AspHead.outerDynamic.licensesDynamicity Features.Dynamicity.dynamic = true ∧ AspHead.outerDynamic.licensesDynamicity Features.Dynamicity.stative = false

An outerDynamic head licenses dynamic but not stative complements — this is the @cite{lin-liu-2009} [+D] constraint, derived rather than stipulated.