Theta theory as a coloring algorithm

[ML25] implements theta theory in the mathematical model of Minimalism ([MCB25] §3.8) as a coloring algorithm: structures freely formed by Merge are filtered by membership in the language of a bud generating system ([Gir19], Core/Algebra/RootedTree/Bud.lean) 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 node one receiver peels off to the sister position, and the residue continues toward the maximal projection.

Main declarations

• PolarizedRole, Color — giver/receiver-marked roles, and the color set: bare grids (nonterminal; [] is the non-theta marker), lexically anchored grids (terminal), and the empty-tree marker.
• IsGen, rules, system — the generating set: external-role closure, hierarchy-ordered internal discharge, adjunct attachment, and movement landing ([ML25]'s complete theta bud system).
• IsGen.conservation — the local conservation law each generator satisfies; derives_thetaLocal — every vertex of every derivable structure is a generator instance, hence conserves theta roles.
• comb, comb_derivable — the bare theta combs (complete grids discharged one role per node) are derivable in the complete system: the generator half of [ML25]'s comparison of bare and complete systems.
• rules_emptyTree_out — a generator with an empty-tree input has a non-theta output: movement lands only in non-theta positions, the External/Internal Merge dichotomy at generator level.
• SatisfiesCriterion, comb_satisfiesCriterion — the theta criterion (a head grid matched bijectively by single receivers at the other positions) and its verification on the bare combs.
• derives_soleReceiver — the sole-role invariant: in a movement-free derivable structure with a sole-receiver root, every position receives at most one role.

inductive Minimalist.Theta.Polarity : Type

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

• 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 : 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 (ρ : ThetaRole) : PolarizedRole

The giver occurrence θ↑.

Equations

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

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

The receiver occurrence θ↓.

Equations

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

def Minimalist.Theta.upGrid (g : List 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 {ρ : ThetaRole} {g : List ThetaRole} : PolarizedRole.down ρ ∉ upGrid g

@[simp]

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

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

The color set: a bare grid (nonterminal; the empty grid is 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

Terminal colors: lexically anchored grids and the empty-tree marker.

Equations

• (Minimalist.Theta.Color.free a).IsTerminal = False
• (Minimalist.Theta.Color.lex a a_1).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 a).grid? = some a
• (Minimalist.Theta.Color.lex a a_1).grid? = some a_1
• 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 : ThetaRole → 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 (children unordered; the rule set closes under swapping). 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 attaches under a non-theta root.

• close {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} (g₀ : List PolarizedRole) (ρE : 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 : ThetaRole → ThetaRole → Prop} (g : List ThetaRole) (ρ : 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 : ThetaRole → ThetaRole → Prop} (g₀ : List PolarizedRole) : IsGen hier g₀ (Color.free g₀) Color.nontheta
• move {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} (c' : Color L) (hc' : c' ≠ Color.emptyTree) : IsGen hier [] c' Color.emptyTree

def Minimalist.Theta.gen {L : Type u_1} (c a b : Color L) : Bud.Tree (Color L)

A one-node colored operation.

Equations

• Minimalist.Theta.gen c a b = Bud.Tree.node c (Bud.Tree.leaf a) (Bud.Tree.leaf b)

def Minimalist.Theta.rules {L : Type u_1} (hier : ThetaRole → ThetaRole → Prop) : Set (Bud.Tree (Color L))

The rule set: the generator shapes in either orientation, rooted at a nonterminal color.

Equations

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

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

The complete theta bud system.

Equations

• Minimalist.Theta.system hier = { rules := Minimalist.Theta.rules hier, Terminal := {c : Minimalist.Theta.Color L | c.IsTerminal} }

theorem Minimalist.Theta.IsGen.conservation {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} {g₀ : List PolarizedRole} {a b : Color L} (h : IsGen hier g₀ a b) : (∃ (ρ : ThetaRole) (g : List 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.

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

The vertex-local law of the theta system: the vertex is a generator instance in some orientation.

Equations

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

theorem Minimalist.Theta.rules_nodeLocal {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} {r : Bud.Tree (Color L)} (hr : r ∈ rules hier) : Bud.Tree.NodeLocal (ThetaLocal hier) r

theorem Minimalist.Theta.derives_thetaLocal {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} {c : Color L} {x : Bud.Tree (Color L)} (h : (system hier).Derives c x) : Bud.Tree.NodeLocal (ThetaLocal hier) x

Every vertex of every derivable structure is a generator instance: filtering by the coloring rules is checkable vertex-locally, the engine of [ML25]'s recursive theta criterion.

theorem Minimalist.Theta.rules_emptyTree_out {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} {r : Bud.Tree (Color L)} (hr : r ∈ rules hier) (h : Color.emptyTree ∈ r.inputs) : r.out = Color.nontheta

Movement lands only in non-theta positions: a generator with an empty-tree input has the non-theta output. The External/Internal Merge dichotomy of theta theory, derived from the generator shapes.

def Minimalist.Theta.combSpine {L : Type u_1} (g : List ThetaRole) : List 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 : ThetaRole) (ρIs : List 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.

theorem Minimalist.Theta.combSpine_derivable {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} (g : List ThetaRole) (hg : g ≠ []) (rest : List ThetaRole) (hchain : List.IsChain hier (g ++ rest).tail) : (system hier).Derives (Color.free (upGrid g)) (combSpine g rest)

theorem Minimalist.Theta.comb_derivable {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} (g₀ : List PolarizedRole) (ρE : ThetaRole) (ρIs : List ThetaRole) (hchain : List.IsChain hier ρIs) : (system hier).Derives (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 ThetaRole) : (combSpine g rest).inputs = List.map (fun (ρ : 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 : ThetaRole) (ρIs : List ThetaRole) : (comb g₀ ρE ρIs).inputs = Color.free [PolarizedRole.down ρE] :: List.map (fun (ρ : 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 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} (ρ : 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, since the trees are nonplanar.

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 : ThetaRole) (ρIs : List ThetaRole) : SatisfiesCriterion (comb g₀ ρE ρIs)

The bare theta combs satisfy the theta criterion: the head's grid is matched exactly by the receivers at the other positions.

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 ThetaRole) : receiverCount (upGrid g) = 0

@[simp]

theorem Minimalist.Theta.receiverCount_down_singleton (ρ : 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, if any, has 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_emptyTree {L : Type u_1} : emptyTree.SoleReceiver

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.derives_soleReceiver {L : Type u_1} {hier : ThetaRole → ThetaRole → Prop} {c : Color L} {x : Bud.Tree (Color L)} (h : (system hier).Derives 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.