def Minimalist.immediatelyCCommands (x y root : SyntacticObject) : Prop

X immediately c-commands Y within tree root iff X c-commands Y (in root) and there is no Z such that X c-commands Z and Z c-commands Y (in root).

This is the "closest" c-command relation, used to define amalgamation locality (HMC compliance).

Equations

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

structure Minimalist.Amalgamation : Type

An amalgamation of two heads at PF (@cite{harizanov-gribanova-2019}).

Amalgamation forms a complex morphological word from two adjacent heads via PF affixation. Since affixation requires adjacency, amalgamation is strictly local and cannot skip intervening heads (HMC compliance).

Example: French V-to-T in Jean ne parlait pas français — V amalgamates with T at PF.

NB: This is NOT MCB-Merge content. Amalgamation lives in the PF layer (per @cite{marcolli-larson-huijbregts-2025} §4.1). It is distinct from Step.im, which is narrow-syntactic Internal Merge of a head leaf (e.g., Bulgarian LHM).

• target : SyntacticObject

  The element that amalgamates (the "target").

• host : SyntacticObject

  The host (what it amalgamates to).

• is_local (root : SyntacticObject) : immediatelyCCommands self.host self.target root

  Amalgamation is LOCAL: host immediately c-commands target. Defining property that distinguishes amalgamation from narrow-syntactic head movement (which can skip intervening heads, e.g., Bulgarian LHM, Germanic V2).

theorem Minimalist.amalgamation_no_intervener (a : Amalgamation) (root : SyntacticObject) : ¬∃ (z : SyntacticObject), z ≠ a.host ∧ z ≠ a.target ∧ cCommandsIn root a.host z ∧ cCommandsIn root z a.target

Amalgamation cannot skip intervening elements (@cite{harizanov-gribanova-2019} §3.3, p.15: "Amalgamation-based displacement obeys the Head Movement Constraint"). Immediate from the definition: is_local requires no intervener.

theorem Minimalist.intervener_rules_out_amalgamation (host target intervener root : SyntacticObject) (h_neq_host : intervener ≠ host) (h_neq_target : intervener ≠ target) (h_host_cmd : cCommandsIn root host intervener) (h_int_cmd : cCommandsIn root intervener target) : ¬∃ (a : Amalgamation), a.host = host ∧ a.target = target

If there's an intervening element, the displacement cannot be amalgamation. Diagnostic: a head displacement that skips an intervening head must be syntactic (= Step.im), not amalgamation.

theorem Minimalist.amalgamation_host_ccommands_target (a : Amalgamation) (root : SyntacticObject) : cCommandsIn root a.host a.target

Amalgamation respects locality: the host c-commands the target.

def Minimalist.VerbDoublingIsSyntacticIn (d : Derivation) (x : SyntacticObject) : Prop

"x underwent syntactic Internal Merge in derivation d" — MCB-aligned via Derivation.movedItems.

Per @cite{marcolli-chomsky-berwick-2025} §1.4.3.1, IM is the syntactic mechanism that produces surface verb doubling via PF copy/trace pronunciation rules: the verb appears once in the syntactic tree (with its deeper copy replaced by mkTrace), but PF rules pronounce both positions in certain constructions.

A construction's verb-doubling is "syntactic" iff the analyst can exhibit a Derivation where the verb appears as the mover of a Step.im step. Russian (@cite{harizanov-gribanova-2019}) and Guébie (@cite{sande-clem-dabkowski-2026}) license positive instances; Hebrew (@cite{landau-2006}) is argued to be PF-driven instead.

Decidable for any concrete Derivation.

Migration note: previously lived in Phenomena/WordOrder/Studies/ HarizanovGribanova2019Amalgamation.lean, which was deleted at 0.230.X. The relational-predicate substrate from that file (covers, coversAmongHeads, coversProjection, isMaximalProjectionOf, containsAmongHeads, headsIn, HeadDisplacement, etc.) was tied to the deleted legacy getCategory/isHeadIn/sameLabel/isMaximalIn API. A future rewrite will rebuild HG2019's amalgamation-as-covering analysis on top of the MCB-native Minimalist.Labeling.isMaximalAt h / isHeadIn h predicates.

Equations

• Minimalist.VerbDoublingIsSyntacticIn d x = (x ∈ d.movedItems)

@[implicit_reducible]

instance Minimalist.instDecidableVerbDoublingIsSyntacticIn (d : Derivation) (x : SyntacticObject) : Decidable (VerbDoublingIsSyntacticIn d x)

Equations

• Minimalist.instDecidableVerbDoublingIsSyntacticIn d x = id inferInstance