Readings as cuts of the copy object

import Linglib.Syntax.Minimalist.Copy.Cut · namespace Minimalist.LinearizedSyntacticObject.Marked

This file relates the readings of a marked object to the coproducts on trees. A reading cuts a forest from the copy object: the lower copies of the chains read high, each leaving its trace, and the higher copies of the chains read low, each leaving nothing, with the unary vertex that leaves contracted. With no chain read low the reading is a term of the coproduct $\Delta^c$, and with every chain read low a term of the deletion coproduct $\Delta^d$. A reading with chains of both kinds is a cut under a policy of its own, which pruning follows on some trees and extractC on the rest.

Implementation notes

Δ^c labels a trace by a function of the tree it cuts, where a replay gives a lower copy the mark of its mover's contraction at that step, so MarkedBy is a hypothesis on the object.

TODO

Prove MarkedBy of termTrace selHead for the objects a replay reaches, under conditions on the moved heads.
Characterize cutForest by the positions it cuts.

References

Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized

Declarations

Readings and the coproducts

A reading gives a cut of the copy object under its policy, its unary vertices contracted.

theorem exists_mem_cutSummandsG_lf L321–335

{τ : UnorderedTree SyntacticObject.Vertex → Option LexicalItem.Token} (t : Marked) (low : Finset SyntacticObject) (hroot : (↑t).value.1 = none) (hτ : MarkedBy τ ↑t) :

∃ (T : RoseTree SyntacticObject.Vertex), (t.cutForest low, T) ∈ ConnesKreimer.cutSummandsG (extractReading low (τ ∘ UnorderedTree.mk)) ↑t.unmark ∧ T.contractUnary = ↑(t.lf low)

Built from , ,

With no chain read low, a reading is the contraction, a term of the coproduct Δ^c: the lower copies are an admissible cut of the copy object.

theorem mem_cutSummandsCN_contract L337–352

{τ : UnorderedTree SyntacticObject.Vertex → Option LexicalItem.Token} (t : Marked) (hroot : (↑t).value.1 = none) (hτ : MarkedBy τ ↑t) :

(Multiset.map UnorderedTree.mk (t.cutForest ∅), UnorderedTree.mk ↑t.contract) ∈ ConnesKreimer.cutSummandsCN τ (UnorderedTree.mk ↑t.unmark)

Built from ,

With every chain read low, a reading is a term of the deletion coproduct Δ^d: the higher copies are an admissible cut of the copy object.

theorem mem_cutSummandsDN_lf L354–369

(t : Marked) (low : Finset SyntacticObject) (hlow : ∀ r ∈ (↑t).subtrees, Option.isSome r.value.1 = true → ReadLow low r) :

(Multiset.map UnorderedTree.mk (t.cutForest low), UnorderedTree.mk ↑(t.lf low)) ∈ ConnesKreimer.cutSummandsDN (UnorderedTree.mk ↑t.unmark)

Built from