Theta theory as a coloring algorithm

Marcolli and Larson implement theta theory in the mathematical model of Minimalism as a coloring algorithm: structures freely formed by Merge are filtered by membership in the language of a bud generating system whose colors are theta grids, tuples of giver- or receiver-marked roles, and whose generators are the local theta-discharge configurations. A grid injected at a predicate's leaf propagates up the tree like a conserved quantity: at each generator one receiver peels off to the sister position, and the residue continues toward the maximal projection.

Main definitions

• PolarizedRole, Color: giver- and receiver-marked roles, and the colors, which are bare grids (nonterminal; the empty grid marks a non-theta position), lexically anchored grids (terminal), and the empty-tree marker.
• IsGen, ThetaLocal, system: the generator shapes, the cherries they license, and the complete theta bud system.
• comb: the bare theta combs, a complete grid discharged one role per vertex.
• SatisfiesCriterion: the theta criterion on a colored operation.

Main statements

• IsGen.conservation: each generator conserves theta roles.
• ThetaLocal.eq_nontheta: movement lands only in non-theta positions.
• comb_derivable: the bare combs are derivable in the complete system.
• derives_soleReceiver: in a movement-free derivable structure with a sole-receiver root, every position receives at most one role.

Implementation notes

The trees are planar, so each generator shape licenses its children in either order, and the theta criterion compares received roles with the head's grid as multisets.

References

• [ML25]
• [MCB25]
• [Gir19]

inductive Minimalist.Theta.Polarity : Type

Whether a role occurrence gives or receives, [ML25]'s marks θ↑ and θ↓.

• giver : Polarity
• receiver : Polarity

@[instance_reducible]

instance Minimalist.Theta.instDecidableEqPolarity : DecidableEq Polarity

Equations

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

@[instance_reducible]

instance Minimalist.Theta.instReprPolarity : Repr Polarity

Equations

• Minimalist.Theta.instReprPolarity = { reprPrec := Minimalist.Theta.instReprPolarity.repr }

def Minimalist.Theta.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

structure Minimalist.Theta.PolarizedRole : Type

A theta role marked as given or received.

• role : ArgumentStructure.ThetaRole
• polarity : Polarity

def Minimalist.Theta.instDecidableEqPolarizedRole.decEq (x✝ x✝¹ : PolarizedRole) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Minimalist.Theta.instDecidableEqPolarizedRole : DecidableEq PolarizedRole

Equations

• Minimalist.Theta.instDecidableEqPolarizedRole = Minimalist.Theta.instDecidableEqPolarizedRole.decEq

def Minimalist.Theta.instReprPolarizedRole.repr : PolarizedRole → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Theta.instReprPolarizedRole : Repr PolarizedRole

Equations

• Minimalist.Theta.instReprPolarizedRole = { reprPrec := Minimalist.Theta.instReprPolarizedRole.repr }

def Minimalist.Theta.PolarizedRole.up (ρ : ArgumentStructure.ThetaRole) : PolarizedRole

The giver occurrence θ↑.

Equations

• Minimalist.Theta.PolarizedRole.up ρ = { role := ρ, polarity := Minimalist.Theta.Polarity.giver }

def Minimalist.Theta.PolarizedRole.down (ρ : ArgumentStructure.ThetaRole) : PolarizedRole

The receiver occurrence θ↓.

Equations

• Minimalist.Theta.PolarizedRole.down ρ = { role := ρ, polarity := Minimalist.Theta.Polarity.receiver }

def Minimalist.Theta.upGrid (g : List ArgumentStructure.ThetaRole) : List PolarizedRole

A grid of giver occurrences, the undischarged residue a predicate carries.

Equations

• Minimalist.Theta.upGrid g = List.map Minimalist.Theta.PolarizedRole.up g

@[simp]

theorem Minimalist.Theta.upGrid_nil : upGrid [] = []

@[simp]

theorem Minimalist.Theta.down_notMem_upGrid {ρ : ArgumentStructure.ThetaRole} {g : List ArgumentStructure.ThetaRole} : PolarizedRole.down ρ ∉ upGrid g

@[simp]

theorem Minimalist.Theta.upGrid_append (g h : List ArgumentStructure.ThetaRole) : upGrid (g ++ h) = upGrid g ++ upGrid h

inductive Minimalist.Theta.Color (L : Type u_2) : Type u_2

A color is a bare grid (nonterminal, the empty grid being the non-theta marker θ0), a lexically anchored grid (terminal), or the empty-tree marker (1, θ0).

• free {L : Type u_2} (g : List PolarizedRole) : Color L
• lex {L : Type u_2} (item : L) (g : List PolarizedRole) : Color L
• emptyTree {L : Type u_2} : Color L

@[instance_reducible]

instance Minimalist.Theta.instDecidableEqColor {L✝ : Type u_2} [DecidableEq L✝] : DecidableEq (Color L✝)

Equations

• Minimalist.Theta.instDecidableEqColor = Minimalist.Theta.instDecidableEqColor.decEq

def Minimalist.Theta.instDecidableEqColor.decEq {L✝ : Type u_2} [DecidableEq L✝] (x✝ x✝¹ : Color L✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Theta.instDecidableEqColor.decEq (Minimalist.Theta.Color.free a) (Minimalist.Theta.Color.free b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalist.Theta.instDecidableEqColor.decEq (Minimalist.Theta.Color.free g) (Minimalist.Theta.Color.lex item g_1) = isFalse ⋯
• Minimalist.Theta.instDecidableEqColor.decEq (Minimalist.Theta.Color.free g) Minimalist.Theta.Color.emptyTree = isFalse ⋯
• Minimalist.Theta.instDecidableEqColor.decEq (Minimalist.Theta.Color.lex item g) (Minimalist.Theta.Color.free g_1) = isFalse ⋯
• Minimalist.Theta.instDecidableEqColor.decEq (Minimalist.Theta.Color.lex item g) Minimalist.Theta.Color.emptyTree = isFalse ⋯
• Minimalist.Theta.instDecidableEqColor.decEq Minimalist.Theta.Color.emptyTree (Minimalist.Theta.Color.free g) = isFalse ⋯
• Minimalist.Theta.instDecidableEqColor.decEq Minimalist.Theta.Color.emptyTree (Minimalist.Theta.Color.lex item g) = isFalse ⋯
• Minimalist.Theta.instDecidableEqColor.decEq Minimalist.Theta.Color.emptyTree Minimalist.Theta.Color.emptyTree = isTrue ⋯

@[instance_reducible]

instance Minimalist.Theta.instReprColor {L✝ : Type u_2} [Repr L✝] : Repr (Color L✝)

Equations

• Minimalist.Theta.instReprColor = { reprPrec := Minimalist.Theta.instReprColor.repr }

def Minimalist.Theta.instReprColor.repr {L✝ : Type u_2} [Repr L✝] : Color L✝ → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Minimalist.Theta.Color.nontheta {L : Type u_1} : Color L

The non-theta marker θ0, the empty grid.

Equations

• Minimalist.Theta.Color.nontheta = Minimalist.Theta.Color.free []

def Minimalist.Theta.Color.IsTerminal {L : Type u_1} : Color L → Prop

The terminal colors are the lexically anchored grids and the empty-tree marker.

Equations

• (Minimalist.Theta.Color.free g).IsTerminal = False
• (Minimalist.Theta.Color.lex item g).IsTerminal = True
• Minimalist.Theta.Color.emptyTree.IsTerminal = True

@[simp]

theorem Minimalist.Theta.Color.isTerminal_free {L : Type u_1} {g : List PolarizedRole} : ¬(free g).IsTerminal

def Minimalist.Theta.Color.grid? {L : Type u_1} : Color L → Option (List PolarizedRole)

The grid a color carries, if any; lexical anchoring is transparent to theta structure.

Equations

• (Minimalist.Theta.Color.free g).grid? = some g
• (Minimalist.Theta.Color.lex item g).grid? = some g
• Minimalist.Theta.Color.emptyTree.grid? = none

def Minimalist.Theta.Color.Matches {L : Type u_1} (c : Color L) (g : List PolarizedRole) : Prop

The color carries exactly the grid g.

Equations

• c.Matches g = (c.grid? = some g)

@[simp]

theorem Minimalist.Theta.Color.matches_free {L : Type u_1} {g h : List PolarizedRole} : (free g).Matches h ↔ g = h

@[simp]

theorem Minimalist.Theta.Color.matches_lex {L : Type u_1} {α : L} {g h : List PolarizedRole} : (lex α g).Matches h ↔ g = h

@[simp]

theorem Minimalist.Theta.Color.not_matches_emptyTree {L : Type u_1} {g : List PolarizedRole} : ¬emptyTree.Matches g

inductive Minimalist.Theta.IsGen {L : Type u_1} (hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop) : List PolarizedRole → Color L → Color L → Prop

The generator shapes of the theta bud system, as a relation between the root grid and the two children's colors. The four cases are [ML25]'s complete-system generators:

• close: the external role discharges and the maximal projection is recolored arbitrarily;
• discharge: one internal role, next in the hierarchy, peels off to the sister while the residue propagates;
• adjunct: a non-theta position attaches without disturbing the color;
• move: a movement landing site, the empty-tree marker attached under a non-theta root.

• close {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} (g₀ : List PolarizedRole) (ρE : ArgumentStructure.ThetaRole) {a b : Color L} (ha : a.Matches [PolarizedRole.down ρE]) (hb : b.Matches [PolarizedRole.up ρE]) : IsGen hier g₀ a b
• discharge {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} (g : List ArgumentStructure.ThetaRole) (ρ : ArgumentStructure.ThetaRole) (hg : g ≠ []) (hchain : List.IsChain hier (g ++ [ρ]).tail) {a b : Color L} (ha : a.Matches [PolarizedRole.down ρ]) (hb : b.Matches (upGrid (g ++ [ρ]))) : IsGen hier (upGrid g) a b
• adjunct {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} (g₀ : List PolarizedRole) : IsGen hier g₀ (Color.free g₀) Color.nontheta
• move {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} (c' : Color L) (hc' : c' ≠ Color.emptyTree) : IsGen hier [] c' Color.emptyTree

def Minimalist.Theta.ThetaLocal {L : Type u_1} (hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop) (c a b : Color L) : Prop

The cherries of the theta bud system: a bare grid at the root over children forming a generator in either order, [ML25]'s compatibility relation for colored Merge.

Equations

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

@[reducible, inline]

abbrev Minimalist.Theta.system {L : Type u_1} (hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop) : Bud.System (Color L)

The complete theta bud system: the theta cherries, with the bare grids initial and the anchored grids and the empty-tree marker terminal.

Equations

• Minimalist.Theta.system hier = Bud.System.ofCherries (Minimalist.Theta.ThetaLocal hier) {c : Minimalist.Theta.Color L | ¬c.IsTerminal} {c : Minimalist.Theta.Color L | c.IsTerminal}

theorem Minimalist.Theta.IsGen.conservation {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {g₀ : List PolarizedRole} {a b : Color L} (h : IsGen hier g₀ a b) : (∃ (ρ : ArgumentStructure.ThetaRole) (g : List ArgumentStructure.ThetaRole), a.Matches [PolarizedRole.down ρ] ∧ b.Matches (upGrid g ++ [PolarizedRole.up ρ]) ∧ (g₀ = upGrid g ∨ g = [])) ∨ a = Color.free g₀ ∧ b = Color.nontheta ∨ g₀ = [] ∧ b = Color.emptyTree

The local conservation law: at every generator, either one child receives the last role of the other child's giver grid while the root keeps the residue, or the node is an adjunct attachment, or a movement landing under a non-theta root.

theorem Minimalist.Theta.IsGen.eq_nil_of_emptyTree {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {g₀ : List PolarizedRole} {a b : Color L} (h : IsGen hier g₀ a b) (he : a = Color.emptyTree ∨ b = Color.emptyTree) : g₀ = []

theorem Minimalist.Theta.ThetaLocal.eq_nontheta {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {c a b : Color L} (h : ThetaLocal hier c a b) (he : a = Color.emptyTree ∨ b = Color.emptyTree) : c = Color.nontheta

Movement lands only in non-theta positions: a generator with an empty-tree child has the non-theta root. The External/Internal Merge dichotomy of theta theory, at generator level.

def Minimalist.Theta.combSpine {L : Type u_1} (g : List ArgumentStructure.ThetaRole) : List ArgumentStructure.ThetaRole → Bud.Tree (Color L)

The spine of a bare theta comb: the residue grid grows by one role per node on the path to the head leaf, which carries the complete grid.

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Theta.combSpine g [] = Bud.Tree.leaf (Minimalist.Theta.Color.free (Minimalist.Theta.upGrid g))

def Minimalist.Theta.comb {L : Type u_1} (g₀ : List PolarizedRole) (ρE : ArgumentStructure.ThetaRole) (ρIs : List ArgumentStructure.ThetaRole) : Bud.Tree (Color L)

A bare theta comb ([ML25]'s bare-system generators): an external role, hierarchy-ordered internal roles, one receiver per node, the full giver grid at the head leaf, and an arbitrary root recoloring.

Equations

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

@[simp]

theorem Minimalist.Theta.out_combSpine {L : Type u_1} (g rest : List ArgumentStructure.ThetaRole) : (combSpine g rest).out = Color.free (upGrid g)

theorem Minimalist.Theta.combSpine_nodeLocal {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {g : List ArgumentStructure.ThetaRole} (hg : g ≠ []) {rest : List ArgumentStructure.ThetaRole} (hchain : List.IsChain hier (g ++ rest).tail) : Bud.Tree.NodeLocal (ThetaLocal hier) (combSpine g rest)

theorem Minimalist.Theta.comb_derivable {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} (g₀ : List PolarizedRole) (ρE : ArgumentStructure.ThetaRole) (ρIs : List ArgumentStructure.ThetaRole) (hchain : List.IsChain hier ρIs) : (system hier).Derives (Bud.Tree.leaf (Color.free g₀)) (comb g₀ ρE ρIs)

The bare theta combs are derivable in the complete system, provided the internal roles descend the hierarchy: the generator half of [ML25]'s reduction of the bare system to the complete one.

theorem Minimalist.Theta.combSpine_inputs {L : Type u_1} (g rest : List ArgumentStructure.ThetaRole) : (combSpine g rest).inputs = List.map (fun (ρ : ArgumentStructure.ThetaRole) => Color.free [PolarizedRole.down ρ]) rest ++ [Color.free (upGrid (g ++ rest))]

The inputs of a comb spine: one receiver per internal role, then the head carrying the accumulated grid.

theorem Minimalist.Theta.comb_inputs {L : Type u_1} (g₀ : List PolarizedRole) (ρE : ArgumentStructure.ThetaRole) (ρIs : List ArgumentStructure.ThetaRole) : (comb g₀ ρE ρIs).inputs = Color.free [PolarizedRole.down ρE] :: List.map (fun (ρ : ArgumentStructure.ThetaRole) => Color.free [PolarizedRole.down ρ]) ρIs ++ [Color.free (upGrid (ρE :: ρIs))]

The inputs of a comb: the external receiver, one receiver per internal role, and the head carrying the complete grid.

The theta criterion

def Minimalist.Theta.Color.receiver? {L : Type u_1} : Color L → Option ArgumentStructure.ThetaRole

The role a color receives, when it is a single receiver.

Equations

• c.receiver? = match c.grid? with | some [{ role := ρ, polarity := Minimalist.Theta.Polarity.receiver }] => some ρ | x => none

@[simp]

theorem Minimalist.Theta.Color.receiver?_free_down {L : Type u_1} (ρ : ArgumentStructure.ThetaRole) : (free [PolarizedRole.down ρ]).receiver? = some ρ

def Minimalist.Theta.SatisfiesCriterion {L : Type u_1} (x : Bud.Tree (Color L)) : Prop

The theta criterion on a colored operation. Some input, the head, carries an all-giver grid, every other input is a single receiver, and the received roles match the head's grid bijectively, as multisets.

Equations

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

theorem Minimalist.Theta.comb_satisfiesCriterion {L : Type u_1} (g₀ : List PolarizedRole) (ρE : ArgumentStructure.ThetaRole) (ρIs : List ArgumentStructure.ThetaRole) : SatisfiesCriterion (comb g₀ ρE ρIs)

The bare theta combs satisfy the theta criterion.

The sole-role invariant

def Minimalist.Theta.receiverCount (g : List PolarizedRole) : ℕ

The number of receiver occurrences in a grid.

Equations

• Minimalist.Theta.receiverCount g = List.countP (fun (p : Minimalist.Theta.PolarizedRole) => p.polarity == Minimalist.Theta.Polarity.receiver) g

@[simp]

theorem Minimalist.Theta.receiverCount_upGrid (g : List ArgumentStructure.ThetaRole) : receiverCount (upGrid g) = 0

@[simp]

theorem Minimalist.Theta.receiverCount_down_singleton (ρ : ArgumentStructure.ThetaRole) : receiverCount [PolarizedRole.down ρ] = 1

def Minimalist.Theta.Color.SoleReceiver {L : Type u_1} (c : Color L) : Prop

The color receives at most one role, its grid having at most one receiver occurrence.

Equations

• c.SoleReceiver = ∀ (g : List Minimalist.Theta.PolarizedRole), c.grid? = some g → Minimalist.Theta.receiverCount g ≤ 1

theorem Minimalist.Theta.Color.soleReceiver_of_receiverCount_le {L : Type u_1} {c : Color L} {g : List PolarizedRole} (hc : c.grid? = some g) (hg : receiverCount g ≤ 1) : c.SoleReceiver

theorem Minimalist.Theta.IsGen.soleReceiver {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {g₀ : List PolarizedRole} {a b : Color L} (h : IsGen hier g₀ a b) (hc : (Color.free g₀).SoleReceiver) (hb : b ≠ Color.emptyTree) : a.SoleReceiver ∧ b.SoleReceiver

A generator passes a sole receiver at its root down to its children, unless the second child is a movement landing site.

theorem Minimalist.Theta.ThetaLocal.soleReceiver {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {c a b : Color L} (h : ThetaLocal hier c a b) (hc : c.SoleReceiver) (ha : a ≠ Color.emptyTree) (hb : b ≠ Color.emptyTree) : a.SoleReceiver ∧ b.SoleReceiver

theorem Minimalist.Theta.out_ne_emptyTree {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {x : Bud.Tree (Color L)} (hx : Bud.Tree.NodeLocal (ThetaLocal hier) x) (hmove : Color.emptyTree ∉ x.inputs) : x.out ≠ Color.emptyTree

In a theta structure, only a leaf can carry the empty-tree marker.

theorem Minimalist.Theta.derives_soleReceiver {L : Type u_1} {hier : ArgumentStructure.ThetaRole → ArgumentStructure.ThetaRole → Prop} {c : Color L} {x : Bud.Tree (Color L)} (h : (system hier).Derives (Bud.Tree.leaf c) x) (hroot : c.SoleReceiver) (hmove : Color.emptyTree ∉ x.inputs) (d : Color L) : d ∈ x.inputs → d.SoleReceiver

The sole-role invariant: in a movement-free derivable structure whose root color receives at most one role, every argument position receives at most one role. Adding a dual-receiver generator, as se-marked parasitic assignment does, is the only way to violate it.