Syntactic Objects and Containment

@cite{chomsky-2013} @cite{marcolli-chomsky-berwick-2025}

Foundation module for the Minimalist Program formalization.

Syntactic Objects

SyntacticObject is FreeMagma LIToken: bare phrase structure as the free magma over lexical-item tokens, following @cite{marcolli-chomsky-berwick-2025}. The two constructors are FreeMagma.of (lexical leaves) and FreeMagma.mul (binary Merge). The shims SyntacticObject.leaf / SyntacticObject.node rename them at the linguistic interface.

The Y-model branches by map, not by type: PF lives natively on SyntacticObject via linearize/phonYield; the LF lift to Tree Unit String lives in SpellOut.lean (SyntacticObject.toLFTree), which handles trace detection and phonForm extraction.

• SimpleLI, LexicalItem, LIToken, SyntacticObject
• merge, externalMerge, internalMerge

Containment Relations

• Immediate Containment: X immediately contains Y iff Y is a member of X
• Containment (Dominance): Transitive closure of immediate containment
• C-command: Standard asymmetric relation for binding and locality

inductive Minimalist.Cat : Type

Categorial features (Definition 10).

Enumerates the head categories of the Minimalist Program clausal spine and nominal extended projection: cartographic left periphery, inflectional spine, v/Voice/Appl event-structure layer, nominal categorizer-and-quantity sequence, and adpositional Place/Path articulation.

• V : Cat
• N : Cat
• A : Cat
• P : Cat
• D : Cat
• T : Cat
• C : Cat
• v : Cat
• n : Cat
• a : Cat
• Place : Cat
• Path : Cat
• Num : Cat
• Q : Cat
• Voice : Cat
• Appl : Cat
• Foc : Cat
• Top : Cat
• Fin : Cat
• SA : Cat
• Force : Cat
• Neg : Cat
• Mod : Cat
• Rel : Cat
• Pol : Cat
• Asp : Cat
• Evid : Cat
• Nmlz : Cat
• K : Cat

def Minimalist.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• Minimalist.instReprCat.repr Minimalist.Cat.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.V")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.N")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.A")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.P prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.P")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.D")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.T prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.T")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.C")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.v")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.n")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.a")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Place prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Place")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Path prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Path")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Num prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Num")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Q prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Q")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Voice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Voice")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Appl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Appl")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Foc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Foc")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Top")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Fin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Fin")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.SA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.SA")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Force prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Force")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Neg")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Mod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Mod")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Rel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Rel")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Pol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Pol")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Asp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Asp")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Evid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Evid")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.Nmlz prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.Nmlz")).group prec✝
• Minimalist.instReprCat.repr Minimalist.Cat.K prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalist.Cat.K")).group prec✝

@[implicit_reducible]

instance Minimalist.instReprCat : Repr Cat

Equations

• Minimalist.instReprCat = { reprPrec := Minimalist.instReprCat.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqCat : DecidableEq Cat

Equations

• Minimalist.instDecidableEqCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.instInhabitedCat.default : Cat

Equations

• Minimalist.instInhabitedCat.default = Minimalist.Cat.V

@[implicit_reducible]

instance Minimalist.instInhabitedCat : Inhabited Cat

Equations

• Minimalist.instInhabitedCat = { default := Minimalist.instInhabitedCat.default }

@[reducible, inline]

abbrev Minimalist.SelStack : Type

Selectional stack consumed left-to-right

Equations

• Minimalist.SelStack = List Minimalist.Cat

structure Minimalist.SimpleLI : Type

A simple LI is a ⟨CAT, SEL⟩ pair (Definition 10), optionally with a phonological form for linearization.

• cat : Cat
• sel : SelStack
• phonForm : String

@[implicit_reducible]

instance Minimalist.instReprSimpleLI : Repr SimpleLI

Equations

• Minimalist.instReprSimpleLI = { reprPrec := Minimalist.instReprSimpleLI.repr }

def Minimalist.instReprSimpleLI.repr : SimpleLI → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqSimpleLI : DecidableEq SimpleLI

Equations

• Minimalist.instDecidableEqSimpleLI = Minimalist.instDecidableEqSimpleLI.decEq

def Minimalist.instDecidableEqSimpleLI.decEq (x✝ x✝¹ : SimpleLI) : Decidable (x✝ = x✝¹)

Equations

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

structure Minimalist.LexicalItem : Type

Lexical item (simple or complex from head movement, Definition 88)

• features : List SimpleLI
• nonempty : self.features ≠ []

def Minimalist.instReprLexicalItem.repr : LexicalItem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprLexicalItem : Repr LexicalItem

Equations

• Minimalist.instReprLexicalItem = { reprPrec := Minimalist.instReprLexicalItem.repr }

@[implicit_reducible]

instance Minimalist.instDecidableEqLexicalItem : DecidableEq LexicalItem

Equations

• Minimalist.instDecidableEqLexicalItem a b = if h : a.features = b.features then isTrue ⋯ else isFalse ⋯

def Minimalist.LexicalItem.simple (cat : Cat) (sel : SelStack) (phonForm : String := "") : LexicalItem

Create a simple (non-complex) LI

Equations

• Minimalist.LexicalItem.simple cat sel phonForm = { features := [{ cat := cat, sel := sel, phonForm := phonForm }], nonempty := ⋯ }

def Minimalist.LexicalItem.outerCat (li : LexicalItem) : Cat

Get the outer (projecting) category of an LI

Equations

• li.outerCat = match li.features with | [] => Minimalist.Cat.V | s :: tail => s.cat

def Minimalist.LexicalItem.outerSel (li : LexicalItem) : SelStack

Get the outer selectional requirements

Equations

• li.outerSel = match li.features with | [] => [] | s :: tail => s.sel

def Minimalist.LexicalItem.isComplex (li : LexicalItem) : Bool

Is this LI complex (result of head-to-head movement)?

Equations

• li.isComplex = decide (li.features.length > 1)

def Minimalist.LexicalItem.combine (target mover : LexicalItem) : LexicalItem

Combine two LIs for head-to-head movement (target reprojects)

Equations

• target.combine mover = { features := target.features ++ mover.features, nonempty := ⋯ }

structure Minimalist.LIToken : Type

LI token: specific instance of an LI in a derivation

• item : LexicalItem
• id : ℕ

@[implicit_reducible]

instance Minimalist.instReprLIToken : Repr LIToken

Equations

• Minimalist.instReprLIToken = { reprPrec := Minimalist.instReprLIToken.repr }

def Minimalist.instReprLIToken.repr : LIToken → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableEqLIToken : DecidableEq LIToken

Equations

• Minimalist.instDecidableEqLIToken a b = if hid : a.id = b.id then if hitem : a.item = b.item then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Minimalist.SyntacticObject : Type

Syntactic object: nonplanar binary tree over LIToken ⊕ Nat, realized as FreeCommMagma (LIToken ⊕ Nat).

Per @cite{marcolli-chomsky-berwick-2025} Definition 1.1.1 (book p. 22), SO is the free, non-associative, commutative magma Magma_{na,c}(SO_0, M) with M(α,β) = {α,β} (unordered). Linguistically, this is the position that Merge produces unordered sets, with linearization (PF / LCA / head-directionality) as a separate Externalization step.

The three "constructors" at the SO interface are:

• .leaf tok — a lexical leaf, encoded as FreeCommMagma.of (.inl tok)
• .trace n — a trace marker, encoded as FreeCommMagma.of (.inr n)
• binary Merge, written l * r (commutative: l * r = r * l as a strict equality inside the quotient)

Trace handling: linglib's LIToken ⊕ Nat is a deliberate divergence from MCB

MCB's SO_0 (book p. 22, Def 1.1.1) consists of lexical items and syntactic features only — not trace markers. Internal Merge in MCB is a workspace-level cut-and-extract operation: an accessible term is extracted, leaving one of three possible remainder forms (Defs 1.2.5–1.2.8, book p. 31–35):

• T/^c F_v (contraction) — extracted term becomes a "deeper copy" labelling the leaf left by edge-contraction; visible to semantics, cancelled at PF
• T/^d F_v (deletion) — edge-contracted, no trace marker carried
• T/^ρ F_v (admissible cut) — an unlabeled structural vertex remains as the trace; used by the combined process

These are three forms of the remainder tree after extraction, not three carrier choices for the SO type itself. In all three, the SO type's base alphabet is SO_0 = lexical items + syntactic features only.

Linglib makes a different choice. SyntacticObject := FreeCommMagma (LIToken ⊕ Nat) adds labeled, indexed trace markers to the base alphabet. This is structurally distinct from MCB's ^ρ form (where the trace is an unlabeled structural vertex in the remainder tree only). Linglib's encoding admits trace-bearing SOs at any stage of derivation, not just as remainders.

Why this divergence is here: chain-tracking ergonomics. The Nat index lets downstream code identify which mover produced a given trace, which is load-bearing for binding theory and reconstruction effects. MCB handles chain-identification at the workspace level (a workspace forest may have multiple connected components that are isomorphic to the same tree, and those isomorphism classes are the chain). Linglib's chain-tracking-via-index is expressively sufficient but inexpressively redundant w.r.t. MCB.

Phase 2+ migration target: replace LIToken ⊕ Nat with LIToken and move chain-identification to the workspace layer. All current .trace / .isTrace / mkTrace / Step.im operations become projection-side rather than substrate. See project memory note project_so_carrier_rho_projection.md.

The migration from the prior planar TraceTree LIToken Nat carrier landed at version 0.230.857 (Phase 0.5 substrate) + 0.230.858 (mathlib-canonical DecidableEq via CommEqv, no LinearOrder needed). See docs/nonplanar-migration-plan.md and Linglib/Scratch/PreLiePlanarCheck.lean (counterexample showing the §1.7 pre-Lie identity is FALSE on planar trees, the headline reason for nonplanarity).

For LF composition, see SyntacticObject.toLFTree.

Equations

• Minimalist.SyntacticObject = FreeCommMagma (Minimalist.LIToken ⊕ ℕ)

@[reducible, inline]

abbrev Minimalist.SyntacticObject.leaf (tok : LIToken) : SyntacticObject

Leaf shim: SyntacticObject.leaf tok ≡ FreeCommMagma.of (.inl tok).

Equations

• Minimalist.SyntacticObject.leaf tok = FreeCommMagma.of (Sum.inl tok)

@[reducible, inline]

abbrev Minimalist.SyntacticObject.trace (n : ℕ) : SyntacticObject

Trace shim: SyntacticObject.trace n ≡ FreeCommMagma.of (.inr n).

Equations

• Minimalist.SyntacticObject.trace n = FreeCommMagma.of (Sum.inr n)

@[reducible, inline]

abbrev Minimalist.SyntacticObject.mul (l r : SyntacticObject) : SyntacticObject

Binary-Merge shim: SyntacticObject.mul l r ≡ l * r. The construction side of binary Merge; * is commutative on SyntacticObject.

Equations

• l.mul r = l * r

@[reducible, inline]

abbrev Minimalist.SyntacticObject.node (l r : SyntacticObject) : SyntacticObject

Construction-only alias .node l r ≡ mul l r ≡ l * r. Pattern matching against .node does NOT work (the carrier is Quot _, so Lean cannot invert through it); use induction so with | mul l r ihl ihr instead. Retained as a construction shim to keep call sites readable during the TraceTree → FreeCommMagma migration.

Equations

• l.node r = l.mul r

theorem Minimalist.SyntacticObject.ind {motive : SyntacticObject → Prop} (leaf : ∀ (tok : LIToken), motive (leaf tok)) (trace : ∀ (n : ℕ), motive (trace n)) (mul : ∀ (l r : SyntacticObject), motive l → motive r → motive (l * r)) (so : SyntacticObject) : motive so

The induction principle for SyntacticObject with linguistic case names. For Prop motives, Quot.ind propagates through the equivalence automatically — no swap-respect obligation needed. The mul case must cover both orderings (since l * r = r * l), which Quot.ind handles transparently for propositional motives.

theorem Minimalist.SyntacticObject.ind₂ {motive : SyntacticObject → SyntacticObject → Prop} (h : ∀ (a b : FreeMagma (LIToken ⊕ ℕ)), motive (Quot.mk FreeMagma.CommRel a) (Quot.mk FreeMagma.CommRel b)) (s t : SyntacticObject) : motive s t

Two-argument version of ind. Useful for theorems about pairs of SOs.

Predicates

Each predicate is defined via FreeCommMagma.lift from a swap-respecting helper on the underlying FreeMagma. The _leaf / _trace / _mul simp lemmas unfold cleanly.

def Minimalist.SyntacticObject.isLeaf : SyntacticObject → Prop

Equations

• Minimalist.SyntacticObject.isLeaf = FreeCommMagma.lift Minimalist.SyntacticObject.isLeafAux✝ Minimalist.SyntacticObject.isLeafAux_respects✝

@[simp]

theorem Minimalist.SyntacticObject.isLeaf_leaf (tok : LIToken) : (leaf tok).isLeaf ↔ True

@[simp]

theorem Minimalist.SyntacticObject.isLeaf_trace (n : ℕ) : (trace n).isLeaf ↔ True

@[simp]

theorem Minimalist.SyntacticObject.isLeaf_mul (l r : SyntacticObject) : ¬(l * r).isLeaf

@[implicit_reducible]

instance Minimalist.SyntacticObject.instDecidablePredIsLeaf : DecidablePred isLeaf

Equations

• so.instDecidablePredIsLeaf = Quot.recOnSubsingleton so fun (fm : FreeMagma (Minimalist.LIToken ⊕ ℕ)) => match fm with | FreeMagma.of a => isTrue trivial | a.mul a_1 => isFalse ⋯

def Minimalist.SyntacticObject.isNode : SyntacticObject → Prop

Equations

• Minimalist.SyntacticObject.isNode = FreeCommMagma.lift Minimalist.SyntacticObject.isNodeAux✝ Minimalist.SyntacticObject.isNodeAux_respects✝

@[simp]

theorem Minimalist.SyntacticObject.isNode_leaf (tok : LIToken) : ¬(leaf tok).isNode

@[simp]

theorem Minimalist.SyntacticObject.isNode_trace (n : ℕ) : ¬(trace n).isNode

@[simp]

theorem Minimalist.SyntacticObject.isNode_mul (l r : SyntacticObject) : (l * r).isNode

@[implicit_reducible]

instance Minimalist.SyntacticObject.instDecidablePredIsNode : DecidablePred isNode

Equations

• so.instDecidablePredIsNode = Quot.recOnSubsingleton so fun (fm : FreeMagma (Minimalist.LIToken ⊕ ℕ)) => match fm with | FreeMagma.of a => isFalse ⋯ | a.mul a_1 => isTrue trivial

def Minimalist.SyntacticObject.getLIToken : SyntacticObject → Option LIToken

Equations

• Minimalist.SyntacticObject.getLIToken = FreeCommMagma.lift Minimalist.SyntacticObject.getLITokenAux✝ Minimalist.SyntacticObject.getLITokenAux_respects✝

@[simp]

theorem Minimalist.SyntacticObject.getLIToken_leaf (tok : LIToken) : (leaf tok).getLIToken = some tok

@[simp]

theorem Minimalist.SyntacticObject.getLIToken_trace (n : ℕ) : (trace n).getLIToken = none

@[simp]

theorem Minimalist.SyntacticObject.getLIToken_mul (l r : SyntacticObject) : (l * r).getLIToken = none

@[reducible, inline]

abbrev Minimalist.liftFM {β : Type u_1} (f : FreeMagma (LIToken ⊕ ℕ) → β) (h : ∀ (a b : FreeMagma (LIToken ⊕ ℕ)), a.CommRel b → f a = f b) : SyntacticObject → β

Cascade combinator: lift a FreeMagma (LIToken ⊕ Nat) → β aux to SyntacticObject → β, hiding the FreeMagma.CommRel machinery from Phenomena consumers. Same as FreeCommMagma.lift modulo the SO type ascription at the SO interface. The _respects hypothesis still has to be provided, but the type signature is consumer-friendly.

Lives at Minimalist.liftFM (sibling of leafShape below), not inside the SyntacticObject namespace — liftFM f h takes no SO self-argument, so dot notation wouldn't apply.

Equations

• Minimalist.liftFM f h = FreeCommMagma.lift f h

def Minimalist.merge (x y : SyntacticObject) : SyntacticObject

Merge: the fundamental structure-building operation. Equal to FreeCommMagma.mul and to (· * ·). Commutative: merge x y = merge y x as a strict equality on the quotient.

Equations

• Minimalist.merge x y = x * y

@[simp]

theorem Minimalist.merge_comm (x y : SyntacticObject) : merge x y = merge y x

Headline of the MCB Phase 1.0 nonplanar migration: Merge is symmetric on the FreeCommMagma carrier. merge x y = merge y x as strict equality on the quotient, per @cite{marcolli-chomsky-berwick-2025} Definition 1.1.1 (book p. 22) + Remark 1.1.2 (p. 23). The earlier planar TraceTree-based theorem merge_distinguishes_children (x ≠ y → merge x y ≠ merge y x) is now PROVABLY FALSE; this merge_comm lemma is what replaces it at the substrate level.

Available as a simp lemma so consumers can rewrite merge x y to merge y x (or vice versa) freely.

def Minimalist.validMerge (x y : SyntacticObject) : Prop

Equations

• Minimalist.validMerge x y = (x ≠ y)

def Minimalist.externalMerge (x y : SyntacticObject) (_h : x ≠ y) : SyntacticObject

Equations

• Minimalist.externalMerge x y _h = Minimalist.merge x y

def Minimalist.internalMerge (target mover : SyntacticObject) (_h : target ≠ mover) : SyntacticObject

Equations

• Minimalist.internalMerge target mover _h = Minimalist.merge mover target

def Minimalist.mkLeaf (cat : Cat) (sel : SelStack) (id : ℕ) : SyntacticObject

Create a leaf SO from category and selection

Equations

• Minimalist.mkLeaf cat sel id = Minimalist.SyntacticObject.leaf { item := Minimalist.LexicalItem.simple cat sel, id := id }

def Minimalist.mkLeafPhon (cat : Cat) (sel : SelStack) (phon : String) (id : ℕ) : SyntacticObject

Create a leaf SO with a phonological form

Equations

• Minimalist.mkLeafPhon cat sel phon id = Minimalist.SyntacticObject.leaf { item := Minimalist.LexicalItem.simple cat sel phon, id := id }

def Minimalist.uposToCat : UD.UPOS → Cat

Map UD UPOS tags to Minimalist categories.

This bridges the theory-neutral UD POS tags used in Core/Basic.lean and Fragments/ to the Minimalist Cat system.

Equations

• Minimalist.uposToCat UD.UPOS.VERB = Minimalist.Cat.V
• Minimalist.uposToCat UD.UPOS.AUX = Minimalist.Cat.T
• Minimalist.uposToCat UD.UPOS.NOUN = Minimalist.Cat.N
• Minimalist.uposToCat UD.UPOS.PROPN = Minimalist.Cat.N
• Minimalist.uposToCat UD.UPOS.ADJ = Minimalist.Cat.A
• Minimalist.uposToCat UD.UPOS.ADP = Minimalist.Cat.P
• Minimalist.uposToCat UD.UPOS.DET = Minimalist.Cat.D
• Minimalist.uposToCat UD.UPOS.SCONJ = Minimalist.Cat.C
• Minimalist.uposToCat UD.UPOS.CCONJ = Minimalist.Cat.C
• Minimalist.uposToCat x✝ = Minimalist.Cat.N

Linearization-dependent operations (Phase 1.0 placeholder)

phonYield, linearize, leftmostLeaf, outerCat traverse the SO in planar order, which is a representative-choice over the unordered quotient. Per @cite{marcolli-chomsky-berwick-2025} Remark 1.1.2 (book p. 23), linearization belongs to Externalization, not to Merge proper.

Phase 1.0 placeholder: pick an arbitrary representative via Quot.out and traverse it on the underlying FreeMagma. Noncomputable because Quot.out uses Classical.choose. Phase 2 of the migration replaces this with a head-marking + head-directionality parameter (LCA), making linearization a parameterized choice rather than an arbitrary one.

def Minimalist.mkTraceToken (index : ℕ) : LIToken

Trace marker token: synthesized when traversal needs an LIToken at a .trace n position. Encodes the trace index in the id field (sentinel ≥ 10000), preserving backward-compat for code that inspects tok.id.

Equations

• Minimalist.mkTraceToken index = { item := Minimalist.LexicalItem.simple Minimalist.Cat.N [], id := index + 10000 }

def Minimalist.phonYieldPlanar : FreeMagma (LIToken ⊕ ℕ) → List String

Underlying phonological yield on a planar FreeMagma representative. Public so HeadFunction.phonYieldWith can compose it with a chosen externalize section.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.phonYieldPlanar (FreeMagma.of (Sum.inr val)) = []
• Minimalist.phonYieldPlanar (a.mul a_1) = Minimalist.phonYieldPlanar a ++ Minimalist.phonYieldPlanar a_1

def Minimalist.linearizePlanar : FreeMagma (LIToken ⊕ ℕ) → List LIToken

Underlying linearization on a planar FreeMagma representative. Public so HeadFunction.linearize can compose it with a chosen Section.σ for harmonic head-initial linearization.

Equations

• Minimalist.linearizePlanar (FreeMagma.of (Sum.inl tok)) = [tok]
• Minimalist.linearizePlanar (FreeMagma.of (Sum.inr val)) = []
• Minimalist.linearizePlanar (a.mul a_1) = Minimalist.linearizePlanar a ++ Minimalist.linearizePlanar a_1

def Minimalist.leftmostLeafPlanar : FreeMagma (LIToken ⊕ ℕ) → LIToken

Underlying leftmost-leaf on a planar FreeMagma representative. Exposed (not private) so HeadFunction.head can compose it with a chosen Section.σ for harmonic head-initial head extraction.

Equations

• Minimalist.leftmostLeafPlanar (FreeMagma.of (Sum.inl tok)) = tok
• Minimalist.leftmostLeafPlanar (FreeMagma.of (Sum.inr val)) = Minimalist.mkTraceToken val
• Minimalist.leftmostLeafPlanar (a.mul a_1) = Minimalist.leftmostLeafPlanar a

def Minimalist.rightmostLeafPlanar : FreeMagma (LIToken ⊕ ℕ) → LIToken

Underlying rightmost-leaf on a planar FreeMagma representative. Mirror of leftmostLeafPlanar for harmonic head-final convention (per @cite{marcolli-chomsky-berwick-2025} Lemma 1.13.5).

Equations

• Minimalist.rightmostLeafPlanar (FreeMagma.of (Sum.inl tok)) = tok
• Minimalist.rightmostLeafPlanar (FreeMagma.of (Sum.inr val)) = Minimalist.mkTraceToken val
• Minimalist.rightmostLeafPlanar (a.mul a_1) = Minimalist.rightmostLeafPlanar a_1

def Minimalist.LIToken.phonForm (tok : LIToken) : String

Extract the phonological form from an LIToken.

Equations

• tok.phonForm = (Option.map (fun (x : Minimalist.SimpleLI) => x.phonForm) tok.item.features.head?).getD ""

theorem Minimalist.phonYield_eq_linearize_planar (fm : FreeMagma (LIToken ⊕ ℕ)) : phonYieldPlanar fm = List.filterMap (fun (tok : LIToken) => have p := tok.phonForm; if p.isEmpty = true then none else some p) (linearizePlanar fm)

Underlying agreement on a planar representative: phonYield is the non-empty-phonForm filter of linearize. Used as a lemma for any HeadFunction h consumer that wants to relate h.phonYield to h.linearize.

def Minimalist.mkTrace (index : ℕ) : SyntacticObject

Create a trace SO with binding index index. Detectable via isTrace.

Equations

• Minimalist.mkTrace index = Minimalist.SyntacticObject.trace index

def Minimalist.isTrace : SyntacticObject → Option ℕ

Equations

• Minimalist.isTrace = FreeCommMagma.lift Minimalist.isTraceAux✝ Minimalist.isTraceAux_respects✝

@[simp]

theorem Minimalist.isTrace_leaf (tok : LIToken) : isTrace (SyntacticObject.leaf tok) = none

@[simp]

theorem Minimalist.isTrace_trace (n : ℕ) : isTrace (SyntacticObject.trace n) = some n

@[simp]

theorem Minimalist.isTrace_mul (l r : SyntacticObject) : isTrace (l * r) = none

def Minimalist.exampleVerb : SyntacticObject

Equations

• Minimalist.exampleVerb = Minimalist.mkLeaf Minimalist.Cat.V [Minimalist.Cat.D] 1

def Minimalist.exampleNoun : SyntacticObject

Equations

• Minimalist.exampleNoun = Minimalist.mkLeaf Minimalist.Cat.N [] 2

def Minimalist.exampleDet : SyntacticObject

Equations

• Minimalist.exampleDet = Minimalist.mkLeaf Minimalist.Cat.D [Minimalist.Cat.N] 3

def Minimalist.SyntacticObject.nodeCount : SyntacticObject → ℕ

Equations

• Minimalist.SyntacticObject.nodeCount = FreeCommMagma.lift Minimalist.nodeCountAux✝ Minimalist.nodeCountAux_respects✝

@[simp]

theorem Minimalist.SyntacticObject.nodeCount_leaf (tok : LIToken) : (leaf tok).nodeCount = 0

@[simp]

theorem Minimalist.SyntacticObject.nodeCount_trace (n : ℕ) : (trace n).nodeCount = 0

@[simp]

theorem Minimalist.SyntacticObject.nodeCount_mul (l r : SyntacticObject) : (l * r).nodeCount = 1 + l.nodeCount + r.nodeCount

def Minimalist.SyntacticObject.leafCount : SyntacticObject → ℕ

Equations

• Minimalist.SyntacticObject.leafCount = FreeCommMagma.lift Minimalist.leafCountAux✝ Minimalist.leafCountAux_respects✝

@[simp]

theorem Minimalist.SyntacticObject.leafCount_leaf (tok : LIToken) : (leaf tok).leafCount = 1

@[simp]

theorem Minimalist.SyntacticObject.leafCount_trace (n : ℕ) : (trace n).leafCount = 1

@[simp]

theorem Minimalist.SyntacticObject.leafCount_mul (l r : SyntacticObject) : (l * r).leafCount = l.leafCount + r.leafCount

theorem Minimalist.leaf_node_relation (so : SyntacticObject) : so.leafCount = so.nodeCount + 1

Subtree enumeration — Multiset (MCB-faithful)

Two operators, distinguished by whether the root is included:

• subtrees : SO → Multiset SO — all subtrees including the root. Useful for membership tests like "is x an internal node of s".
• Acc : SO → Multiset SO — accessible-terms-only (excludes the root). This is MCB's Acc(T) from Def 1.2.2 (book p. 28). Eq (1.2.5) #V(F) = b₀(F) + #Acc(F) only holds for the proper-accessible-terms version. Internal vertices (V_int(T)) by MCB's definition exclude the root.

Both are Multiset-valued (multiplicity-preserving) because MCB §1.6/§1.7 counting and the pre-Lie matching coefficient c^T_{T_1,T_2} (book p. 79) require multiplicities. For linglib's typical use (distinct-LIToken.id leaves), each subtree is a distinct value, so Multiset and Finset coincide extensionally — but the substrate commits to Multiset for faithfulness.

Multiset addition (+) preserves multiplicity (additive union); cons (::ₘ) adds an element regardless of presence.

def Minimalist.SyntacticObject.subtrees : SyntacticObject → Multiset SyntacticObject

All subtrees of a SyntacticObject, including the root itself. Returns a Multiset (multiplicity-preserving). For the MCB accessible-terms operator that excludes the root, see Acc below. Computable via FreeCommMagma.lift from a swap-respecting helper.

Equations

• Minimalist.SyntacticObject.subtrees = FreeCommMagma.lift Minimalist.subtreesAux✝ Minimalist.subtreesAux_respects✝

@[simp]

theorem Minimalist.SyntacticObject.subtrees_leaf (tok : LIToken) : (leaf tok).subtrees = {leaf tok}

@[simp]

theorem Minimalist.SyntacticObject.subtrees_trace (n : ℕ) : (trace n).subtrees = {trace n}

@[simp]

theorem Minimalist.SyntacticObject.subtrees_mul (l r : SyntacticObject) : (l * r).subtrees = l * r ::ₘ (l.subtrees + r.subtrees)

def Minimalist.SyntacticObject.Acc (so : SyntacticObject) : Multiset SyntacticObject

MCB's accessible-terms operator Acc(T) (Def 1.2.2, book p. 28): the multiset of all proper subtrees of T, excluding the root. Defined as subtrees - {self} (Multiset difference subtracts one occurrence). This is the operator that satisfies the MCB vertex-counting identity #V(F) = b₀(F) + #Acc(F) (eq. 1.2.5).

Equations

• so.Acc = so.subtrees - {so}

@[simp]

theorem Minimalist.SyntacticObject.Acc_leaf (tok : LIToken) : (leaf tok).Acc = 0

@[simp]

theorem Minimalist.SyntacticObject.Acc_trace (n : ℕ) : (trace n).Acc = 0

Terminal nodes — planar List (order matters for LCA)

terminalNodes returns a List because the leftmost-to-rightmost order is the input to LCA-derived linearization. Phase 1.0 placeholder via Quot.out (planar representative); Phase 2 will replace with LCA + head-directionality.

def Minimalist.terminalNodesPlanar : FreeMagma (LIToken ⊕ ℕ) → List (FreeMagma (LIToken ⊕ ℕ))

Underlying terminal-node enumeration on a planar FreeMagma representative. Public so HeadFunction.terminalNodesWith can compose it with a chosen externalize section.

Equations

• Minimalist.terminalNodesPlanar (FreeMagma.of a) = [FreeMagma.of a]
• Minimalist.terminalNodesPlanar (l.mul r) = Minimalist.terminalNodesPlanar l ++ Minimalist.terminalNodesPlanar r

noncomputable def Minimalist.terminalNodes (so : SyntacticObject) : List SyntacticObject

The terminal (leaf-position) SOs of a SyntacticObject. Order depends on the chosen planar representative.

Equations

• Minimalist.terminalNodes so = List.map (Quot.mk FreeMagma.CommRel) (Minimalist.terminalNodesPlanar (Quot.out so))

theorem Minimalist.terminalNodes_are_leaves {so t : SyntacticObject} (h : t ∈ terminalNodes so) : t.isLeaf

Every terminal node is leaf-position.

@[simp]

theorem Minimalist.terminalNodes_leaf (tok : LIToken) : terminalNodes (SyntacticObject.leaf tok) = [SyntacticObject.leaf tok]

For a leaf SO, terminalNodes is the singleton list [.leaf tok]. Same singleton-class argument as leftmostLeaf_leaf.

theorem Minimalist.terminalNodes_sub_subtrees {so t : SyntacticObject} (h : t ∈ terminalNodes so) : t ∈ so.subtrees

Every terminal is a subtree.

theorem Minimalist.self_mem_subtrees (so : SyntacticObject) : so ∈ so.subtrees

The root is always in its own subtrees.

theorem Minimalist.subtrees_subset_of_mem {t s : SyntacticObject} (h : t ∈ s.subtrees) : t.subtrees ⊆ s.subtrees

subtrees is downward-monotone along the subtree relation: if t is a subtree of s (at any multiplicity), then every subtree of t is also a subtree of s (Multiset.Subset ignores multiplicity, only membership).

def Minimalist.immediatelyContains (x y : SyntacticObject) : Prop

Equations

• Minimalist.immediatelyContains x y = FreeCommMagma.lift (Minimalist.immediatelyContainsAux✝ y) ⋯ x

@[simp]

theorem Minimalist.immediatelyContains_leaf (tok : LIToken) (y : SyntacticObject) : ¬immediatelyContains (SyntacticObject.leaf tok) y

@[simp]

theorem Minimalist.immediatelyContains_trace (n : ℕ) (y : SyntacticObject) : ¬immediatelyContains (SyntacticObject.trace n) y

@[simp]

theorem Minimalist.immediatelyContains_mul (l r y : SyntacticObject) : immediatelyContains (l * r) y ↔ y = l ∨ y = r

@[implicit_reducible]

instance Minimalist.decImmediatelyContains (x y : SyntacticObject) : Decidable (immediatelyContains x y)

Decidable immediate containment. Recurses via Quot.recOnSubsingleton on the underlying FreeMagma representative.

Equations

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

inductive Minimalist.contains : SyntacticObject → SyntacticObject → Prop

Containment is the transitive closure of immediate containment

"X contains Y iff X immediately contains Y or X immediately contains some SO Z such that Z contains Y"

This is standard syntactic dominance.

• imm (x y : SyntacticObject) : immediatelyContains x y → contains x y
• trans (x y z : SyntacticObject) : immediatelyContains x z → contains z y → contains x y

theorem Minimalist.imm_implies_contains {x y : SyntacticObject} (h : immediatelyContains x y) : contains x y

Immediate containment implies containment

theorem Minimalist.contains_trans {x y z : SyntacticObject} (hxy : contains x y) (hyz : contains y z) : contains x z

Containment is transitive

theorem Minimalist.leaf_contains_nothing (tok : LIToken) (y : SyntacticObject) : ¬contains (SyntacticObject.leaf tok) y

Leaves contain nothing

theorem Minimalist.trace_contains_nothing (n : ℕ) (y : SyntacticObject) : ¬contains (SyntacticObject.trace n) y

Trace markers contain nothing.

theorem Minimalist.immediatelyContains_lt_nodeCount {x y : SyntacticObject} (h : immediatelyContains x y) : y.nodeCount < x.nodeCount

Immediate containment strictly decreases nodeCount

theorem Minimalist.contains_lt_nodeCount {x y : SyntacticObject} (h : contains x y) : y.nodeCount < x.nodeCount

Containment strictly decreases nodeCount

theorem Minimalist.contains_irrefl (x : SyntacticObject) : ¬contains x x

No element contains itself (containment is irreflexive)

@[implicit_reducible]

instance Minimalist.decContains (x y : SyntacticObject) : Decidable (contains x y)

Containment is decidable by structural recursion on the containing SO's underlying FreeMagma representative (via Quot.recOnSubsingleton — Decidable p is a subsingleton up to propositional equality).

Equations

• Minimalist.decContains x y = Quot.recOnSubsingleton x fun (a : FreeMagma (Minimalist.LIToken ⊕ ℕ)) => Minimalist.decContainsAux✝ y a

def Minimalist.isTermOf (x y : SyntacticObject) : Prop

X is a term of Y iff X = Y or Y contains X

"X is a term of SO Y iff X = Y or Y contains X"

This is useful for stating when an element is "somewhere in" a structure

Equations

• Minimalist.isTermOf x y = (x = y ∨ Minimalist.contains y x)

theorem Minimalist.self_is_term (x : SyntacticObject) : isTermOf x x

Every SO is a term of itself

theorem Minimalist.contained_is_term {x y : SyntacticObject} (h : contains y x) : isTermOf x y

If Y contains X, then X is a term of Y

@[implicit_reducible]

instance Minimalist.decIsTermOf (x y : SyntacticObject) : Decidable (isTermOf x y)

Equations

• Minimalist.decIsTermOf x y = id inferInstance

def Minimalist.containsOrEq (x y : SyntacticObject) : Prop

Reflexive containment (useful for stating constraints)

Equations

• Minimalist.containsOrEq x y = (x = y ∨ Minimalist.contains x y)

@[implicit_reducible]

instance Minimalist.decContainsOrEq (x y : SyntacticObject) : Decidable (containsOrEq x y)

Equations

• Minimalist.decContainsOrEq x y = id inferInstance

theorem Minimalist.refl_containsOrEq (x : SyntacticObject) : containsOrEq x x

Every SO reflexively contains itself

theorem Minimalist.containsOrEq_trans {x y z : SyntacticObject} (hxy : containsOrEq x y) (hyz : containsOrEq y z) : containsOrEq x z

Reflexive containment is transitive

Subtree-Finset ↔ containment bridge

These theorems relate subtrees : SO → Finset SO to the propositional contains/containsOrEq relations. With subtrees Finset-typed (order-blind, computable), the bridges are provable by induction — no Quot.out oracle dependence.

theorem Minimalist.mem_subtrees_of_imm_contains {root w z : SyntacticObject} (hw : w ∈ root.subtrees) (hwz : immediatelyContains w z) : z ∈ root.subtrees

Children of any subtree of root are themselves subtrees of root.

theorem Minimalist.mem_subtrees_of_contains {y z : SyntacticObject} (h : contains y z) : z ∈ y.subtrees

Containment implies subtree-Finset membership.

theorem Minimalist.isTermOf_of_mem_subtrees {y z : SyntacticObject} (h : z ∈ y.subtrees) : isTermOf z y

Subtree-Multiset membership implies term-of relation.

theorem Minimalist.isTermOf_iff_mem_subtrees (y z : SyntacticObject) : isTermOf z y ↔ z ∈ y.subtrees

isTermOf z y iff z is in y.subtrees. The bridge between the propositional term-of relation and the Finset-typed enumeration.

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

X and Y are sisters IN tree root: they are distinct co-daughters of some node that is a subtree of root.

Equations

• Minimalist.areSistersIn root x y = ∃ z ∈ root.subtrees, Minimalist.immediatelyContains z x ∧ Minimalist.immediatelyContains z y ∧ x ≠ y

@[implicit_reducible]

instance Minimalist.decAreSistersIn (root x y : SyntacticObject) : Decidable (areSistersIn root x y)

Equations

• Minimalist.decAreSistersIn root x y = Multiset.decidableExistsMultiset

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

X c-commands Y IN tree root: X has a sister (in root) that contains-or-equals Y.

Equations

• Minimalist.cCommandsIn root x y = ∃ z ∈ root.subtrees, Minimalist.areSistersIn root x z ∧ Minimalist.containsOrEq z y

@[implicit_reducible]

instance Minimalist.decCCommandsIn (root x y : SyntacticObject) : Decidable (cCommandsIn root x y)

cCommandsIn is decidable: bounded existential over root.subtrees (Multiset). Computable since subtrees is.

Equations

• Minimalist.decCCommandsIn root x y = Multiset.decidableExistsMultiset

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

X asymmetrically c-commands Y in tree root.

Equations

• Minimalist.asymCCommandsIn root x y = (Minimalist.cCommandsIn root x y ∧ ¬Minimalist.cCommandsIn root y x)

@[implicit_reducible]

instance Minimalist.decAsymCCommandsIn (root x y : SyntacticObject) : Decidable (asymCCommandsIn root x y)

Equations

• Minimalist.decAsymCCommandsIn root x y = id inferInstance

Note on Barker-Pullum command relations

An earlier draft of this file recast cCommandsIn as B&P K-command (Core.Order.commandRelation over FreeMagma.toTree's tree-order), aiming to inherit B&P's antitonicity / intersection theorems "for free" in the same lattice as HPSG o-command and DG d-command.

That recast does not work: B&P's commandRelation is universal ("every branching ancestor of α also dominates β") and admits pairs that sister-form c-command excludes — e.g., on tree (a, (b, c)), the leaf a B&P-commands itself and the root, since the only branching strict ancestor is the root, which trivially dominates everything. Reinhart c-command is sister-form (∃ sister of α containing β); the two relations are not biconditionally equivalent on FreeMagma.

The mathlib-style resolution: keep cCommandsIn value-side and sister-form (it's what binding consumers need, and it reads directly off bare phrase structure per @cite{marcolli-chomsky-berwick-2025}). Cross-tradition unification via B&P's parametric command lives in Core/Order/Command.lean and is exercised by HPSG / DG, where its universal shape matches the native primitive. Minimalism's c-command does not reduce to it, so no bridge belongs here.

Multiset shape — abstract geometry over the nonplanar quotient

The unlabeled SO shape: replace every leaf token / trace marker with (). The result lives in FreeCommMagma Unit — the canonical nonplanar analog of the prior planar TreeShape (which was deleted because .node L R = .node R L failed to hold under MCB §1.1.3, book p. 23). Two SOs are structurally isomorphic iff their shapes are equal as elements of FreeCommMagma Unit.

def Minimalist.SyntacticObject.shape : SyntacticObject → FreeCommMagma Unit

The unlabeled multiset-shape of an SO: forget every leaf token and trace marker, keeping only the binary-tree structure modulo nonplanar quotient. Functorial via FreeCommMagma.map.

Equations

• Minimalist.SyntacticObject.shape = ⇑(FreeCommMagma.map (Function.const (Minimalist.LIToken ⊕ ℕ) ()))

@[reducible, inline]

abbrev Minimalist.leafShape : FreeCommMagma Unit

The unit shape — a single leaf in FreeCommMagma Unit. Useful abbreviation for stating shape equalities like so.shape = leafShape * (leafShape * leafShape). Was previously duplicated as private def leafShape in three Phenomena Studies files (DendikkenBasic, HaddicanEtAl, Causatives); hoisted to substrate to eliminate the triplicate.

Equations

• Minimalist.leafShape = FreeCommMagma.of ()

@[simp]

theorem Minimalist.SyntacticObject.shape_leaf (tok : LIToken) : (leaf tok).shape = FreeCommMagma.of ()

@[simp]

theorem Minimalist.SyntacticObject.shape_trace (n : ℕ) : (trace n).shape = FreeCommMagma.of ()

@[simp]

theorem Minimalist.SyntacticObject.shape_mul (l r : SyntacticObject) : (l * r).shape = l.shape * r.shape

def Minimalist.structurallyIsomorphic (x y : SyntacticObject) : Prop

Two SOs are structurally isomorphic iff they have the same nonplanar shape (ignoring all leaf labels). Replaces the prior Bool-valued structurallyIsomorphic from the planar substrate; Prop-valued + DecidableEq is more mathlib-aligned.

Equations

• Minimalist.structurallyIsomorphic x y = (x.shape = y.shape)

@[implicit_reducible]

instance Minimalist.instDecidableStructurallyIsomorphic (x y : SyntacticObject) : Decidable (structurallyIsomorphic x y)

Equations

• Minimalist.instDecidableStructurallyIsomorphic x y = id inferInstance

Y-model branch to LF

The LF lift SyntacticObject.toLFTree : SyntacticObject → Tree Unit String lives in Theories/Syntax/Minimalism/SpellOut.lean, where trace detection and phonForm extraction are handled. PF (linearize / phonYield) operates natively on SyntacticObject and does not require a lift.