Realization of colored trees

Pruning the colors of a theta structure gives the syntactic object it builds: lexically anchored leaves become lexical leaves, binary vertices become bare Merge, and the empty-tree marker is the unit of the magma, so that a movement landing site realizes to its host unchanged.

Main definitions

• realize: pruning to the SyntacticObject carrier, none playing the magma unit.

Main statements

• realize_node_emptyTree_right: the unit law, under which movement landing sites leave no mark on the realized object.
• realize_isSome: a tree with a lexically anchored input realizes.

References

• [ML25]

noncomputable def Minimalist.Theta.realize : Bud.Tree (Color LexicalItem.Token) → Option SyntacticObject

Prune a colored tree to the syntactic object it builds. Lexically anchored leaves become lexical leaves, vertices become bare Merge, and none is the magma unit, contributed by the empty-tree marker and, degenerately, by bare-grid leaves, which a tree with terminal inputs lacks.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Theta.realize (Bud.Tree.leaf (Minimalist.Theta.Color.lex tok g)) = some ↑tok
• Minimalist.Theta.realize (Bud.Tree.leaf c) = none

@[simp]

theorem Minimalist.Theta.realize_leaf_lex (tok : LexicalItem.Token) (g : List PolarizedRole) : realize (Bud.Tree.leaf (Color.lex tok g)) = some ↑tok

@[simp]

theorem Minimalist.Theta.realize_leaf_emptyTree : realize (Bud.Tree.leaf Color.emptyTree) = none

@[simp]

theorem Minimalist.Theta.realize_leaf_free (g : List PolarizedRole) : realize (Bud.Tree.leaf (Color.free g)) = none

theorem Minimalist.Theta.realize_node_some_some {l r : Bud.Tree (Color LexicalItem.Token)} {c : Color LexicalItem.Token} {L R : SyntacticObject} (hl : realize l = some L) (hr : realize r = some R) : realize (Bud.Tree.node c l r) = some (L.merge R)

@[simp]

theorem Minimalist.Theta.realize_node_emptyTree_right {x : Bud.Tree (Color LexicalItem.Token)} {c : Color LexicalItem.Token} : realize (Bud.Tree.node c x (Bud.Tree.leaf Color.emptyTree)) = realize x

The unit law M(T, 1) = T: a movement landing site realizes to its host unchanged, the empty-tree marker existing only for the coloring.

theorem Minimalist.Theta.realize_isSome {x : Bud.Tree (Color LexicalItem.Token)} (h : ∃ (tok : LexicalItem.Token) (g : List PolarizedRole), Color.lex tok g ∈ x.inputs) : (realize x).isSome = true

A tree with a lexically anchored input realizes to a syntactic object.