Liu & Yip 2026: Again, finiteness, and split aspect in Chinese languages

[LY26] (NLLT 44:25, doi 10.1007/s11049-026-09708-5).

Paper's central claims

(1) Hierarchical, size-based finiteness in Chinese. Three clause sizes: Type I (CP, finite), Type II (TP, nonfinite without Aspect Restructuring), Type III (vP, nonfinite with Aspect Restructuring). (2) Split aspect. Two aspectual projections in the spine: AspP_outer above vP, AspP_inner inside vP. (3) Asymmetry of again-elements. Mandarin preverbal you and Cantonese postverbal -faan associate with AspP_outer (and may exhibit "exceptional scopal behavior" — you-skipping by movement+reconstruction; -faan-lowering by Agree). Mandarin zai and Cantonese -gwo associate with AspP_inner (and never scope-mismatch). (4) Defective intervention. When the embedded clause is TP-sized, its embedded AspP_outer blocks the matrix probe's reach to the embedded again-element. (5) [WL23] ICH (proposition > situation > event) instantiated by Chinese as CP > TP > vP. (6) vP is the minimal nonfinite size. Empirical: AspP_inner is mandatory above V; aspect-lowering and -gwo-lowering systematically don't occur.

What this Studies file commits to substrate

• No new substrate files. The [WL23] ICH, the [Wur01] truncation operator, and the [Pes21] Exfoliation primitive all violate the ≥ 2-paper-anchor graduation rule. They live as local definitions here, ready to graduate when a second study consumes them.

• The substrate-level addition [LY26]'s analysis does motivate is the bipartite split-aspect typing: AspFlavor and AspHead, landed in Syntax/Minimalist/Aspect.lean parallel to VoiceHead { flavor }. That commitment is independent of the analytical claims of this paper — it is consumed by [Tra10b], [MD08], [Tsa08], [Syb17], and [LY26] jointly — so it warranted substrate placement.

What this Studies file does NOT commit to

• Defective intervention is NOT bilateral labeling. [LY26]'s intervener is a featurally-matching head occupying a probe position ([Cho00] defective intervention), not a category in a bilateral label ([Kei20] horizon opacity). The two coincide on the Type II / Type III contrast but make distinct predictions on featural mismatch. The defectiveIntervention predicate below uses head-as-intervener; it does not call Probe.Profile.transparentToLabel.

• Aspect-lowering and -faan-lowering are parallel, not the same. Both involve matrix-AspP_outer Agree across a vP boundary, but the empirical diagnostics differ (e.g., -zhe_CONT vs -zhe_IPFV asymmetry; -gwo not lowering in Cantonese). No reduction theorem is asserted.

• The [WL23] ICH is not a baked-in LinearOrder with an implication on transparency. The order on ComplementClass is independent of the claim that transparency is downward-closed; the latter is a theorem about a transparency relation, not a definitional property.

• Minimal-vP is empirical, not structural. Encoded as a per-fragment drift sentry, falsifiable by a single new datum.

Cross-framework reconciliation

§11 below documents divergences with HPSG (lexical-rule analysis of "you-skipping"), Dependency Grammar (no AspP, no ICH), CCG (forward composition), Fragments/Italian/Modals.lean's [Hac06] restructuring substrate, Studies/Landau2015.lean's ControlTier, and Syntax/Minimalist/Phase.lean. The [Cin06] vs. [Wur01] restructuring rivalry is made explicit in §10 as a refutation theorem candidate.

def LiuYip2026.typeI : Minimalist.ComplementSize

[LY26]'s Type I: finite (CP). Selected by xiangxin 'believe', shuo 'say' etc.; blocks you-skipping and -faan-lowering.

Equations

• LiuYip2026.typeI = Minimalist.ComplementSize.cP

def LiuYip2026.typeII : Minimalist.ComplementSize

[LY26]'s Type II: nonfinite without Aspect Restructuring (TP). Selected when the predicate licenses TP but blocks -faan-lowering via embedded AspP_outer intervention.

Equations

• LiuYip2026.typeII = Minimalist.ComplementSize.tP

def LiuYip2026.typeIII : Minimalist.ComplementSize

[LY26]'s Type III: nonfinite with Aspect Restructuring (vP). Selected by xiang 'want', rang 'let' etc.; permits you-skipping and -faan-lowering.

Equations

• LiuYip2026.typeIII = Minimalist.ComplementSize.vP

theorem LiuYip2026.types_ordered : typeIII.fLevel < typeII.fLevel ∧ typeII.fLevel < typeI.fLevel

Type ordering: vP < TP < CP (size-wise, per fValue).

inductive LiuYip2026.ComplementClass : Type

The Implicational Complementation Hierarchy of [WL23]: proposition > situation > event in transparency-decreasing order.

Local to this Studies file; promotion to Syntax/Complementation/ is contingent on a second paper-anchored consumer (the control studies — e.g. Studies/Landau2015.lean — and Studies/Grano2024.lean are candidate second sites).

LinearOrder is not derived: the implicational content of the ICH is a theorem about a transparency relation, not a structural property of the class lattice. The order here is just the enum's natural one (event < situation < proposition); the implicational claim is transparency_downward_closed below.

• event : ComplementClass

  Smallest, most transparent: vP-level event reports.

• situation : ComplementClass

  Mid: TP-level situation reports.

• proposition : ComplementClass

  Largest, most opaque: CP-level proposition reports.

@[implicit_reducible]

instance LiuYip2026.instDecidableEqComplementClass : DecidableEq ComplementClass

Equations

• LiuYip2026.instDecidableEqComplementClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LiuYip2026.instReprComplementClass.repr : ComplementClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LiuYip2026.instReprComplementClass : Repr ComplementClass

Equations

• LiuYip2026.instReprComplementClass = { reprPrec := LiuYip2026.instReprComplementClass.repr }

def LiuYip2026.ComplementClass.rank : ComplementClass → ℕ

Numeric rank for ComplementClass: event = 0, situation = 1, proposition = 2.

Equations

• LiuYip2026.ComplementClass.event.rank = 0
• LiuYip2026.ComplementClass.situation.rank = 1
• LiuYip2026.ComplementClass.proposition.rank = 2

def LiuYip2026.complementClass (cs : Minimalist.ComplementSize) : ComplementClass

Project a ComplementSize onto the [WL23] 3-tier ComplementClass, by fValue thresholds. This is [LY26]'s Chinese-specific mapping (the paper notes explicitly that other languages may calibrate differently). The Studies file instantiates the mapping; a richer cross-linguistic substrate would parameterize it per-language.

Equations

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

theorem LiuYip2026.typeI_proposition : complementClass typeI = ComplementClass.proposition

theorem LiuYip2026.typeII_situation : complementClass typeII = ComplementClass.situation

theorem LiuYip2026.typeIII_event : complementClass typeIII = ComplementClass.event

def LiuYip2026.restructure : Minimalist.ClauseSpine → Option Minimalist.ClauseSpine

[Wur01]-style restructuring: drop the topmost projected head from a ClauseSpine. Returns none if the spine has only one head (the floor).

Local to this Studies file. Fails the ≥2-consumer rule for substrate; promotion candidate when Fragments/Italian/Modals.lean's informal restructuring discussion gets a Studies file or when a [Wur14] study lands.

Implementation: the dropLast of an at-least-2-element list is non-empty, proved via the [x, y :: rest] pattern's structural guarantee.

Equations

• LiuYip2026.restructure { projectedHeads := [], nonempty := h } = absurd LiuYip2026.restructure._proof_1 h
• LiuYip2026.restructure { projectedHeads := [head], nonempty := nonempty } = none
• LiuYip2026.restructure { projectedHeads := x_1 :: y :: rest, nonempty := nonempty } = some { projectedHeads := x_1 :: (y :: rest).dropLast, nonempty := ⋯ }

theorem LiuYip2026.restructure_decreases (s s' : Minimalist.ClauseSpine) : s' ∈ restructure s → s'.projectedHeads.length < s.projectedHeads.length

Restructuring strictly decreases spine length (when defined). The proof unfolds via the structural constructors of ClauseSpine.

def LiuYip2026.intervenes (matrixProbe embeddedHead : Minimalist.AspHead) : Bool

[LY26]'s defective intervention ([Cho00]): an embedded head of the same category as the matrix probe blocks Agree, regardless of bilateral labeling. The featural-compatibility check enforces that intervention is by an element occupying an embedded probe position, not by a category in a sister's label.

intervenes returns true when the embedded head's selectional requirement (e.g. Asp_outer's [+D] dynamicity expectation) overlaps with the matrix probe's expectation in a way that creates a defective intervention configuration. The simplest such check: same-flavor + same-or-compatible selectional spec.

This predicate deliberately does NOT call Probe.Profile.transparentToLabel — head-as-intervener and label-as-locus diverge on featurally-mismatched probes.

Equations

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

def LiuYip2026.youAspHead : Minimalist.AspHead

Studies-side projection: Mandarin you 'again' is typed as an AspP_outer-associated probe-bearing head with a [+D] dynamicity selectional restriction (per [LL09], building on [She04]). The lexical entry in Fragments/Mandarin/Particles.lean carries only the presupposition trigger; the syntactic typing here is [LY26]'s analytical commitment.

Equations

• LiuYip2026.youAspHead = Minimalist.AspHead.outerDynamic

def LiuYip2026.zaiAspHead : Minimalist.AspHead

Studies-side projection: Mandarin zai 'again' is typed as an AspP_inner-associated bare head, no dynamicity restriction.

Equations

• LiuYip2026.zaiAspHead = Minimalist.AspHead.bareInner

theorem LiuYip2026.you_outer : youAspHead.flavor = Minimalist.AspFlavor.outer

theorem LiuYip2026.zai_inner : zaiAspHead.flavor = Minimalist.AspFlavor.inner

theorem LiuYip2026.you_requires_dynamic : youAspHead.selectsDynamicity = some Features.Dynamicity.dynamic

theorem LiuYip2026.zai_no_requirement : zaiAspHead.selectsDynamicity = none

def LiuYip2026.faanAspHead : Minimalist.AspHead

Studies-side projection: Cantonese -faan 'again' is AspP_outer-associated but, unlike Mandarin you, does NOT carry a [+D] selectional restriction (it is compatible with stative jau 'have' per [LY26]).

Equations

• LiuYip2026.faanAspHead = Cantonese.Aspect.faan.toAspHead

def LiuYip2026.gwoAspHead : Minimalist.AspHead

Studies-side projection: Cantonese -gwo (repetitive use) is AspP_inner-associated. Its experiential use is also AspP_inner per the lexical entry, but pragmatically distinct.

Equations

• LiuYip2026.gwoAspHead = Cantonese.Aspect.gwo.toAspHead

theorem LiuYip2026.faan_outer_no_dyn : faanAspHead.flavor = Minimalist.AspFlavor.outer ∧ faanAspHead.selectsDynamicity = none

theorem LiuYip2026.gwo_inner : gwoAspHead.flavor = Minimalist.AspFlavor.inner

theorem LiuYip2026.you_vs_faan_dynamicity : youAspHead.selectsDynamicity = some Features.Dynamicity.dynamic ∧ faanAspHead.selectsDynamicity = none

Mandarin you and Cantonese -faan are BOTH outer-aspect, but only you carries [+D]. Encoding -faan with selectsDynamicity = some .dynamic would over-predict (it would force incompatibility with stative jau).

theorem LiuYip2026.generalization_I_mandarin : youAspHead.isOuter = true ∧ zaiAspHead.isOuter = false

Generalization I ([LY26]): in Mandarin, an again-element exhibits exceptional scopal behavior IFF it is outer-aspect-associated.

On the substrate: youAspHead.isOuter = true (you may skip); zaiAspHead.isOuter = false (zai may not). The empirical content is the biconditional between AspFlavor and the scope-mismatch facts the paper documents.

theorem LiuYip2026.generalization_I_cantonese : faanAspHead.isOuter = true ∧ gwoAspHead.isOuter = false

Generalization I (Cantonese counterpart): -faan (outer) may lower; -gwo (inner) may not.

theorem LiuYip2026.generalization_II_mandarin : typeIII.fLevel < typeII.fLevel ∧ typeII.fLevel < typeI.fLevel

Generalization II ([LY26]): the exceptional scopal behavior of again may cross nonfinite (vP) but not finite (CP) clause boundaries.

On the substrate: this is an instance of upward entailment of opacity (Probe.lean upward_entailment_label). Stated here without invoking bilateral labeling — see §5 above. The content is that for any matrix again-bearing AspO probe, the complement clause's size determines transparency: vP transparent, TP / CP opaque.

theorem LiuYip2026.correlation_I_mandarin : youAspHead.licensesDynamicity Features.Dynamicity.dynamic = true ∧ youAspHead.licensesDynamicity Features.Dynamicity.stative = false ∧ zaiAspHead.licensesDynamicity Features.Dynamicity.dynamic = true ∧ zaiAspHead.licensesDynamicity Features.Dynamicity.stative = true

Correlation I ([LY26], Mandarin): an again-element exhibits exceptional scopal behavior IFF it cannot surface in an embedded nonfinite clause without a dynamic ([+D]) aspect.

On the substrate: this is the consequence of Mandarin you's selectsDynamicity = some .dynamic. zai, with no such restriction, can attach to either dynamic or stative complements but never scopes mismatch.

theorem LiuYip2026.correlation_II_mandarin : Minimalist.AspFlavor.outer.defaultFLevel > Minimalist.AspFlavor.inner.defaultFLevel

Correlation II ([LY26]): an again-element exhibits exceptional scopal behavior IFF it is structurally higher than aspectual elements.

On the substrate: AspO has higher defaultFLevel (2) than AspI (1). Outer you / -faan are above the inner aspectual elements; inner zai / -gwo are not.

The minimal-vP claim is an empirical generalization about Chinese, not a structural property derived from substrate. Stated here as a per-fragment assertion that every nonfinite-clause-taking predicate in the Mandarin and Cantonese fragments selects a complement of size ≥ vP. Falsifiable by a single new datum.

theorem LiuYip2026.mandarin_nonfinite_takers_min_vP : ([Mandarin.Predicates.xiang, Mandarin.Predicates.rang, Mandarin.Predicates.quan, Mandarin.Predicates.bi, Mandarin.Predicates.dasuan, Mandarin.Predicates.shefa].all fun (x : Mandarin.Predicates.MandarinVerbEntry) => decide (x.complementType = ComplementType.infinitival)) = true

All Mandarin nonfinite-takers (xiang, rang, quan, bi, dasuan, shefa) have complementType = .infinitival, consistent with vP-as-floor and falsifiable by a single new datum. The Fragment-side companion is Mandarin.Predicates.liuyip_partition.

theorem LiuYip2026.cantonese_nonfinite_takers_min_vP : ([Cantonese.Predicates.soeng, Cantonese.Predicates.hyun, Cantonese.Predicates.bik, Cantonese.Predicates.giu, Cantonese.Predicates.daasyun].all fun (x : Cantonese.Predicates.CTPEntry) => decide (x.selects = [Cantonese.Predicates.ComplementSizeLabel.vP])) = true

All Cantonese nonfinite-takers select [.vP] per the per-language fragment classification ([LY26]).

Internal tension in the [LY26] architecture

There is a hidden incoherence: the spine substrate (ClauseSpine + AspFlavor.outer / inner always projected when present) commits to [Cin06]'s "always project all functional heads" view; the restructuring operator above (truncate the topmost head) commits to [Wur01]'s "remove projection on restructuring" view. These are direct rivals on the same Chinese aspect data.

The current formalization adopts both — and lives with the tension — because:

(a) The split-aspect substrate (AspHead { flavor }) is theory-neutral: a flavor field on a single Cat.Asp constructor doesn't itself say that AspP_outer is always projected. Languages can opt in to projecting only one flavor.

(b) The local restructure operator above is Wurmbrand-flavored, not a cross-framework commitment. A Cinque-flavored alternative would leave the spine unchanged but mark some heads as silent — trivially, id. The substrate accommodates both projections; the rivalry is visible rather than hidden.

The sharp refutation theorem ¬ (Wurmbrand.truncated.projects .Asp ↔ Cinque.full.projects .Asp) is contingent on a Cinque-style "always project" formalization landing in Syntax/Minimalist/. Until then, the rivalry is documented in prose, not theorem.

def LiuYip2026.cinqueRestructure (s : Minimalist.ClauseSpine) : Minimalist.ClauseSpine

A trivial Cinque-flavored "restructuring" (identity) for comparison with the Wurmbrand-flavored restructure above. [Cin06]'s claim is that restructuring is projection-marking, not truncation; structurally, the spine is unchanged.

Equations

• LiuYip2026.cinqueRestructure s = s

theorem LiuYip2026.cinque_vs_wurmbrand_diverge (s s' : Minimalist.ClauseSpine) : s' ∈ restructure s → s'.projectedHeads.length < (cinqueRestructure s).projectedHeads.length

Sister-framework treatments of "you-skipping" / -faan-lowering

Each major sister framework analyzes the same data via a fundamentally different mechanism. This section documents the divergences without attempting bridge theorems (which would require the sister frameworks to have Studies-level Chinese formalizations they currently lack):

• HPSG (Syntax/HPSG/Basic.lean): no clausal spine, no AspP, no ICH. The "you-skipping" pattern would naturally be a lexical rule on argument structure (an argument-structure–changing lexical-cxt, in the RSRL terms of Syntax/HPSG/Construction). [LY26]'s movement+reconstruction has no HPSG analog. SILENT DIVERGENCE.

• Dependency Grammar (Studies/Osborne2019Control.lean): control and raising are structurally identical in DG; AspP is absent. "you-skipping," restructuring, and -faan-lowering would all be xcomp plus enhanced-edge propagation. SILENT DIVERGENCE (irreconcilable at substrate level; bridgeable only at the empirical prediction level).

• CCG (Syntax/CCG/Basic.lean, Scope.lean): scope mismatch is type-shifting + composition. you's skipping naturally maps to forward composition; no movement+reconstruction needed. A bridge theorem LiuYip.youSkipping iff CCG.derivableViaComposition is tractable on a small fragment but not attempted here.

• Fragments/Italian/Modals.lean has a developed restructuring substrate based on [Riz78] + [Hac06] (event-relativity analysis). The [LY26] formalization here uses a [Wur01] truncation operator (§4 above). The two are direct rivals; integration with the Italian substrate would be a productive next step but is deferred (the Italian file currently has no Wurmbrand-truncation bridge of its own).

• Studies/Landau2015.lean has ControlTier (predicative vs logophoric) cross-classifying CTPs along an axis the [WL23] ICH ComplementClass (event/situation/proposition) parallels. A bridge theorem LiuYip.proposition → Landau.logophoric is candidate future work; both Studies files currently formalize their own complement-class projections without sharing substrate.

• Syntax/Minimalist/Phase.lean has [Cho00] / [Cho01] phase machinery (PICStrength). [LY26]'s intervention is by AspP_outer, a non-phase head — defective intervention is a third locality regime alongside PICStrength.{strong, weak, linearizationBound}. The current formalization silently bypasses the Phase substrate. Resolution: either extend PICStrength with a "head-as-intervener" case, or add explicit prose noting the alternative locality model.

def LiuYip2026.ComplementClass.size : ComplementClass → Minimalist.ComplementSize

[WL23] ICH classes track structural size — proposition = CP, situation = TP, event = vP. Replaces the retired projection onto the deleted surface enum, which forced situation/event onto an Ā-dependency cell the ICH does not claim. ([Dea26]'s shell/Ā axes live in Syntax/Clause/Complementation; the ICH makes no claim on either axis, so no bridge is stated.)

Equations

• LiuYip2026.ComplementClass.proposition.size = Minimalist.ComplementSize.cP
• LiuYip2026.ComplementClass.situation.size = Minimalist.ComplementSize.tP
• LiuYip2026.ComplementClass.event.size = Minimalist.ComplementSize.vP

Deferred items

• [Pes21] Exfoliation: not formalized here. The shuo-CP puzzle [LY26] resolve via Exfoliation (CP layer peelable under A-dependency) is left as prose. Promotion to a substrate operator awaits a second consumer.

• Semantics/Again/ substrate: a uniform again-presupposition substrate ([vS96] / [Bec06] parameterization) is recommended but not landed. Without it, every again-element's presupposition is encoded independently in its Fragment lexical entry, which silently commits to an anti-decompositional account when it type-equates you's repetitive reading with zai's. The substrate module is deferred until a German-wieder or English-again study joins.

• The repetitive-vs-restitutive distinction: explicitly bracketed by [LY26] as out of scope. The Mandarin you Fragment entry currently encodes only the repetitive reading; a you_restitutive companion entry would be a small addition if needed.

• The minimal-vP empirical claim (§9): per-fragment drift sentries here cover Mandarin (6 verbs) and Cantonese (5 verbs). A larger cohort, especially for typologically distant languages claimed to have similar restructuring, would strengthen the empirical content.

• [Wur14] restructuring data (German / Romance): the local restructure operator is [Wur01]-flavored and tested only on Chinese. [Wur14]'s lexical / functional restructuring dichotomy is a richer typology this Studies file does not yet engage.