Late Merger

@cite{lebeaux-1988} @cite{takahashi-hulsey-2009} @cite{bhatt-pancheva-2004}

Late merger (originally @cite{lebeaux-1988} for adjuncts; extended to NP restrictors as Wholesale Late Merger by @cite{takahashi-hulsey-2009}; extended to degree clauses by @cite{bhatt-pancheva-2004}) introduces some sub-constituent of a moved phrase countercyclically at a non-base position on the movement chain.

Generic shape

Late merger comes in flavors that differ only in which positions are admissible targets for late merger:

• WLM (NP restrictors): admissible iff case can be assigned there.
• B&P (degree clauses): admissible iff the position can host a ⟨t⟩-scope for the degree quantifier (subject to the Heim-Kennedy Constraint).
• Lebeaux (adjuncts): admissible everywhere on the chain.

The Condition C bleeding profile is the same in every flavor: late merger bleeds Condition C iff there exists an admissible chain position strictly above the pronoun binder. We factor this shared shape into the polymorphic lateMergerBleeds operation, with wlmBleedsCondC as the case-licensing specialization for NPs.

Core ideas

The late-merger account is theory-neutral about the encoding of movement chains. Under the copy theory of movement, a moved phrase leaves explicit copies at every position on its chain. Under the trace-as-leaf encoding that linglib's substrate currently uses (MCB ^ρ-form-with-indexing — see Basic.lean SyntacticObject docstring), each chain position is marked by a .trace n leaf sharing the index n with its mover. Either encoding licenses the same Late Merger reasoning: the sub-constituent is introduced at any admissible chain position, regardless of how that position is materialized in the SO. This file's chain : List ChainPosition abstraction is encoding-agnostic at the API level; the substrate choice (trace-as-leaf) shows up only at the level of the concrete SO produced after IM.

If the late-merged constituent contains an R-expression that would be c-commanded by a coreferential pronoun at the base position, full reconstruction triggers a Condition C violation. Late merger can avoid this by introducing the constituent at a higher admissible copy position.

@cite{gong-2022} shows that for NP restrictors the case requirement is the key factor controlling Condition C reconstruction effects in Mongolian scrambling: reconstruction tracks case positions, not the A/A-bar distinction.

Definitions

• lateMergerBleeds — generic late-merger bleeding test, polymorphic in position type and admissibility predicate
• ChainPosition — a position on a movement chain with its height and case availability
• wlmBleedsCondC — case-licensing specialization for NP restrictors
• wlmForcesReconstruction — negation of wlmBleedsCondC

def Minimalist.lateMergerBleeds {α : Type u_1} (admissible : α → Bool) (height : α → ℕ) (chain : List α) (binderHeight : ℕ) : Bool

Generic late-merger bleeding test.

Given a movement chain (any list of positions), a height projection, an admissibility predicate, and a binder height: late merger bleeds Condition C iff there exists an admissible chain position strictly above the binder.

Specializations:

• wlmBleedsCondC (@cite{takahashi-hulsey-2009}): NP restrictors, admissible := case-available
• Late merger of degree clauses (@cite{bhatt-pancheva-2004}): degree clauses, admissible := position can host a ⟨t⟩-scope subject to the Heim-Kennedy Constraint

Equations

• Minimalist.lateMergerBleeds admissible height chain binderHeight = chain.any fun (p : α) => admissible p && decide (height p > binderHeight)

theorem Minimalist.lateMerger_bleeding_monotone {α : Type u_1} (admissible : α → Bool) (height : α → ℕ) (chain : List α) (p : α) (binderHeight : ℕ) (h : lateMergerBleeds admissible height chain binderHeight = true) : lateMergerBleeds admissible height (p :: chain) binderHeight = true

Adding a chain position never removes late-merger bleeding.

theorem Minimalist.admissible_above_binder_bleeds {α : Type u_1} (admissible : α → Bool) (height : α → ℕ) (chain : List α) (p : α) (binderHeight : ℕ) (hadm : admissible p = true) (hgt : height p > binderHeight) : lateMergerBleeds admissible height (p :: chain) binderHeight = true

Consing an admissible position above the binder guarantees bleeding.

theorem Minimalist.top_binder_no_bleed {α : Type u_1} (admissible : α → Bool) (height : α → ℕ) (chain : List α) (binderHeight : ℕ) (h : ∀ p ∈ chain, height p ≤ binderHeight) : lateMergerBleeds admissible height chain binderHeight = false

If every chain position is at or below the binder, late merger cannot bleed Condition C — regardless of which admissibility predicate is used.

theorem Minimalist.no_admissible_no_bleed {α : Type u_1} (admissible : α → Bool) (height : α → ℕ) (chain : List α) (binderHeight : ℕ) (h : ∀ p ∈ chain, admissible p = false) : lateMergerBleeds admissible height chain binderHeight = false

If no chain position is admissible, late merger cannot bleed.

structure Minimalist.ChainPosition : Type

A position on a movement chain. height encodes structural position (higher = larger Nat). caseAvailable records whether case can be assigned at this position (i.e., whether the Case Filter can be satisfied here).

• height : ℕ
• caseAvailable : Bool

def Minimalist.instDecidableEqChainPosition.decEq (x✝ x✝¹ : ChainPosition) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqChainPosition : DecidableEq ChainPosition

Equations

• Minimalist.instDecidableEqChainPosition = Minimalist.instDecidableEqChainPosition.decEq

def Minimalist.instReprChainPosition.repr : ChainPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprChainPosition : Repr ChainPosition

Equations

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

def Minimalist.wlmBleedsCondC (chain : List ChainPosition) (binderHeight : ℕ) : Bool

Wholesale late merger bleeds Condition C iff there exists a position on the movement chain that is (a) strictly above the pronoun binder and (b) a position where case can be assigned.

Case-licensing specialization of lateMergerBleeds.

@cite{gong-2022} condition (2): WLM may bleed Condition C if the movement chain permits a case position higher than the pronoun binder.

Equations

• Minimalist.wlmBleedsCondC chain binderHeight = Minimalist.lateMergerBleeds (fun (x : Minimalist.ChainPosition) => x.caseAvailable) Minimalist.ChainPosition.height chain binderHeight

def Minimalist.wlmForcesReconstruction (chain : List ChainPosition) (binderHeight : ℕ) : Bool

WLM forces Condition C reconstruction when no case position on the chain is above the binder. The NP restrictor must merge at its base position (or at least below the binder), placing the R-expression within the binder's c-command domain.

Equations

• Minimalist.wlmForcesReconstruction chain binderHeight = !Minimalist.wlmBleedsCondC chain binderHeight

def Minimalist.ppAlwaysReconstructs : Bool

PP-scrambling never benefits from WLM: PPs do not contain a determiner with an NP restrictor that can be late-merged. PP-scrambling always exhibits obligatory Condition C reconstruction.

@cite{gong-2022} section 6.2: scrambling of PPs headed by esreg 'against' always forces reconstruction, regardless of the binder's position.

Equations

• Minimalist.ppAlwaysReconstructs = true

theorem Minimalist.top_binder_forces_reconstruction (chain : List ChainPosition) (binderHeight : ℕ) (h : ∀ cp ∈ chain, cp.height ≤ binderHeight) : wlmForcesReconstruction chain binderHeight = true

If every chain position is at or below the binder, WLM forces reconstruction. Specialization of top_binder_no_bleed.

theorem Minimalist.case_above_binder_bleeds (chain : List ChainPosition) (binderHeight h : ℕ) (hgt : h > binderHeight) : wlmBleedsCondC ({ height := h, caseAvailable := true } :: chain) binderHeight = true

A case position above the binder guarantees WLM bleeds Condition C. Specialization of admissible_above_binder_bleeds.

theorem Minimalist.wlm_bleeding_monotone (chain : List ChainPosition) (cp : ChainPosition) (binderHeight : ℕ) (h : wlmBleedsCondC chain binderHeight = true) : wlmBleedsCondC (cp :: chain) binderHeight = true

WLM bleeding is monotone: adding positions never removes it. Specialization of lateMerger_bleeding_monotone.

theorem Minimalist.no_case_forces_reconstruction (chain : List ChainPosition) (binderHeight : ℕ) (h : ∀ cp ∈ chain, cp.caseAvailable = false) : wlmForcesReconstruction chain binderHeight = true

If no chain position has case available, WLM forces reconstruction regardless of heights. Specialization of no_admissible_no_bleed.

def Minimalist.conditionCViolation (root binder rExpr : SyntacticObject) : Bool

Condition C violation check: does the binder c-command the R-expression in tree root?

This is the structural condition checked on concrete SyntacticObject trees, complementing the abstract chain-position analysis in wlmForcesReconstruction.

Equations

• Minimalist.conditionCViolation root binder rExpr = decide (Minimalist.cCommandsIn root binder rExpr)

def Minimalist.conditionCSatisfied (tree binder rExpr : SyntacticObject) : Bool

Condition C is satisfied in a tree: the binder does NOT c-command the R-expression. Takes the tree after any WLM has applied. Returns true when the R-expression is free.

Equations

• Minimalist.conditionCSatisfied tree binder rExpr = !Minimalist.conditionCViolation tree binder rExpr

structure Minimalist.PhaseEdgePosition : Type

A position at a phase edge on a movement chain.

Successive-cyclic movement creates an intermediate copy at each phase edge the mover passes through (@cite{chomsky-2000}). Whether case is available at the edge determines whether WLM can target that position (@cite{gong-2022}).

• phaseCat : Cat
• height : ℕ
• caseAvailable : Bool

@[implicit_reducible]

instance Minimalist.instDecidableEqPhaseEdgePosition : DecidableEq PhaseEdgePosition

Equations

• Minimalist.instDecidableEqPhaseEdgePosition = Minimalist.instDecidableEqPhaseEdgePosition.decEq

def Minimalist.instDecidableEqPhaseEdgePosition.decEq (x✝ x✝¹ : PhaseEdgePosition) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instReprPhaseEdgePosition : Repr PhaseEdgePosition

Equations

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

def Minimalist.instReprPhaseEdgePosition.repr : PhaseEdgePosition → ℕ → Std.Format

Equations

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

def Minimalist.PhaseEdgePosition.toChainPosition (p : PhaseEdgePosition) : ChainPosition

Convert a phase edge position to a chain position for WLM.

Equations

• p.toChainPosition = { height := p.height, caseAvailable := p.caseAvailable }

def Minimalist.successiveCyclicChain (edges : List PhaseEdgePosition) : List ChainPosition

Derive chain positions from successive-cyclic movement through phase edges. Each phase edge the mover passes through becomes a position on the movement chain.

Equations

• Minimalist.successiveCyclicChain edges = List.map Minimalist.PhaseEdgePosition.toChainPosition edges

theorem Minimalist.cp_edge_no_case (h : ℕ) : { phaseCat := Cat.C, height := h, caseAvailable := false }.toChainPosition.caseAvailable = false

CP edges do not provide case positions. C does not assign structural case; it passes tense/agreement features to T via Feature Inheritance (@cite{chomsky-2008}).

def Minimalist.ldsChainTemplate (cpEdgeHeight matrixHeight : ℕ) (matrixCaseAvailable : Bool) : List ChainPosition

LDS chain template: movement from an embedded clause through the CP edge to a matrix clause position. The CP edge provides no case, but the matrix position may — depending on case competitors.

This is the structural template for @cite{gong-2022}'s LDS data: embedded ACC object → Spec,CP (no case) → matrix clause (case depends on whether a dependent case competitor exists).

Equations

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

theorem Minimalist.lds_cp_edge_alone_no_bleed (cpEdgeHeight binderHeight : ℕ) : wlmForcesReconstruction (successiveCyclicChain [{ phaseCat := Cat.C, height := cpEdgeHeight, caseAvailable := false }]) binderHeight = true

A CP edge alone never bleeds Condition C: case is unavailable.

theorem Minimalist.lds_matrix_case_bleeds (cpEdgeHeight matrixHeight binderHeight : ℕ) (h : matrixHeight > binderHeight) : wlmBleedsCondC (ldsChainTemplate cpEdgeHeight matrixHeight true) binderHeight = true

LDS with a matrix case position above the binder bleeds Condition C.

@cite{gong-2022} (41): embedded ACC object scrambled to matrix clause; matrix dative argument is the binder. Dependent ACC is available in the matrix clause (above the binder), so WLM bleeds.