Sande, Clem & Dąbkowski 2026: discontinuous vowel harmony in Guébie

[SCD26]: in Guébie particle-verb focus constructions, the fronted particle harmonizes in ATR with the clause-final verb across intervening harmony-eligible words (their (24)). The analysis: harmony is strictly local at vP Spell-out, and later A′-movement separates target from trigger — spelled-out material staying accessible to later syntax (§6.2, via [FP05]'s Cyclic Linearization). Everything below is derived from the two §4 parameters (Aux blocking V-to-T, remnant fronting) rather than stipulated; the empirical core is their (44): harmony iff V is spelled out inside vP.

Main definitions

• ClauseConfig, WordOrder: the §4 parameters and the four attested settings, with derived Spell-outs ((45)/(48)) and surface strings ((31)–(34)).
• ClauseConfig.harmony, surfaceATR, harmonyTableau: trigger-locality (§6.1), the particle's surface value ((12)–(13)), and the (46)/(47) ranking as a tableau.
• FrozenATR, guebiePICMode: the per-cycle harmony record (§6.1) and the PIC stance (§6.2).
• guebiePredicateDoubling: the §3 movement witnesses.
• HarmonyProfile, WolofShape: the §7 prediction schema — trigger and target co-spelled-out low, movement after — instantiated by Guébie and Wolof.

Main results

• harmony_eq_hasAux, discontinuous_harmony: the (44) correlation derived; harmony without surface adjacency.
• all_clauses_consistent, nonedge_particle_fronting_crashes: every setting linearizes; the §6.2 escape-hatch counterfactual crashes.
• optimal_eq_surfaceATR, PartSAuxOV_atr_persists_through_fronting: the ranking derives the surface value, and it survives the CP cycle.
• guebie_VDIS_positive_instance: doubling is narrow-syntactic ((25)–(30), contra [Lan06]).
• guebie_profile, wolof_profile, wolof_discontinuous: both languages instantiate the §7 schema ([Sy05], [Mar19]).

Implementation notes

Spell-out snapshots are List String labels, as in Studies/FoxPesetsky2005.lean. The paper deems the harmony implementation "not crucial" ([San19]'s (46)/(47) in [Han14]'s Agreement by Projection); harmonyTableau renders only the ranking. §5's rejected phonological approaches ([CS82a], [Gaf98], [RW04a]) are formalized in Studies/Sagey1986.lean, Studies/RoseWalker2004.lean, Studies/Hansson2010.lean. TODO: the Atchan parallel ((51), Katherine Russell p.c., [Rus23]) awaits movement diagnostics; the paper leaves it open and so do we.

The ATR feature ([SCD26] (1))

Guébie has a ten-vowel system, +ATR ə e i o u vs. −ATR a ɛ ɪ ɔ ʊ, harmonizing as a binary feature; affixes and particles agree with the verb root when both are inside the same Spell-out domain. Only the per-terminal binary value matters here.

@[reducible, inline]

abbrev SandeClemDabkowski2026.ATR : Type

The tongue-root feature value (Phonology.TongueRoot.ATR).

Equations

• SandeClemDabkowski2026.ATR = Phonology.TongueRoot.ATR

def SandeClemDabkowski2026.particleDefaultATR : ATR

The particle's lexical default, surfacing when no harmony trigger is local ((13)). Defaults are lexical per particle ((12)); we model the /jɔkʊ/ type, derived from the fragment lexicon (Fragments/Guebie/ParticleVerbs.lean).

Equations

• SandeClemDabkowski2026.particleDefaultATR = Guebie.jOkU.atr

The §4 syntax: two parameters derive the four orders

structure SandeClemDabkowski2026.ClauseConfig : Type

The two parameters of [SCD26] §4's predicate-fronting analysis: an auxiliary in T blocks V-to-T ((32)/(34)), and the remnant VP (containing the particle) may front to Spec,CP ((33)/(34)).

• hasAux : Bool
• fronted : Bool

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableEqClauseConfig : DecidableEq ClauseConfig

Equations

• SandeClemDabkowski2026.instDecidableEqClauseConfig = SandeClemDabkowski2026.instDecidableEqClauseConfig.decEq

def SandeClemDabkowski2026.instDecidableEqClauseConfig.decEq (x✝ x✝¹ : ClauseConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instReprClauseConfig : Repr ClauseConfig

Equations

• SandeClemDabkowski2026.instReprClauseConfig = { reprPrec := SandeClemDabkowski2026.instReprClauseConfig.repr }

def SandeClemDabkowski2026.instReprClauseConfig.repr : ClauseConfig → ℕ → Std.Format

Equations

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

def SandeClemDabkowski2026.ClauseConfig.verbInVP (c : ClauseConfig) : Bool

V stays in v — hence inside the vP Spell-out — iff Aux occupies T (§4.1).

Equations

• c.verbInVP = c.hasAux

def SandeClemDabkowski2026.ClauseConfig.vPSpellOut (c : ClauseConfig) : List String

Overt terminals spelled out within vP ((45)/(48)): the particle, plus V iff it has not raised past v. The object has independently shifted out.

Equations

• c.vPSpellOut = "Part" :: if c.verbInVP = true then ["V"] else []

def SandeClemDabkowski2026.ClauseConfig.surfaceOrder (c : ClauseConfig) : List String

The surface clause, derived compositionally ((31)–(34)): fronted particle, subject, T-material, object, in-situ particle, clause-final verb.

Equations

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

def SandeClemDabkowski2026.ClauseConfig.derivation (c : ClauseConfig) : List (List String)

The two-phase Cyclic-Linearization derivation: vP Spell-out, then the full surface clause ([FP05]'s final Linearize). Previously-spelled-out terminals recur, so Order Preservation is what makes consistency contentful.

Equations

• c.derivation = [c.vPSpellOut, c.surfaceOrder]

inductive SandeClemDabkowski2026.WordOrder : Type

The four attested word orders as parameter settings ([SCD26] (44)).

• SVOPart : WordOrder

  S V O Part: V moves to T; Part stays in vP, clause-final.

• SAuxOPartV : WordOrder

  S Aux O Part V: Aux occupies T, V stays in v; V and Part both in vP.

• PartSVO : WordOrder

  Part S V O: V moves to T; the remnant VP (just Part) fronts to Spec,CP.

• PartSAuxOV : WordOrder

  Part S Aux O V: V stays in v; the remnant VP (just Part) fronts.

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableEqWordOrder : DecidableEq WordOrder

Equations

• SandeClemDabkowski2026.instDecidableEqWordOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SandeClemDabkowski2026.instReprWordOrder.repr : WordOrder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instReprWordOrder : Repr WordOrder

Equations

• SandeClemDabkowski2026.instReprWordOrder = { reprPrec := SandeClemDabkowski2026.instReprWordOrder.repr }

def SandeClemDabkowski2026.WordOrder.config : WordOrder → ClauseConfig

The parameter settings behind the four orders ((31)–(34)).

Equations

• SandeClemDabkowski2026.WordOrder.SVOPart.config = { hasAux := false, fronted := false }
• SandeClemDabkowski2026.WordOrder.SAuxOPartV.config = { hasAux := true, fronted := false }
• SandeClemDabkowski2026.WordOrder.PartSVO.config = { hasAux := false, fronted := true }
• SandeClemDabkowski2026.WordOrder.PartSAuxOV.config = { hasAux := true, fronted := true }

theorem SandeClemDabkowski2026.surfaceOrder_attested : WordOrder.SVOPart.config.surfaceOrder = ["S", "V", "O", "Part"] ∧ WordOrder.SAuxOPartV.config.surfaceOrder = ["S", "Aux", "O", "Part", "V"] ∧ WordOrder.PartSVO.config.surfaceOrder = ["Part", "S", "V", "O"] ∧ WordOrder.PartSAuxOV.config.surfaceOrder = ["Part", "S", "Aux", "O", "V"]

The derived surface strings are the attested orders.

Consistency: every setting linearizes; non-edge fronting would not

theorem SandeClemDabkowski2026.all_clauses_consistent (aux fronted : Bool) : Minimalist.Linearization.Consistent { hasAux := aux, fronted := fronted }.derivation

Every parameter setting linearizes consistently.

theorem SandeClemDabkowski2026.nonedge_particle_fronting_crashes : ¬Minimalist.Linearization.Consistent [["V", "Part"], ["Part", "S", "Aux", "O", "V"]]

The §6.2 escape-hatch argument: the particle can front because it is "the leftmost overt element in the vP phase upon spell-out". A counterfactual vP spelling the particle out to the right of V could not front it without an ordering cycle.

The (44) correlation, derived

def SandeClemDabkowski2026.ClauseConfig.harmony (c : ClauseConfig) : Bool

Harmony applies iff the trigger V is spelled out within vP (§6.1).

Equations

• c.harmony = c.vPSpellOut.contains "V"

theorem SandeClemDabkowski2026.harmony_eq_hasAux (aux fronted : Bool) : { hasAux := aux, fronted := fronted }.harmony = aux

The (44) correlation derived from the syntax: harmony iff Aux blocks V-to-T.

theorem SandeClemDabkowski2026.harmony_independent_of_fronting (aux f₁ f₂ : Bool) : { hasAux := aux, fronted := f₁ }.harmony = { hasAux := aux, fronted := f₂ }.harmony

Fronting is irrelevant to harmony — the discontinuity is purely a surface effect of later movement.

theorem SandeClemDabkowski2026.discontinuous_harmony : { hasAux := true, fronted := true }.harmony = true ∧ ¬(["Part", "V"] <:+: { hasAux := true, fronted := true }.surfaceOrder ∨ ["V", "Part"] <:+: { hasAux := true, fronted := true }.surfaceOrder)

Discontinuity as a theorem: in the fronted SAuxOV clause, particle and verb are not surface-adjacent in either order, yet harmony applies ((24)).

def SandeClemDabkowski2026.surfaceATR (c : ClauseConfig) (vRoot : ATR) : ATR

The particle's surface ATR: the verb root's value under harmony ((12)), its lexical default otherwise ((13)).

Equations

• SandeClemDabkowski2026.surfaceATR c vRoot = if c.harmony = true then vRoot else SandeClemDabkowski2026.particleDefaultATR

§6.1's mechanism: the (46)/(47) ranking derives the surface value

The paper implements local harmony as [San19]'s constraints in [Han14]'s Agreement by Projection, ranked ATRHARM ≫ IDENT-IO(ATR) within the vP domain; the winner harmonizes exactly when a trigger is local.

structure SandeClemDabkowski2026.HarmonyCand : Type

An output candidate for the particle at vP Spell-out: lexical input value, domain-local trigger (the verb root, when V is in the domain), and output.

• lexical : ATR
• trigger : Option ATR
• out : ATR

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableEqHarmonyCand : DecidableEq HarmonyCand

Equations

• SandeClemDabkowski2026.instDecidableEqHarmonyCand = SandeClemDabkowski2026.instDecidableEqHarmonyCand.decEq

def SandeClemDabkowski2026.instDecidableEqHarmonyCand.decEq (x✝ x✝¹ : HarmonyCand) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instReprHarmonyCand : Repr HarmonyCand

Equations

• SandeClemDabkowski2026.instReprHarmonyCand = { reprPrec := SandeClemDabkowski2026.instReprHarmonyCand.repr }

def SandeClemDabkowski2026.instReprHarmonyCand.repr : HarmonyCand → ℕ → Std.Format

Equations

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

def SandeClemDabkowski2026.identIO : Constraints.Constraint HarmonyCand

(46) IDENT-IO(ATR): one violation if the output differs from the input.

Equations

• SandeClemDabkowski2026.identIO = Constraints.Constraint.binary fun (c : SandeClemDabkowski2026.HarmonyCand) => c.out ≠ c.lexical

def SandeClemDabkowski2026.atrHarm : Constraints.Constraint HarmonyCand

(47) ATRHARM: one violation if a domain-local trigger disagrees with the output.

Equations

• SandeClemDabkowski2026.atrHarm = Constraints.Constraint.binary fun (c : SandeClemDabkowski2026.HarmonyCand) => ∃ t ∈ c.trigger, t ≠ c.out

def SandeClemDabkowski2026.vPTrigger (c : ClauseConfig) (vRoot : ATR) : Option ATR

The domain-local trigger: the verb root's value when V is spelled out in vP.

Equations

• SandeClemDabkowski2026.vPTrigger c vRoot = if c.harmony = true then some vRoot else none

def SandeClemDabkowski2026.harmonyTableau (lex : ATR) (trig : Option ATR) : OptimalityTheory.Tableau HarmonyCand 2

The vP-domain tableau: both output values, ranked ATRHARM ≫ IDENT-IO(ATR).

Equations

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

theorem SandeClemDabkowski2026.optimal_eq_surfaceATR (aux fronted : Bool) (vRoot : ATR) : (harmonyTableau particleDefaultATR (vPTrigger { hasAux := aux, fronted := fronted } vRoot)).optimal = {{ lexical := particleDefaultATR, trigger := vPTrigger { hasAux := aux, fronted := fronted } vRoot, out := surfaceATR { hasAux := aux, fronted := fronted } vRoot }}

§6.1's mechanism, closed: the unique OT winner under ATRHARM ≫ IDENT-IO(ATR) surfaces with exactly surfaceATR — harmonized when a trigger is local, faithful to the lexical default otherwise.

Frozen ATR survives later movement (§6.1)

[FP05]'s Order Preservation shape applied to harmony outcomes: [SCD26] §6.1 — the particle "will retain this ATR value when it undergoes focus fronting". The record is append-only across cycles.

@[reducible, inline]

abbrev SandeClemDabkowski2026.FrozenATR : Type

Per-cycle log of frozen ATR values (terminal, value); append-only.

Equations

• SandeClemDabkowski2026.FrozenATR = List (String × SandeClemDabkowski2026.ATR)

def SandeClemDabkowski2026.extendFrozenATR (existing new : FrozenATR) : FrozenATR

Extend the log with one cycle's assignments.

Equations

• SandeClemDabkowski2026.extendFrozenATR existing new = existing ++ new

theorem SandeClemDabkowski2026.extendFrozenATR_preserves (existing new : FrozenATR) {e : String × ATR} (h : e ∈ existing) : e ∈ extendFrozenATR existing new

Order-Preservation analogue: earlier freezings survive later cycles.

def SandeClemDabkowski2026.frozenATR? (table : FrozenATR) (terminal : String) : Option ATR

The most recently frozen value on terminal, if any.

Equations

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

theorem SandeClemDabkowski2026.frozenATR?_later_overrides : frozenATR? (extendFrozenATR [("Part", Phonology.TongueRoot.ATR.plus)] [("Part", Phonology.TongueRoot.ATR.minus)]) "Part" = some Phonology.TongueRoot.ATR.minus

A later re-freeze overrides — the intended semantics, though [SCD26] posit no CP-cycle ATR re-write for the particle.

def SandeClemDabkowski2026.vPFrozen_PartSAuxOV (vRoot : ATR) : FrozenATR

The vP-cycle freezing for PartSAuxOV: Part inherits the verb root's value (e.g. /ni/ 'see' +ATR yields the particle surface form [joku], (11)–(12)).

Equations

• SandeClemDabkowski2026.vPFrozen_PartSAuxOV vRoot = [("Part", vRoot)]

theorem SandeClemDabkowski2026.PartSAuxOV_atr_persists_through_fronting (vRoot : ATR) : frozenATR? (extendFrozenATR (vPFrozen_PartSAuxOV vRoot) []) "Part" = some vRoot

The CP cycle issues no new ATR assignment for Part; the vP value persists — §6.1's "it will retain this ATR value when it undergoes focus fronting".

The PIC stance (§6.2)

def SandeClemDabkowski2026.guebiePICMode : Minimalist.PICStrength

[SCD26] §6.2: spelled-out material stays accessible to later syntax; strict PIC₁/PIC₂ would block the remnant-VP movement. The Cyclic-Linearization-bounded regime is PICStrength.linearizationBound.

Equations

• SandeClemDabkowski2026.guebiePICMode = Minimalist.PICStrength.linearizationBound

theorem SandeClemDabkowski2026.guebie_PIC_admits_remnant_movement (φ : Minimalist.Phase) (goal : Minimalist.SyntacticObject) : Minimalist.admitsExtraction guebiePICMode φ goal

Under the Guébie PIC mode every phase admits extraction; concrete crashes come from Consistent instead (nonedge_particle_fronting_crashes).

Predicate fronting is narrow-syntactic (§3)

Three diagnostics: successive cyclicity ((25)–(26)), island sensitivity ((27)–(28)), and island creation ((29)–(30)). This registers Guébie beside [HG19]'s Russian as a positive instance of VerbDoublingIsSyntactic, against [Lan06]'s PF-driven Hebrew analysis (the reason the substrate predicate is per-construction, not universal — see HarizanovGribanova2019Amalgamation.lean). The witnesses are schematic: the fronted remnant is an evacuation trace plus the verb copy, per their (31).

def SandeClemDabkowski2026.guebiePredicateDoubling : Minimalist.Movement.PredicateDoubling

The Guébie predicate-fronting witness: V evacuates, the remnant VP fronts to Spec,CP, and the trace is pronounced — verb doubling.

Equations

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

theorem SandeClemDabkowski2026.guebie_properRemnant : Minimalist.Movement.properRemnant guebiePredicateDoubling.toRemnantFronting

The evacuated verb sat inside the fronted remnant.

def SandeClemDabkowski2026.guebieFrontingDerivation : Minimalist.SyntacticObject.Derivation

On the carrier, Internal Merge leaves a trace at the deeper position ([MCB25] §1.4.3); surface doubling is the pronunciation of both positions.

Equations

• SandeClemDabkowski2026.guebieFrontingDerivation = { initial := SandeClemDabkowski2026.guebieFrontedVP✝, steps := [Minimalist.SyntacticObject.Step.im SandeClemDabkowski2026.guebieVerbLeaf✝] }

theorem SandeClemDabkowski2026.guebie_VDIS_positive_instance : Minimalist.VerbDoublingIsSyntacticIn guebieFrontingDerivation SandeClemDabkowski2026.guebieVerbLeaf✝

Guébie registered as a positive instance of VerbDoublingIsSyntacticIn (§3's diagnostics; decidable from the derivation structure).

The §7 prediction and the Wolof parallel

The analysis predicts that "the target and trigger of harmony must be local at some point in the derivation, namely at an instance of spell-out", with later movement of one of them deriving surface discontinuity (§7). Guébie instantiates it with the target (particle) moving; Wolof relative clauses ([Sy05], [Mar19]) with the trigger (head noun) moving out of the DP phase, past non-harmonizing stative-verb material ((49)–(50)).

def SandeClemDabkowski2026.HarmonyProfile (low surface : List String) (trigger target : String) : Prop

The §7 prediction schema: trigger and target co-spelled-out at a low phase, and the two-phase derivation linearizes.

Equations

• SandeClemDabkowski2026.HarmonyProfile low surface trigger target = (trigger ∈ low ∧ target ∈ low ∧ Minimalist.Linearization.Consistent [low, surface])

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableHarmonyProfile (low surface : List String) (trigger target : String) : Decidable (HarmonyProfile low surface trigger target)

Equations

• SandeClemDabkowski2026.instDecidableHarmonyProfile low surface trigger target = id inferInstance

theorem SandeClemDabkowski2026.guebie_profile : HarmonyProfile { hasAux := true, fronted := true }.vPSpellOut { hasAux := true, fronted := true }.surfaceOrder "V" "Part"

Guébie's fronted SAuxOV clause instantiates the §7 profile: V and Part are co-spelled-out in vP, and the fronted surface linearizes consistently.

inductive SandeClemDabkowski2026.WolofShape : Type

The Wolof shapes ([Sy05] (49)–(50)): a bare noun–demonstrative DP, or a relative clause with the head noun fronted past the stative verb.

• localDP : WolofShape

  head dem ((49)): no relative clause.

• relClause : WolofShape

  head rel stative dem ((50)): head noun A′-moved to the left edge.

@[instance_reducible]

instance SandeClemDabkowski2026.instDecidableEqWolofShape : DecidableEq WolofShape

Equations

• SandeClemDabkowski2026.instDecidableEqWolofShape x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SandeClemDabkowski2026.instReprWolofShape.repr : WolofShape → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SandeClemDabkowski2026.instReprWolofShape : Repr WolofShape

Equations

• SandeClemDabkowski2026.instReprWolofShape = { reprPrec := SandeClemDabkowski2026.instReprWolofShape.repr }

def SandeClemDabkowski2026.WolofShape.dpSpellOut : WolofShape → List String

Head noun and demonstrative are spelled out together at the DP phase in both shapes — harmony's locality is phase-internal, not surface.

Equations

• x✝.dpSpellOut = ["head", "dem"]

def SandeClemDabkowski2026.WolofShape.surfaceOrder : WolofShape → List String

The surface strings of (49)–(50).

Equations

• SandeClemDabkowski2026.WolofShape.localDP.surfaceOrder = ["head", "dem"]
• SandeClemDabkowski2026.WolofShape.relClause.surfaceOrder = ["head", "rel", "stative", "dem"]

theorem SandeClemDabkowski2026.wolof_profile (sh : WolofShape) : HarmonyProfile sh.dpSpellOut sh.surfaceOrder "head" "dem"

Both Wolof shapes instantiate the §7 profile — the same schema Guébie satisfies, with the trigger rather than the target moving.

theorem SandeClemDabkowski2026.wolof_discontinuous : ¬["head", "dem"] <:+: WolofShape.relClause.surfaceOrder ∧ "head" ∈ WolofShape.relClause.dpSpellOut ∧ "dem" ∈ WolofShape.relClause.dpSpellOut

Wolof discontinuity: in the relative clause the head and demonstrative are not surface-adjacent, yet they were co-spelled-out at the DP phase.