Quotient tree (Definition 2.5)

Given a tree T and a contained subtree Tᵥ, the quotient tree T/Tᵥ is obtained by replacing Tᵥ with a single leaf (contracting the subtree to a point).

def Minimalism.quotientTree (T v : SyntacticObject) : Option SyntacticObject

Quotient tree: replace the first occurrence of v in T with a leaf. Returns none if v is not found in T.

Equations

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

theorem Minimalism.quotientTree_some_of_contains (T v : SyntacticObject) (h : contains T v) : (quotientTree T v).isSome = true

If v is contained in T, quotientTree succeeds

theorem Minimalism.quotientTree_leafCount (T v q : SyntacticObject) (h : contains T v) (hq : quotientTree T v = some q) : q.leafCount = T.leafCount - v.leafCount + 1

Admissible cuts (§2.2)

An admissible cut is a set of internal nodes such that no two are in an ancestor-descendant relation (i.e., they are pairwise incomparable under containment).

structure Minimalism.AdmissibleCut (so : SyntacticObject) : Type

Admissible cut: a finite set of nodes that form an antichain under containment. Uses mathlib's IsAntichain — s.Pairwise rᶜ — to express pairwise incomparability.

• cutNodes : Finset SyntacticObject
• contained (n : SyntacticObject) : n ∈ self.cutNodes → contains so n

  All cut nodes are proper subtrees of so

• admissible : IsAntichain contains ↑self.cutNodes

  Cut nodes are pairwise incomparable (no ancestor-descendant pairs)

def Minimalism.trivialCut (so : SyntacticObject) : AdmissibleCut so

The trivial cut: empty set of cut nodes

Equations

• Minimalism.trivialCut so = { cutNodes := ∅, contained := ⋯, admissible := Minimalism.trivialCut._proof_2 }

def Minimalism.numAdmissibleCuts (so : SyntacticObject) : ℕ

Number of admissible cuts

Equations

• Minimalism.numAdmissibleCuts (Minimalism.SyntacticObject.leaf a) = 1
• Minimalism.numAdmissibleCuts (a.node b) = Minimalism.numAdmissibleCuts a * Minimalism.numAdmissibleCuts b + 1

Leading coproduct (equation 2.16)

The leading coproduct Δ₍₂₎(T) extracts each proper subtree Tᵥ and pairs it with the quotient T/Tᵥ:

Δ₍₂₎(T) = Σ_{v ∈ V_int} Tᵥ ⊗ T/Tᵥ

This is the "first-order" term of the full Connes-Kreimer coproduct.

def Minimalism.leadingCoproduct (T : SyntacticObject) : List (SyntacticObject × Option SyntacticObject)

Leading coproduct: pairs (subtree, quotient) for each internal node subtree

Equations

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

theorem Minimalism.coproduct_size_identity (T v q : SyntacticObject) (hc : contains T v) (hq : quotientTree T v = some q) : T.leafCount = v.leafCount + q.leafCount - 1

Coproduct size identity: T.leafCount = v.leafCount + (T/v).leafCount - 1

This is the key size conservation law for the coproduct decomposition. It says that cutting a tree into a subtree and quotient preserves the total "weight" up to the shared boundary.

Merge on workspaces (Definition 2.10)

Merge lifts from an operation on pairs of SOs to an operation on the workspace (list of SOs). The algebraic formulation uses the coproduct to identify which subterms can be re-merged (Internal Merge) or combines distinct workspace members (External Merge).

def Minimalism.listExternalMerge (T₁ T₂ : SyntacticObject) (F : List SyntacticObject) : List SyntacticObject

External Merge on workspace: combine two members into one

Equations

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

def Minimalism.listInternalMerge (T β : SyntacticObject) (F : List SyntacticObject) : List SyntacticObject

Internal Merge on workspace: re-merge a contained subterm

Equations

• Minimalism.listInternalMerge T β F = Minimalism.merge β T :: List.filter (fun (x : Minimalism.SyntacticObject) => x != T) F

theorem Minimalism.list_em_contains_merge (T₁ T₂ : SyntacticObject) (F : List SyntacticObject) : merge T₁ T₂ ∈ listExternalMerge T₁ T₂ F

External Merge on workspaces produces a workspace containing merge(T₁, T₂)

theorem Minimalism.list_im_contains_merge (T β : SyntacticObject) (F : List SyntacticObject) : merge β T ∈ listInternalMerge T β F

Internal Merge on workspaces produces a workspace containing merge(β, T)

theorem Minimalism.workspace_merge_recovers_merge (T₁ T₂ : SyntacticObject) : merge T₁ T₂ ∈ listExternalMerge T₁ T₂ [T₁, T₂]

The workspace merge operation reduces to pointwise merge on SOs. This is the key theorem that the algebraic (Hopf algebra) formulation recovers the simple set-theoretic Merge operation.

theorem Minimalism.workspace_merge_partition (α β : SyntacticObject) (_hne : α ≠ β) (F : List SyntacticObject) (_hα : α ∈ F) : (¬contains α β ∧ ¬contains β α → merge α β ∈ listExternalMerge α β F) ∧ (contains α β → merge β α ∈ listInternalMerge α β F)

Connection to MergeUnification: the EM/IM workspace operations align with the containment-based partition. When inputs are incomparable, listExternalMerge is the appropriate operation; when one contains the other, listInternalMerge is appropriate.