@cite{bruening-alkhalaf-2020} — Category Mismatches in Coordination Revisited

Bruening, Benjamin & Eman Al Khalaf. 2020. Category mismatches in coordination revisited. Linguistic Inquiry 51(1). 1–36.

The Directionality Effect (§3.1)

The linearly closest conjunct to the selecting head must satisfy c-selection. In VO languages (English complement position), this is the first conjunct. In OV languages, or when coordination precedes the verb (English subject position, postpositions), this is the last conjunct.

Two Permitted Violations (§3.2)

Only two genuine category mismatches occur in selection-violating coordination: CP↔NP and non-ly Adverb↔Adjective. Both parallel displacement and ellipsis patterns.

Supercategories (§2)

Apparent category mismatches in predication and modification are not true violations but supercategory selection. become selects Pred (AP, VP, PP); prenominal position selects Mod (AP, AdvP).

Left-to-Right Derivation (§4)

PF and LF are built left-to-right simultaneously. Feature checking at &P proceeds linearly, explaining why the closest conjunct must satisfy selection.

Connection to @cite{schwarzer-2026}

@cite{schwarzer-2026} tests the cross-linguistic prediction using German OV: B&AK predict CP-first for OV complements, but Schwarzer finds DP-first (~77%), supporting bottom-up accounts instead.

inductive BrueningAlKhalaf2020.ConjunctOrder : Type

Preferred order of conjuncts in DP-CP selection-violating coordination.

• dpFirst : ConjunctOrder

  DP conjunct precedes CP conjunct.

• cpFirst : ConjunctOrder

  CP conjunct precedes DP conjunct.

@[implicit_reducible]

instance BrueningAlKhalaf2020.instDecidableEqConjunctOrder : DecidableEq ConjunctOrder

Equations

• BrueningAlKhalaf2020.instDecidableEqConjunctOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BrueningAlKhalaf2020.instReprConjunctOrder.repr : ConjunctOrder → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BrueningAlKhalaf2020.instReprConjunctOrder : Repr ConjunctOrder

Equations

• BrueningAlKhalaf2020.instReprConjunctOrder = { reprPrec := BrueningAlKhalaf2020.instReprConjunctOrder.repr }

def BrueningAlKhalaf2020.instBEqConjunctOrder.beq : ConjunctOrder → ConjunctOrder → Bool

Equations

• BrueningAlKhalaf2020.instBEqConjunctOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance BrueningAlKhalaf2020.instBEqConjunctOrder : BEq ConjunctOrder

Equations

• BrueningAlKhalaf2020.instBEqConjunctOrder = { beq := BrueningAlKhalaf2020.instBEqConjunctOrder.beq }

inductive BrueningAlKhalaf2020.FeaturePercolation : Type

How selectional features percolate through &P to the selecting head.

The competing analyses of selection-violating coordination disagree on a single parameter: which conjunct's categorical features are visible to the selecting head. This parameter determines conjunct order preferences as a function of surface position.

• structural : FeaturePercolation

  Features percolate from the structurally prominent (spec) position. The first conjunct always determines &P's categorical features, regardless of surface position relative to the verb. Analyses: @cite{sag-etal-1985}, @cite{munn-1993}, @cite{peterson-2004}, @cite{zhang-2010}.

• linear : FeaturePercolation

  Features percolate from the linearly closest conjunct to the selecting head. Which conjunct is closest depends on surface position relative to the verb. Analysis: @cite{bruening-alkhalaf-2020}.

@[implicit_reducible]

instance BrueningAlKhalaf2020.instDecidableEqFeaturePercolation : DecidableEq FeaturePercolation

Equations

• BrueningAlKhalaf2020.instDecidableEqFeaturePercolation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BrueningAlKhalaf2020.instReprFeaturePercolation.repr : FeaturePercolation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BrueningAlKhalaf2020.instReprFeaturePercolation : Repr FeaturePercolation

Equations

• BrueningAlKhalaf2020.instReprFeaturePercolation = { reprPrec := BrueningAlKhalaf2020.instReprFeaturePercolation.repr }

def BrueningAlKhalaf2020.instBEqFeaturePercolation.beq : FeaturePercolation → FeaturePercolation → Bool

Equations

• BrueningAlKhalaf2020.instBEqFeaturePercolation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance BrueningAlKhalaf2020.instBEqFeaturePercolation : BEq FeaturePercolation

Equations

• BrueningAlKhalaf2020.instBEqFeaturePercolation = { beq := BrueningAlKhalaf2020.instBEqFeaturePercolation.beq }

def BrueningAlKhalaf2020.predictOrder (fp : FeaturePercolation) (pos : Typology.WordOrder.VerbPosition) : ConjunctOrder

Derive conjunct order preference from feature percolation mechanism.

The core principle: the conjunct whose features percolate to &P must satisfy c-selection (= must be the DP). The percolation mechanism determines which conjunct that is:

• Structural: spec (= first conjunct) → always DP-first
• Linear: closest to V → DP-first postverbally, CP-first preverbally

Equations

• BrueningAlKhalaf2020.predictOrder BrueningAlKhalaf2020.FeaturePercolation.structural pos = BrueningAlKhalaf2020.ConjunctOrder.dpFirst
• BrueningAlKhalaf2020.predictOrder BrueningAlKhalaf2020.FeaturePercolation.linear Typology.WordOrder.VerbPosition.postverbal = BrueningAlKhalaf2020.ConjunctOrder.dpFirst
• BrueningAlKhalaf2020.predictOrder BrueningAlKhalaf2020.FeaturePercolation.linear Typology.WordOrder.VerbPosition.preverbal = BrueningAlKhalaf2020.ConjunctOrder.cpFirst

theorem BrueningAlKhalaf2020.structural_position_invariant (pos₁ pos₂ : Typology.WordOrder.VerbPosition) : predictOrder FeaturePercolation.structural pos₁ = predictOrder FeaturePercolation.structural pos₂

Structural percolation is position-invariant: the structurally prominent conjunct is always first, regardless of surface order.

theorem BrueningAlKhalaf2020.linear_position_dependent : predictOrder FeaturePercolation.linear Typology.WordOrder.VerbPosition.preverbal ≠ predictOrder FeaturePercolation.linear Typology.WordOrder.VerbPosition.postverbal

Linear percolation is position-dependent: preverbal and postverbal yield different predictions.

theorem BrueningAlKhalaf2020.percolation_agrees_postverbal : predictOrder FeaturePercolation.structural Typology.WordOrder.VerbPosition.postverbal = predictOrder FeaturePercolation.linear Typology.WordOrder.VerbPosition.postverbal

The two percolation mechanisms agree in postverbal position: both predict DP-first when V precedes the coordination.

theorem BrueningAlKhalaf2020.percolation_diverges_preverbal : predictOrder FeaturePercolation.structural Typology.WordOrder.VerbPosition.preverbal ≠ predictOrder FeaturePercolation.linear Typology.WordOrder.VerbPosition.preverbal

The two percolation mechanisms diverge in preverbal position: structural predicts DP-first, linear predicts CP-first. This is the configuration that empirically distinguishes the accounts.

def BrueningAlKhalaf2020.linearClosenessPrediction : Typology.WordOrder.VerbPosition → ConjunctOrder

Linear closeness prediction (B&AK's core claim, §3.1): the linearly closest conjunct to the selecting head must satisfy c-selection.

In VO complement position: V [&P X and Y] → X is closest → DP-first. In OV complement position: [&P X and Y] V → Y is closest → CP-first (so DP is last, verb-adjacent).

This also applies to English subject position (preverbal even in VO) and postpositions (selecting head follows coordination).

Derived from predictOrder with linear percolation.

Equations

• BrueningAlKhalaf2020.linearClosenessPrediction = BrueningAlKhalaf2020.predictOrder BrueningAlKhalaf2020.FeaturePercolation.linear

def BrueningAlKhalaf2020.bottomUpPrediction : Typology.WordOrder.VerbPosition → ConjunctOrder

Bottom-up prediction (competitor account, §3.1): asymmetric &P structure makes the first conjunct structurally more prominent. The selected DP must be first, regardless of surface position relative to the verb.

Analyses: @cite{sag-etal-1985}, @cite{munn-1993}, @cite{peterson-2004}, @cite{zhang-2010}.

Derived from predictOrder with structural percolation.

Equations

• BrueningAlKhalaf2020.bottomUpPrediction = BrueningAlKhalaf2020.predictOrder BrueningAlKhalaf2020.FeaturePercolation.structural

inductive BrueningAlKhalaf2020.SelectionViolationType : Type

B&AK identify exactly two category mismatches that are permitted in selection-violating coordination (§3.2).

These parallel the categories that allow displacement and ellipsis:

1. CP↔NP: CPs can appear in NP positions (also seen in topicalization, pseudoclefts, "do so" replacement)
2. Non-ly Adv↔Adj: manner adverbs without -ly can appear in adjective positions (also seen in prenominal modification)

• cpAsNp : SelectionViolationType

  CP appearing in an NP-selecting position.

• advAsAdj : SelectionViolationType

  Non-ly adverb appearing in an adjective position.

@[implicit_reducible]

instance BrueningAlKhalaf2020.instDecidableEqSelectionViolationType : DecidableEq SelectionViolationType

Equations

• BrueningAlKhalaf2020.instDecidableEqSelectionViolationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BrueningAlKhalaf2020.instReprSelectionViolationType : Repr SelectionViolationType

Equations

• BrueningAlKhalaf2020.instReprSelectionViolationType = { reprPrec := BrueningAlKhalaf2020.instReprSelectionViolationType.repr }

def BrueningAlKhalaf2020.instReprSelectionViolationType.repr : SelectionViolationType → ℕ → Std.Format

Equations

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

def BrueningAlKhalaf2020.permittedViolations : List SelectionViolationType

The exhaustive list of permitted violations, justified structurally by coordExtension_exhaustive (§ 7): only CP and AdvP have non-empty extensions. See violation_from_extension and extension_to_violation (§ 7) for the bidirectional correspondence.

Equations

• BrueningAlKhalaf2020.permittedViolations = [BrueningAlKhalaf2020.SelectionViolationType.cpAsNp, BrueningAlKhalaf2020.SelectionViolationType.advAsAdj]

theorem BrueningAlKhalaf2020.exactly_two_violations : permittedViolations.length = 2

theorem BrueningAlKhalaf2020.english_is_vo : Fragments.English.wordOrder.ovOrder = Typology.WordOrder.OVOrder.vo

English is VO: complements follow the selecting verb.

theorem BrueningAlKhalaf2020.english_complement_postverbal : Fragments.English.wordOrder.ovOrder.verbPosition = some Typology.WordOrder.VerbPosition.postverbal

English complement position maps to postverbal.

theorem BrueningAlKhalaf2020.bak_english_complement : linearClosenessPrediction Typology.WordOrder.VerbPosition.postverbal = ConjunctOrder.dpFirst

B&AK predict DP-first in English complement position: the first conjunct is closest to V.

You can depend on [DP my assistant] and [CP that he will be on time]. ✓

@cite{sag-etal-1985} ex. (3a), @cite{bruening-alkhalaf-2020} §3.1.

theorem BrueningAlKhalaf2020.accounts_agree_complement : linearClosenessPrediction Typology.WordOrder.VerbPosition.postverbal = bottomUpPrediction Typology.WordOrder.VerbPosition.postverbal

Bottom-up also predicts DP-first for English VO complements. Both accounts agree for this configuration.

B&AK's strongest within-English evidence for closeness over first-conjunct (§3.1, examples (41a/b)):

(41a) [CP That he had been gambling with public funds] and [DP the fact that he had been keeping a mistress] resulted in his being dismissed. ✓

(41b) *[DP The fact that he had been keeping a mistress] and [CP that he had been gambling with public funds] resulted in his being dismissed. ✗

When coordination is in subject position, it precedes the verb even in English VO. The LAST conjunct is closest to V. B&AK predict the DP must be last (closest), giving CP-first order. Bottom-up accounts predict DP-first regardless — wrong for this configuration.

theorem BrueningAlKhalaf2020.bak_subject_cpfirst : linearClosenessPrediction Typology.WordOrder.VerbPosition.preverbal = ConjunctOrder.cpFirst

B&AK predict CP-first in subject position: the last conjunct is closest to V, so the DP must be last.

theorem BrueningAlKhalaf2020.bottomUp_subject_dpfirst : bottomUpPrediction Typology.WordOrder.VerbPosition.preverbal = ConjunctOrder.dpFirst

Bottom-up predicts DP-first even in subject position.

theorem BrueningAlKhalaf2020.subject_position_distinguishes : linearClosenessPrediction Typology.WordOrder.VerbPosition.preverbal ≠ bottomUpPrediction Typology.WordOrder.VerbPosition.preverbal

Subject position distinguishes the two accounts within a single language (English). B&AK argue this is decisive evidence for closeness over structural prominence.

theorem BrueningAlKhalaf2020.bak_predicts_cpfirst_ov : Option.map linearClosenessPrediction Typology.WordOrder.OVOrder.ov.verbPosition = some ConjunctOrder.cpFirst

For OV languages, B&AK predict CP-first: complements precede V, so the last conjunct is closest. The DP must be last → CP-first.

theorem BrueningAlKhalaf2020.bak_predicts_dpfirst_vo : Option.map linearClosenessPrediction Typology.WordOrder.OVOrder.vo.verbPosition = some ConjunctOrder.dpFirst

For VO languages, B&AK predict DP-first.

theorem BrueningAlKhalaf2020.ov_predictions_diverge : Option.map linearClosenessPrediction Typology.WordOrder.OVOrder.ov.verbPosition ≠ Option.map bottomUpPrediction Typology.WordOrder.OVOrder.ov.verbPosition

OV is the cross-linguistic test case. Bottom-up and B&AK diverge on OV complement order.

@cite{schwarzer-2026} tests this with German and finds DP-first (~77%), supporting bottom-up over B&AK for OV complement position.

inductive BrueningAlKhalaf2020.Supercategory : Type

B&AK's supercategory features unify apparent category mismatches that are not true selection violations.

Pred: AP, VP, PP can all serve as predicates. Verbs like become select Pred, not a specific lexical category.

Mod: AP, AdvP can both modify. Prenominal position selects Mod, not specifically Adj.

• pred : Supercategory

  Predicative: AP, VP, PP can all serve as predicates.

• mod : Supercategory

  Modifier: AP, AdvP can both serve as modifiers.

@[implicit_reducible]

instance BrueningAlKhalaf2020.instDecidableEqSupercategory : DecidableEq Supercategory

Equations

• BrueningAlKhalaf2020.instDecidableEqSupercategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BrueningAlKhalaf2020.instReprSupercategory.repr : Supercategory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BrueningAlKhalaf2020.instReprSupercategory : Repr Supercategory

Equations

• BrueningAlKhalaf2020.instReprSupercategory = { reprPrec := BrueningAlKhalaf2020.instReprSupercategory.repr }

def BrueningAlKhalaf2020.Supercategory.cats : Supercategory → Finset Core.Tree.Cat

Categories belonging to each supercategory, grounded in the Cat category system from Core.Tree. The inclusion order on Finset Cat gives the lattice structure: Supercategory.cats .pred and Supercategory.cats .mod are elements ordered by ⊆.

Equations

• BrueningAlKhalaf2020.Supercategory.pred.cats = {Core.Tree.Cat.VP, Core.Tree.Cat.AdjP, Core.Tree.Cat.PP}
• BrueningAlKhalaf2020.Supercategory.mod.cats = {Core.Tree.Cat.AdjP, Core.Tree.Cat.AdvP}

theorem BrueningAlKhalaf2020.adjp_in_pred : Core.Tree.Cat.AdjP ∈ Supercategory.pred.cats

AP belongs to both supercategories.

theorem BrueningAlKhalaf2020.adjp_in_mod : Core.Tree.Cat.AdjP ∈ Supercategory.mod.cats

theorem BrueningAlKhalaf2020.supercats_overlap : Supercategory.pred.cats ∩ Supercategory.mod.cats = {Core.Tree.Cat.AdjP}

Pred and Mod overlap at exactly AP.

def BrueningAlKhalaf2020.coordExtension : Core.Tree.Cat → Finset Core.Tree.Cat

Extended distributional compatibility for coordination (§3.2). Categories that c can appear as in non-coordination contexts (displacement, ellipsis), beyond its native category.

• CP → NP: CPs can be topicalized, pseudoclefted, and pro-form replaced — NP-like distributional properties
• AdvP → AdjP: non-ly adverbs appear prenominally — AdjP-like distributional properties

All other categories have no extended compatibility. Combined with Supercategory.cats, this derives B&AK's "exactly two permitted violations" (§3.2).

Equations

• BrueningAlKhalaf2020.coordExtension Core.Tree.Cat.CP = {Core.Tree.Cat.NP}
• BrueningAlKhalaf2020.coordExtension (Core.Tree.Cat.proj UD.UPOS.ADV) = {Core.Tree.Cat.AdjP}
• BrueningAlKhalaf2020.coordExtension x✝ = ∅

theorem BrueningAlKhalaf2020.cp_extends_np : Core.Tree.Cat.NP ∈ coordExtension Core.Tree.Cat.CP

CP extends to NP positions.

theorem BrueningAlKhalaf2020.advp_extends_adjp : Core.Tree.Cat.AdjP ∈ coordExtension (Core.Tree.Cat.proj UD.UPOS.ADV)

AdvP extends to AdjP positions.

theorem BrueningAlKhalaf2020.coordExtension_exhaustive (c : Core.Tree.Cat) : coordExtension c ≠ ∅ → c = Core.Tree.Cat.CP ∨ c = Core.Tree.Cat.AdvP

Only CP and AdvP have non-empty coordination extensions. This structurally derives B&AK's "exactly two permitted violations" (§3.2) from distributional profiles rather than stipulating them as a list.

def BrueningAlKhalaf2020.SelectionViolationType.cats : SelectionViolationType → Core.Tree.Cat × Core.Tree.Cat

Map each violation type to its source and target categories. The source category can appear in a position selecting the target via coordination.

Equations

• BrueningAlKhalaf2020.SelectionViolationType.cpAsNp.cats = (Core.Tree.Cat.CP, Core.Tree.Cat.NP)
• BrueningAlKhalaf2020.SelectionViolationType.advAsAdj.cats = (Core.Tree.Cat.AdvP, Core.Tree.Cat.AdjP)

theorem BrueningAlKhalaf2020.violation_from_extension (v : SelectionViolationType) : v.cats.2 ∈ coordExtension v.cats.1

Each permitted violation corresponds to a non-empty coordExtension: the target category appears in the extension of the source.

theorem BrueningAlKhalaf2020.extension_to_violation (c : Core.Tree.Cat) (h : coordExtension c ≠ ∅) : ∃ (v : SelectionViolationType), v.cats.1 = c

Every non-empty coordExtension corresponds to a permitted violation. This, together with violation_from_extension, establishes a bijection between SelectionViolationType and non-empty extensions, proving the enumeration is not stipulated but derived from distributional profiles.

B&AK's derivation model (§4) builds structure left-to-right, with PF and LF computed simultaneously. Feature checking at &P uses the linearly closest conjunct. The model posits null syntactic heads (null N dominating CP, null Adv head) to mediate the two permitted violations.

Crucially, B&AK accept asymmetric &P structure — the same assumption as bottom-up accounts. The disagreement is about the mechanism: closeness (B&AK) vs structural prominence (bottom-up). Both theories accept CoordSymmetry.asymmetric, but derive different predictions from it:

• B&AK: closeness → predictions depend on surface position
• Bottom-up: structural prominence → predictions are position-invariant

def BrueningAlKhalaf2020.mergeCoordSymmetry : Features.Coordination.CoordSymmetry

Coordination structure as adopted by both B&AK and the bottom-up accounts is asymmetric: the first conjunct (specifier) is treated as structurally more prominent than the second (complement).

Both accounts accept this asymmetry (§4) and disagree only about the mechanism that derives downstream predictions from it (linear closeness vs structural prominence).

Substrate note (post-MCB Phase 1.0). Under @cite{marcolli-chomsky-berwick-2025} Definition 1.1.1 (book p. 22)

• Remark 1.1.2 (p. 23), syntactic objects are the free, non-associative, commutative magma over SO_0 — merge x y and merge y x are strictly equal on the quotient (mul_comm is a strict equality, not just an isomorphism).

B&AK's account survives nonplanar Merge cleanly. Their headline closeness mechanism (§3.1, §4) is PF-side / linear-order-side: "the closest conjunct at PF wins" is built simultaneously with LF in the Left-to-Right Derivation, with feature checking at &P proceeding linearly, not from Merge structure. The linear FeaturePercolation mode in this file is in fact pure-Externalization — exactly what nonplanar Merge wants. The (now-stipulated) mergeCoordSymmetry := .asymmetric is an assumption B&AK also make (asymmetric &P structure), independent of Merge symmetry.

The bottom-up alternatives (Munn 1993, Zhang 2010, Citko 2011 — Symmetry in Syntax) are the accounts whose status is genuinely affected. They depend on hierarchical asymmetry within &P, which nonplanar Merge does not provide. Such accounts now require either (i) hierarchical asymmetry from a stipulated Coord head, or (ii) re-derivation of asymmetry from LCA + head-directionality (MCB §1.13). Citko 2011 in particular makes the case that coordination is the prototype of symmetric merge (multidominance); that view aligns with MCB but is incompatible with the bottom-up structural-prominence approach.

Equations

• BrueningAlKhalaf2020.mergeCoordSymmetry = Features.Coordination.CoordSymmetry.asymmetric

theorem BrueningAlKhalaf2020.closeness_is_position_dependent : linearClosenessPrediction Typology.WordOrder.VerbPosition.preverbal ≠ linearClosenessPrediction Typology.WordOrder.VerbPosition.postverbal

Despite assuming asymmetric structure, B&AK's closeness prediction is position-DEPENDENT: preverbal and postverbal yield different orders.

theorem BrueningAlKhalaf2020.bottomUp_is_position_invariant : bottomUpPrediction Typology.WordOrder.VerbPosition.preverbal = bottomUpPrediction Typology.WordOrder.VerbPosition.postverbal

Bottom-up accounts derive position-INVARIANT predictions from the same asymmetric structure: always DP-first.

def BrueningAlKhalaf2020.FeaturePercolation.requiredSymmetry : FeaturePercolation → Option Features.Coordination.CoordSymmetry

Structural percolation presupposes asymmetric coordination: there must be a structurally prominent (spec) position for features to percolate from. Linear percolation requires no particular structural assumption — closeness is defined over surface strings, not tree structure.

Equations

• BrueningAlKhalaf2020.FeaturePercolation.structural.requiredSymmetry = some Features.Coordination.CoordSymmetry.asymmetric
• BrueningAlKhalaf2020.FeaturePercolation.linear.requiredSymmetry = none

theorem BrueningAlKhalaf2020.structural_requires_asymmetric : FeaturePercolation.structural.requiredSymmetry = some mergeCoordSymmetry ∧ FeaturePercolation.linear.requiredSymmetry = none

Both accounts adopt asymmetric structure, but only the bottom-up account's predictions require it. B&AK's closeness mechanism would make the same predictions under symmetric structure.

theorem BrueningAlKhalaf2020.merge_is_symmetric (x y : Minimalist.SyntacticObject) : Minimalist.merge x y = Minimalist.merge y x

Merge is symmetric on the SO carrier. Under MCB nonplanar SOs (@cite{marcolli-chomsky-berwick-2025} Def 1.1.1, Remark 1.1.2), merge x y = merge y x is a strict equality. This was not the case under the prior planar TraceTree carrier — the earlier version of this file proved a merge_distinguishes_children theorem (merge x y ≠ merge y x for distinct x, y) by injection. That theorem is now provably false: merge is (· * ·) on FreeCommMagma _, which the CommMagma instance proves commutative.

The change is consequential for Bruening's argument: the "first vs second conjunct" asymmetry can no longer be grounded in Merge structure (which is the original Bruening-style derivation). The asymmetry survives only as a stipulation on the Coord head or as a downstream consequence of Externalization (LCA / head directionality / linearization). See mergeCoordSymmetry's substrate note.

theorem BrueningAlKhalaf2020.stipulated_symmetry_matches_percolation : FeaturePercolation.structural.requiredSymmetry = some mergeCoordSymmetry

Stipulation: structural percolation's required-symmetry hypothesis matches the stipulated mergeCoordSymmetry. Trivially true since both are .asymmetric by stipulation; this lemma exists to make the dependency explicit at the type level rather than load-bearing on Merge's structure.

theorem BrueningAlKhalaf2020.prediction_chain_from_stipulation (pos : Typology.WordOrder.VerbPosition) : mergeCoordSymmetry = Features.Coordination.CoordSymmetry.asymmetric ∧ FeaturePercolation.structural.requiredSymmetry = some mergeCoordSymmetry ∧ predictOrder FeaturePercolation.structural pos = ConjunctOrder.dpFirst

The downstream chain from Coord-asymmetry to bottom-up prediction:

1. mergeCoordSymmetry := .asymmetric (STIPULATION — see substrate note)
2. Structural percolation's presupposition is met by stipulation (stipulated_symmetry_matches_percolation)
3. predictOrder .structural yields position-invariant DP-first

Substrate note (post-MCB Phase 1.0). This was previously merge_grounds_prediction, which claimed (1) was derived from Merge structure rather than stipulated. Under MCB nonplanar Merge (merge_is_symmetric headline) that derivation does not run.

The downstream prediction (predictOrder .structural pos = .dpFirst) is the bottom-up (structural prominence) variant — it requires the asymmetry stipulation. B&AK's own headline (linear closeness) does not require it: their linear mode would predict from PF position alone. So the stipulation is load-bearing only for the alternative account this file also formalizes (Munn 1993 / Zhang 2010 / @cite{citko-2011}-style structural prominence), not for B&AK's own.

B&AK extend the closeness analysis to postpositions (§3.1, examples (43a/b)). When the selecting head is a postposition (e.g., notwithstanding), the coordination precedes it. The LAST conjunct is closest, so it must satisfy selection (= be DP). This gives CP-first order, just as in subject position and OV complements.

Formally, the postposition case reduces to VerbPosition.preverbal: coordination precedes the selecting head, making it structurally identical to subject position (cf. bak_subject_cpfirst).