Cyclic Linearization of Syntactic Structure

@cite{fox-pesetsky-2005}

Formalizes the core of @cite{fox-pesetsky-2005}'s theory of the syntax-phonology interface. The key claims:

1. Spell-out domains: linearization applies at the end of each phase (Spell-out domain), establishing the relative order of overt terminals.

2. Order Preservation: ordering established at Spell-out of a domain is never deleted or contradicted by later Spell-out.

3. Successive cyclicity as a consequence: movement from a phase must proceed through the phase edge (leftmost position) to avoid contradicting ordering established at earlier Spell-out.

4. Ordering contradiction → ungrammaticality: if the ordering statements accumulated across phases form a cycle, the structure cannot be coherently linearized and the derivation crashes.

The formalization here provides the minimal infrastructure needed to derive the meN-deletion effect in Malayic languages (@cite{erlewine-sommerlot-2025}), Holmberg's Generalization (Object Shift requires verb movement), and successive-cyclicity requirements. All three are formalized as concrete theorems.

Key definitions

• Prec: a precedence statement (α precedes β)
• allPrecs: generates all pairwise precedences from a terminal sequence
• hasContradiction: checks for direct ordering cycles (a < b ∧ b < a)
• hasCycle: checks for cycles of any length via BFS reachability
• extendOrderingTable: Linearize operation accumulating precedences across phases
• SpelloutAndCheck: extend an empty table over all phases and check consistency

The operation extendOrderingTable was previously named spellout and collided with Minimalist.spellout (the VI exponent-realization operation in Theories/Morphology/DM/VocabSimple.lean); the rename disambiguates.

structure Minimalist.Linearization.Prec : Type

A precedence statement: before must linearly precede after in PF. Corresponds to @cite{fox-pesetsky-2005}'s "α < β" notation (their (10)).

• before : String
• after : String

@[implicit_reducible]

instance Minimalist.Linearization.instDecidableEqPrec : DecidableEq Prec

Equations

• Minimalist.Linearization.instDecidableEqPrec = Minimalist.Linearization.instDecidableEqPrec.decEq

def Minimalist.Linearization.instDecidableEqPrec.decEq (x✝ x✝¹ : Prec) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.Linearization.instReprPrec.repr : Prec → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.Linearization.instReprPrec : Repr Prec

Equations

• Minimalist.Linearization.instReprPrec = { reprPrec := Minimalist.Linearization.instReprPrec.repr }

def Minimalist.Linearization.allPrecs : List String → List Prec

Generate all pairwise precedences from a left-to-right sequence of overt terminal labels. Given terminals [a, b, c], produces [a < b, a < c, b < c].

Equations

• Minimalist.Linearization.allPrecs [] = []
• Minimalist.Linearization.allPrecs (x_1 :: xs) = List.map (fun (y : String) => { before := x_1, after := y }) xs ++ Minimalist.Linearization.allPrecs xs

@[reducible, inline]

abbrev Minimalist.Linearization.OrderingTable : Type

An Ordering Table is the accumulated set of precedence statements across all Spell-out domains in a derivation. Corresponds to @cite{fox-pesetsky-2005}'s Ordering Table ((52)).

Equations

• Minimalist.Linearization.OrderingTable = List Minimalist.Linearization.Prec

def Minimalist.Linearization.HasContradiction (table : OrderingTable) : Prop

An Ordering Table contains a direct contradiction: some α, β such that both α < β and β < α appear. A contradiction means the derivation cannot be coherently linearized and crashes.

Note: for the Malayic voice/extraction application, all contradictions are direct (no transitive closure needed). For cycles of length > 2 use HasCycle (BFS-based, decidable too).

Equations

• Minimalist.Linearization.HasContradiction table = ∃ s ∈ table, ∃ t ∈ table, s.before = t.after ∧ s.after = t.before

@[implicit_reducible]

instance Minimalist.Linearization.instDecidableHasContradiction (table : OrderingTable) : Decidable (HasContradiction table)

Equations

• Minimalist.Linearization.instDecidableHasContradiction table = id inferInstance

def Minimalist.Linearization.Consistent (table : OrderingTable) : Prop

An Ordering Table is consistent iff it contains no contradictions.

Equations

• Minimalist.Linearization.Consistent table = ¬Minimalist.Linearization.HasContradiction table

@[implicit_reducible]

instance Minimalist.Linearization.instDecidableConsistent (table : OrderingTable) : Decidable (Consistent table)

Equations

• Minimalist.Linearization.instDecidableConsistent table = Minimalist.Linearization.instDecidableConsistent._aux_1 table

def Minimalist.Linearization.extendOrderingTable (existing : OrderingTable) (phaseTerminals : List String) : OrderingTable

Extend an existing Ordering Table by Linearizing one phase: generate ordering statements from the left-to-right sequence of overt terminals in the phase, and append them to the table.

Implements Order Preservation: existing statements are kept (never deleted), new statements appended. Corresponds to @cite{fox-pesetsky-2005}'s Linearize operation ((52)). Renamed from spellout to disambiguate from Minimalist.spellout (the VI exponent-realization operation).

Equations

• Minimalist.Linearization.extendOrderingTable existing phaseTerminals = existing ++ Minimalist.Linearization.allPrecs phaseTerminals

def Minimalist.Linearization.SpelloutAndCheck (phases : List (List String)) : Prop

Multi-phase derivation is consistently linearizable. Each element of phases is the left-to-right sequence of overt terminals at the corresponding Spell-out domain. Ordering statements accumulate across phases via Order Preservation.

Equations

• Minimalist.Linearization.SpelloutAndCheck phases = Minimalist.Linearization.Consistent (List.foldl Minimalist.Linearization.extendOrderingTable [] phases)

@[implicit_reducible]

instance Minimalist.Linearization.instDecidableSpelloutAndCheck (phases : List (List String)) : Decidable (SpelloutAndCheck phases)

Equations

• Minimalist.Linearization.instDecidableSpelloutAndCheck phases = Minimalist.Linearization.instDecidableSpelloutAndCheck._aux_1 phases

theorem Minimalist.Linearization.extendOrderingTable_preserves (existing : OrderingTable) (phase : List String) (p : Prec) (hp : p ∈ existing) : p ∈ extendOrderingTable existing phase

Order Preservation: existing ordering statements are never deleted by extension. All precedences from earlier phases persist. Formal content of @cite{fox-pesetsky-2005}'s Order Preservation.

theorem Minimalist.Linearization.allPrecs_after_mem {p : Prec} {ts : List String} (h : p ∈ allPrecs ts) : p.after ∈ ts

Every element of allPrecs ts has its after field drawn from ts.

theorem Minimalist.Linearization.allPrecs_before_mem {p : Prec} {ts : List String} (h : p ∈ allPrecs ts) : p.before ∈ ts

Every element of allPrecs ts has its before field drawn from ts.

theorem Minimalist.Linearization.allPrecs_antisym (ts : List String) : ts.Nodup → ∀ s ∈ allPrecs ts, ∀ t ∈ allPrecs ts, s.before = t.after → s.after ≠ t.before

In a Nodup list, allPrecs never contains both ⟨a,b⟩ and ⟨b,a⟩: if a precedes b, then b does not precede a.

theorem Minimalist.Linearization.single_phase_consistent (ts : List String) (hnd : ts.Nodup) : Consistent (allPrecs ts)

A single phase is always consistent: no ordering contradiction can arise within a single left-to-right linearization of distinct terminals. Requires Nodup because duplicate terminals create trivial self-loops (α < α), which HasContradiction correctly flags.

theorem Minimalist.Linearization.edge_movement_consistent : SpelloutAndCheck [["X", "Y", "Z"], ["X", "α", "Y", "Z"]]

Leftward movement from the phase edge preserves ordering. Scenario 1 of @cite{fox-pesetsky-2005} (their (13)): X was at the left edge of D; when D' is spelled out, X moves further left. The new ordering X < α is consistent with X < Y from D.

theorem Minimalist.Linearization.non_edge_movement_contradiction : ¬SpelloutAndCheck [["X", "Y", "Z"], ["Y", "α", "X", "Z"]]

Leftward movement from a non-edge position creates contradiction. Scenario 2 of @cite{fox-pesetsky-2005} (their (14)): Y was NOT at the left edge of D (X < Y at D Spell-out). When Y moves left in D', it must precede α, but α < X and X < Y yield a cycle.

theorem Minimalist.Linearization.successive_cyclic_ok : SpelloutAndCheck [["to_whom", "gave", "the_book"], ["to_whom", "that", "Mary", "gave", "the_book"]]

Successive-cyclic wh-movement avoids ordering contradiction. @cite{fox-pesetsky-2005} (their (6)–(8)): to whom moves through Spec,VP before moving to Spec,CP, preserving VP-internal order.

theorem Minimalist.Linearization.non_successive_cyclic_bad : ¬SpelloutAndCheck [["gave", "the_book", "to_whom"], ["to_whom", "that", "Mary", "gave", "the_book"]]

Non-successive-cyclic movement creates ordering contradiction. @cite{fox-pesetsky-2005} (their (3)–(5)): to whom skips Spec,VP and moves directly to Spec,CP, contradicting VP-internal order.

theorem Minimalist.Linearization.simultaneous_order_preserving : SpelloutAndCheck [["A", "B", "C"], ["A", "B", "D", "C"]]

Order-preserving simultaneous movement: two elements moving out of a phase in their original relative order creates no contradiction. This is the key configuration for Malayic object extraction (@cite{erlewine-sommerlot-2025} ex. 55–56).

theorem Minimalist.Linearization.simultaneous_order_reversing : ¬SpelloutAndCheck [["A", "B", "C"], ["B", "A", "D", "C"]]

Simultaneous movement that reverses relative order contradicts.

Object Shift and verb movement

@cite{fox-pesetsky-2005} derive Holmberg's Generalization: Object Shift in Scandinavian is only possible when the verb has also moved out of VP.

VP Spell-out establishes V < Obj. If the verb stays in VP and the object shifts leftward, the higher Spell-out domain orders Obj < V — directly contradicting V < Obj. When the verb also moves, V < Obj is preserved.

theorem Minimalist.Linearization.no_object_shift : SpelloutAndCheck [["V", "Obj"], ["Subj", "V", "Neg", "Obj"]]

Baseline: no Object Shift, verb moves to I. Consistent. VP contains only [V, Obj]; Neg is above VP.

theorem Minimalist.Linearization.object_shift_with_verb_movement : SpelloutAndCheck [["V", "Obj"], ["Subj", "V", "Obj", "Neg"]]

Object Shift WITH verb movement: both V and Obj move past Neg. VP-internal ordering V < Obj is preserved at IP. Consistent. @cite{fox-pesetsky-2005} §3.

theorem Minimalist.Linearization.object_shift_without_verb_movement : ¬SpelloutAndCheck [["V", "Obj"], ["Subj", "Obj", "Neg", "V"]]

Object Shift WITHOUT verb movement: Obj moves past Neg but V stays. VP: V < Obj. IP: Obj < ... < V. Direct contradiction → crash. This IS Holmberg's Generalization, derived from cyclic linearization. @cite{fox-pesetsky-2005} §3.

Full cycle detection via reachability

HasContradiction detects direct ordering cycles (a < b ∧ b < a). For completeness, HasCycle detects cycles of any length via the Relation.ReflTransGen reachability over the directed precedence graph (with Decidable derived from Core.Relation.ReflTransGen.decidable_of_finite). For all current applications (Malayic voice, Holmberg's Generalization), contradictions are direct, so both predicates agree.

def Minimalist.Linearization.precedeStep (table : OrderingTable) (src dst : String) : Prop

One-step precedence relation in table: there exists an entry ⟨src, dst⟩.

Equations

• Minimalist.Linearization.precedeStep table src dst = ({ before := src, after := dst } ∈ table)

@[implicit_reducible]

instance Minimalist.Linearization.instDecidablePrecedeStep (table : OrderingTable) (src dst : String) : Decidable (precedeStep table src dst)

Equations

• Minimalist.Linearization.instDecidablePrecedeStep table src dst = Minimalist.Linearization.instDecidablePrecedeStep._aux_1 table src dst

def Minimalist.Linearization.Reachable (table : OrderingTable) (src dst : String) : Prop

dst is reachable from src via directed edges in table. The relation is Relation.ReflTransGen of the one-step precedeStep. Decidability is supplied by the Core.Relation.ReflTransGen substrate using the table's vertex universe as the finite carrier.

Equations

• Minimalist.Linearization.Reachable table src dst = Relation.ReflTransGen (Minimalist.Linearization.precedeStep table) src dst

@[implicit_reducible]

instance Minimalist.Linearization.instDecidableReachable (table : OrderingTable) (src dst : String) : Decidable (Reachable table src dst)

Equations

• Minimalist.Linearization.instDecidableReachable table src dst = Relation.ReflTransGen.decidable_of_finite (Minimalist.Linearization.tableVerts✝ table) ⋯ src dst

def Minimalist.Linearization.HasCycle (table : OrderingTable) : Prop

An Ordering Table contains a directed cycle of any length: some edge a → b such that b can reach a via other edges.

Equations

• Minimalist.Linearization.HasCycle table = ∃ edge ∈ table, Minimalist.Linearization.Reachable table edge.after edge.before

@[implicit_reducible]

instance Minimalist.Linearization.instDecidableHasCycle (table : OrderingTable) : Decidable (HasCycle table)

Equations

• Minimalist.Linearization.instDecidableHasCycle table = id inferInstance

theorem Minimalist.Linearization.hasCycle_detects_transitive : HasCycle [{ before := "a", after := "b" }, { before := "b", after := "c" }, { before := "c", after := "a" }] ∧ ¬HasContradiction [{ before := "a", after := "b" }, { before := "b", after := "c" }, { before := "c", after := "a" }]

HasCycle detects the transitive cycle a < b, b < c, c < a which HasContradiction misses (no direct a < b ∧ b < a pair).

theorem Minimalist.Linearization.cycle_direct_agree_malayic : have t := allPrecs ["theme", "me-", "agent", "NV"] ++ allPrecs ["theme", "agent", "Aux", "me-", "NV"]; HasCycle t ↔ HasContradiction t

On the Malayic meN-deletion example, both checks agree (the contradiction is direct).

Per-cycle frozen feature assignments

@cite{fox-pesetsky-2005}'s Order Preservation says precedences emitted at one Spell-out are preserved through subsequent Spell-outs. The same shape applies to feature values established by phase-bounded phonological computation: when vP is spelled out and a feature value (e.g. +ATR on a particle) is set by phase-internal phonology, that value is preserved through later syntactic movement of the bearer.

@cite{sande-clem-dabkowski-2026} §6.1 argues this is the right way to think about Guébie discontinuous harmony: the particle's ATR value is fixed at vP spell-out (when the verb is local to it inside vP), and later A′-movement of the remnant VP carries the frozen value to Spec,CP. The intervening subject/auxiliary/object are spelled out in the higher CP phase with their own (unaffected) ATR values.

This section provides the analogous append-only accumulator for feature freezings. It does not generalize OrderingTable (which stays precedence-only); the two registries can be combined externally by a study file when needed.

structure Minimalist.Linearization.FrozenFeature : Type

A frozen feature assignment: terminal t had feature f set to value at the spell-out cycle that emitted this entry.

• terminal : String
• feature : String
• value : Bool

@[implicit_reducible]

instance Minimalist.Linearization.instDecidableEqFrozenFeature : DecidableEq FrozenFeature

Equations

• Minimalist.Linearization.instDecidableEqFrozenFeature = Minimalist.Linearization.instDecidableEqFrozenFeature.decEq

def Minimalist.Linearization.instDecidableEqFrozenFeature.decEq (x✝ x✝¹ : FrozenFeature) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.Linearization.instReprFrozenFeature : Repr FrozenFeature

Equations

• Minimalist.Linearization.instReprFrozenFeature = { reprPrec := Minimalist.Linearization.instReprFrozenFeature.repr }

def Minimalist.Linearization.instReprFrozenFeature.repr : FrozenFeature → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Minimalist.Linearization.FrozenFeatureTable : Type

Per-cycle log of feature assignments preserved across spell-out. The analogue of OrderingTable for features rather than precedences. Append-only: never deleted.

Equations

• Minimalist.Linearization.FrozenFeatureTable = List Minimalist.Linearization.FrozenFeature

def Minimalist.Linearization.extendFrozenFeatures (existing : FrozenFeatureTable) (phaseFreezings : List FrozenFeature) : FrozenFeatureTable

Extend a frozen-feature table with the assignments emitted by one spell-out cycle. The analogue of extendOrderingTable.

Equations

• Minimalist.Linearization.extendFrozenFeatures existing phaseFreezings = existing ++ phaseFreezings

theorem Minimalist.Linearization.extendFrozenFeatures_preserves (existing : FrozenFeatureTable) (phaseFreezings : List FrozenFeature) (f : FrozenFeature) (h : f ∈ existing) : f ∈ extendFrozenFeatures existing phaseFreezings

Order-Preservation analogue for features: feature freezings emitted at earlier phases survive subsequent spell-out. The formal content of @cite{sande-clem-dabkowski-2026}'s "the ATR value persists through syntactic movement" claim.

def Minimalist.Linearization.frozenValue (table : FrozenFeatureTable) (terminal feature : String) : Option Bool

Lookup the most-recently-frozen value of feature on terminal, if any. Returns none if not yet frozen.

Phase-internal phonology that resets a feature value writes a new entry; the most recent assignment wins per List.find? traversal order (we reverse so later-appended entries are checked first).

Equations

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

theorem Minimalist.Linearization.frozen_atr_persists_through_cp_phase : frozenValue (extendFrozenFeatures [{ terminal := "Part", feature := "ATR", value := true }] []) "Part" "ATR" = some true

Two-phase feature preservation example: ATR value frozen at vP survives the CP-phase spell-out. Mimics SCD 2026's PartSAuxOV derivation: at vP spell-out, the particle (Part) is set to +ATR by harmony with the verb; the CP phase emits no further ATR assignments on Part; the value persists.

theorem Minimalist.Linearization.frozen_value_later_overrides : frozenValue (extendFrozenFeatures [{ terminal := "Part", feature := "ATR", value := true }] [{ terminal := "Part", feature := "ATR", value := false }]) "Part" "ATR" = some false

A later phase that re-freezes the same feature overrides the earlier value. (Not used by SCD 2026, which posits no CP-phase ATR re-write for the particle, but documents the intended override semantics.)