Linear Correspondence Axiom

@cite{chomsky-1995} @cite{kayne-1994}

Formalizes the core of @cite{kayne-1994}'s The Antisymmetry of Syntax: the Linear Correspondence Axiom (LCA), which derives linear (temporal) precedence of terminal elements from asymmetric c-command in the hierarchical structure.

Key definitions

• dominatedTerminals: d(X) — the set of terminals dominated by X (alias for terminalNodes from Basic.lean). Noncomputable in Phase 1.0 because terminalNodes is.
• lcaPrecedesIn: the derived precedence relation on terminals
• SatisfiesLCAIn: the LCA as a well-formedness condition (strict total order)

Main results

• Outer precedes inner (outer_precedes_inner): in [x [y z]] where all three are leaves, x precedes both y and z
• Specifier precedes head and complement (spec_precedes_head_complement): alias for outer_precedes_inner
• Head precedes complement internals (head_precedes_complement): alias for outer_precedes_inner
• No right specifier (no_right_specifier)
• Adjunction is left-adjunction (adjunction_left_only)
• Sister terminals are unordered (sister_terminals_unordered)

Phase 1.0 status

This file uses terminalNodes and linearize, both of which became noncomputable in the FreeCommMagma migration (planar order is not preserved by the substrate's commutativity quotient). The LCA itself is intrinsically planar, so this entire module's concrete computational content (e.g., the Examples section) has been moved to sorry / removed pending a Phase 2 LCA-based planarization. The theorems about lcaPrecedesIn survive because they reduce to membership facts about subtrees (now Multiset) and immediatelyContains / cCommandsIn, which remain decidable.

noncomputable def Minimalist.dominatedTerminals : SyntacticObject → List SyntacticObject

d(X): the set of terminals dominated by (or equal to) X. Corresponds to Kayne's d function (p. 16). Noncomputable in Phase 1.0 because terminalNodes lifts via Quot.out. The Phase 2 parameterized variant is dominatedTerminalsWith h (below).

Equations

• Minimalist.dominatedTerminals = Minimalist.terminalNodes

def Minimalist.dominatedTerminalsWith (h : HeadFunction) : SyntacticObject → List SyntacticObject

Parameterized d(X) under head function h: the terminals of h.section_.σ X in left-to-right order. Computable when h.section_.σ is. Alias for HeadFunction.terminalNodes.

Equations

• Minimalist.dominatedTerminalsWith h = h.terminalNodes

def Minimalist.lcaPrecedesIn (root a b : SyntacticObject) : Prop

Tree-relative LCA precedence. Terminal a precedes terminal b within root iff there exist subterms X, Y of root such that X asymmetrically c-commands Y (within root), a ∈ d(X), and b ∈ d(Y).

Equations

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

structure Minimalist.SatisfiesLCAIn (root : SyntacticObject) : Prop

The LCA holds for a tree root iff lcaPrecedesIn root is a strict total order on its terminal nodes: irreflexive, transitive, and total (every pair of distinct terminals is ordered).

• irrefl (t : SyntacticObject) : t ∈ terminalNodes root → ¬lcaPrecedesIn root t t

  No terminal precedes itself.

• trans (a b c : SyntacticObject) : a ∈ terminalNodes root → b ∈ terminalNodes root → c ∈ terminalNodes root → lcaPrecedesIn root a b → lcaPrecedesIn root b c → lcaPrecedesIn root a c

  Precedence is transitive.

• total (a b : SyntacticObject) : a ∈ terminalNodes root → b ∈ terminalNodes root → a ≠ b → lcaPrecedesIn root a b ∨ lcaPrecedesIn root b a

  Every pair of distinct terminals is ordered.

theorem Minimalist.outer_cCommandsIn_inner_left (x y z : SyntacticObject) (hne : x ≠ y.node z) : cCommandsIn (x.node (y.node z)) x y

In root = node x (node y z), x c-commands y within root. Works for arbitrary SOs, not just leaves.

theorem Minimalist.outer_cCommandsIn_inner_right (x y z : SyntacticObject) (hne : x ≠ y.node z) : cCommandsIn (x.node (y.node z)) x z

In root = node x (node y z), x c-commands z within root. Works for arbitrary SOs, not just leaves.

theorem Minimalist.outer_precedes_inner (x y z : LIToken) (hne_xy : x ≠ y) (hne_xz : x ≠ z) (hne_yz : y ≠ z) : have root := (SyntacticObject.leaf x).node ((SyntacticObject.leaf y).node (SyntacticObject.leaf z)); lcaPrecedesIn root (SyntacticObject.leaf x) (SyntacticObject.leaf y) ∧ lcaPrecedesIn root (SyntacticObject.leaf x) (SyntacticObject.leaf z)

Outer precedes inner under the LCA. For root = node (leaf x) (node (leaf y) (leaf z)) where all three are distinct leaves, x precedes both y and z in lcaPrecedesIn root.

This is Kayne's key result (1994, pp. 35-36): the outer daughter asymmetrically c-commands everything in its sister's projection, so all its terminals precede all terminals of the inner daughters.

Subsumes both "specifier precedes head/complement" and "head precedes complement internals".

theorem Minimalist.spec_precedes_head_complement (spec head compl : LIToken) (hne_sh : spec ≠ head) (hne_sc : spec ≠ compl) (hne_hc : head ≠ compl) : have root := (SyntacticObject.leaf spec).node ((SyntacticObject.leaf head).node (SyntacticObject.leaf compl)); lcaPrecedesIn root (SyntacticObject.leaf spec) (SyntacticObject.leaf head) ∧ lcaPrecedesIn root (SyntacticObject.leaf spec) (SyntacticObject.leaf compl)

Specifier precedes head and complement under the LCA. Alias for outer_precedes_inner with conventional names.

theorem Minimalist.head_precedes_complement (head a b : LIToken) (hne_ha : head ≠ a) (hne_hb : head ≠ b) (hne_ab : a ≠ b) : have root := (SyntacticObject.leaf head).node ((SyntacticObject.leaf a).node (SyntacticObject.leaf b)); lcaPrecedesIn root (SyntacticObject.leaf head) (SyntacticObject.leaf a) ∧ lcaPrecedesIn root (SyntacticObject.leaf head) (SyntacticObject.leaf b)

Head precedes complement internals. Alias for outer_precedes_inner with conventional names.

theorem Minimalist.no_right_specifier (head compl spec : SyntacticObject) (hne_hc_node : head.node compl ≠ spec) : have root := (head.node compl).node spec; cCommandsIn root spec head

Right specifiers are LCA-incompatible. In root = node (node head compl) spec, spec's sister is node head compl, which contains head. So spec c-commands head. But head's sister (within the tree) is compl, which does not contain spec (spec is in the other branch).

The LCA therefore orders spec's terminals BEFORE head's terminals. But the PF string has head before spec (right-specifier position). This contradiction means right specifiers are ruled out: the LCA forces specifiers to the left.

theorem Minimalist.adjunction_left_only_with (h : HeadFunction) (mover target : SyntacticObject) (h_ext_node : h.section_.σ (mover.node target) = h.section_.σ mover * h.section_.σ target) : h.linearize (mover.node target) = h.linearize mover ++ h.linearize target

Head-to-head adjunction must be left-adjunction (parameterized). Under a head function h whose externalize section sends a node to the *-product of its children's externalizations, linearization concatenates in left-to-right order (mover then target).

The hypothesis h_ext_node : h.section_.σ (.node mover target) = h.section_.σ mover * h.section_.σ target is the local-magma-morphism property at this specific node. MCB Lemma 1.13.1 rules out a global magma morphism SO → SO^{nc}, but a particular externalize choice can satisfy this property at any specific node — and consumers who supply a derivation-built externalize get this for free per construction.

The unparameterized adjunction_left_only (currently sorry) cannot be proven without committing to an externalize: Quot.out (.node mover target) may pick either mover.out * target.out or target.out * mover.out.

theorem Minimalist.sister_terminals_unordered (a b : LIToken) (hne : a ≠ b) : ¬asymCCommandsIn ((SyntacticObject.leaf a).node (SyntacticObject.leaf b)) (SyntacticObject.leaf a) (SyntacticObject.leaf b)

Sister terminals are unordered by the LCA. For root = node (leaf a) (leaf b), leaf a and leaf b are sisters: each c-commands the other (via its sister). So neither asymmetrically c-commands the other, and lcaPrecedesIn does not order them.

This is not a defect but a feature: in well-formed BPS, sister terminals don't arise. Complements are always phrases (nodes), and heads project, so the complement of a head is always node X Y, not a bare leaf.