Colored Merge and realization

The bridge from the theta bud system to the syntactic-object carrier ([ML25]'s reinterpretation of theta filtering as colored structure formation). The compatibility relation on a colored binary Merge — the root and children colors form a generator — is ThetaLocal, and the colored Merge of derivable structures under a compatible root is derivable (derives_node_of_thetaLocal, via the bottom-up Bud.System.Derives.node): structure building through colored Merge stays within the theta-lawful language. realize prunes the colors, sending a colored tree to the SyntacticObject it builds — lexically anchored leaves become lexical leaves, binary nodes become bare Merge nodes, and the empty-tree marker is the magma unit, so a movement landing site realizes to its host unchanged (realize_node_emptyTree_right).

Main declarations

• derives_node_of_thetaLocal — colored Merge closure: joining derivable structures under a generator-compatible root color is derivable.
• realize — pruning to the SyntacticObject carrier, none playing the magma unit; intended on trees with terminal inputs, where none arises only from the empty-tree marker.
• realize_node_emptyTree_right — the unit law M(T, 1) = T: movement landing sites leave no mark on the realized object.
• realize_isSome — a tree with a lexically anchored input realizes.

theorem Minimalist.Theta.derives_node_of_thetaLocal {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} {c : Color L} {S S' : Bud.Tree (Color L)} (hΞ : ThetaLocal hier c S.out S'.out) (hS : (system hier).Derives S.out S) (hS' : (system hier).Derives S'.out S') : (system hier).Derives c (Bud.Tree.node c S S')

Colored Merge closure: joining two derivable structures under a root color that forms a generator with their output colors is derivable. Structure building by compatible colored Merge stays within the theta-lawful language.

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

Prune a colored tree to the syntactic object it builds: lexically anchored leaves become lexical leaves, nodes become bare Merge nodes, and none is the magma unit — contributed by the empty-tree marker (and, degenerately, by bare-grid leaves, which do not occur in trees with terminal inputs).

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 (Minimalist.SyntacticObject.lexLeaf tok)
• Minimalist.Theta.realize (Bud.Tree.leaf c) = none

@[simp]

theorem Minimalist.Theta.realize_leaf_lex (tok : LIToken) (g : List PolarizedRole) : realize (Bud.Tree.leaf (Color.lex tok g)) = some (SyntacticObject.lexLeaf 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 LIToken)} {c : Color LIToken} {L R : SyntacticObject} (hl : realize l = some L) (hr : realize r = some R) : realize (Bud.Tree.node c l r) = some (L.node R)

@[simp]

theorem Minimalist.Theta.realize_node_emptyTree_right {x : Bud.Tree (Color LIToken)} {c : Color LIToken} : 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 exists only for the coloring.

theorem Minimalist.Theta.realize_isSome {x : Bud.Tree (Color LIToken)} (h : ∃ (tok : LIToken) (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.