Coordination resolution over a dual-feature system

This file defines resolution of gender features on a coordinate structure in a dual-feature system: a nominal's features are interpretable, sent to LF, or uninterpretable, sent to PF, and resolution is the composition of percolation, which collects one feature set from each conjunct at the coordination, with conversion, which intersects the interpretable sets so that the group bears exactly the features every member has. Uninterpretable sets are not intersected; they are realized set by set, and realization converges only when every set receives the same exponent. A feature geometry records, for each node, the nodes it entails, and a geometry satisfies mismatch resolution when every pair of its nodes resolves to something without default insertion.

Main definitions

• Minimalist.Coordination.Annotated, Minimalist.Coordination.Bundle: features annotated for interpretability and the feature sets of a nominal.
• Minimalist.Coordination.percolate, Minimalist.Coordination.percolateU: the interpretable and uninterpretable sets a conjunct contributes.
• Minimalist.Coordination.conversion, Minimalist.Coordination.resolve, Minimalist.Coordination.resolveN: intersection of percolated interpretable sets.
• Minimalist.Coordination.redundancy: the copying of interpretable values into empty uninterpretable slots at Transfer.
• Minimalist.Coordination.realizeAll: realization of a family of feature sets, converging only on a single exponent.
• Minimalist.Coordination.MismatchResolutionOn, Minimalist.Coordination.Geometry, Geometry.Entails, Geometry.MismatchResolution.

Main statements

• Minimalist.Coordination.resolveN_binary: n-ary resolution restricts to binary resolution.
• Minimalist.Coordination.resolve_self: uniform conjuncts resolve to their shared features.

References

• [adamson-anagnostopoulou-2025]
• [Smi15]

structure Minimalist.Coordination.Annotated (F : Type u_3) : Type u_3

A feature value annotated for interpretability.

• value : F
• interp : Interpretability

def Minimalist.Coordination.instDecidableEqAnnotated.decEq {F✝ : Type u_3} [DecidableEq F✝] (x✝ x✝¹ : Annotated F✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Minimalist.Coordination.instDecidableEqAnnotated {F✝ : Type u_3} [DecidableEq F✝] : DecidableEq (Annotated F✝)

Equations

• Minimalist.Coordination.instDecidableEqAnnotated = Minimalist.Coordination.instDecidableEqAnnotated.decEq

def Minimalist.Coordination.instReprAnnotated.repr {F✝ : Type u_3} [Repr F✝] : Annotated F✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Coordination.instReprAnnotated {F✝ : Type u_3} [Repr F✝] : Repr (Annotated F✝)

Equations

• Minimalist.Coordination.instReprAnnotated = { reprPrec := Minimalist.Coordination.instReprAnnotated.repr }

@[reducible, inline]

abbrev Minimalist.Coordination.Bundle (F : Type u_3) : Type u_3

The gender features of a nominal, interpretable and uninterpretable.

Equations

• Minimalist.Coordination.Bundle F = List (Minimalist.Coordination.Annotated F)

def Minimalist.Coordination.percolate {F : Type u_1} (fs : Bundle F) : List F

The interpretable values of a bundle: what percolates to LF-bound resolution.

Equations

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

def Minimalist.Coordination.percolateU {F : Type u_1} (fs : Bundle F) : List F

The uninterpretable values of a bundle.

Equations

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

def Minimalist.Coordination.interpretable {F : Type u_1} (vs : List F) : Bundle F

Interpretable annotation of every value in a list.

Equations

• Minimalist.Coordination.interpretable vs = List.map (fun (v : F) => { value := v, interp := Minimalist.Interpretability.interpretable }) vs

def Minimalist.Coordination.uninterpretable {F : Type u_1} (vs : List F) : Bundle F

Uninterpretable annotation of every value in a list.

Equations

• Minimalist.Coordination.uninterpretable vs = List.map (fun (v : F) => { value := v, interp := Minimalist.Interpretability.uninterpretable }) vs

@[simp]

theorem Minimalist.Coordination.percolate_interpretable {F : Type u_1} (vs : List F) : percolate (interpretable vs) = vs

@[simp]

theorem Minimalist.Coordination.percolateU_uninterpretable {F : Type u_1} (vs : List F) : percolateU (uninterpretable vs) = vs

@[simp]

theorem Minimalist.Coordination.percolate_append {F : Type u_1} (fs gs : Bundle F) : percolate (fs ++ gs) = percolate fs ++ percolate gs

@[simp]

theorem Minimalist.Coordination.percolateU_append {F : Type u_1} (fs gs : Bundle F) : percolateU (fs ++ gs) = percolateU fs ++ percolateU gs

@[simp]

theorem Minimalist.Coordination.percolate_uninterpretable {F : Type u_1} (vs : List F) : percolate (uninterpretable vs) = []

@[simp]

theorem Minimalist.Coordination.percolateU_interpretable {F : Type u_1} (vs : List F) : percolateU (interpretable vs) = []

def Minimalist.Coordination.redundancy {F : Type u_1} (iFs uFs : List F) : List F

The redundancy rule at Transfer: interpretable values fill an empty uninterpretable slot.

Equations

• Minimalist.Coordination.redundancy iFs uFs = if uFs.isEmpty = true then iFs else uFs

@[simp]

theorem Minimalist.Coordination.redundancy_nil {F : Type u_1} (iFs : List F) : redundancy iFs [] = iFs

theorem Minimalist.Coordination.redundancy_of_ne_nil {F : Type u_1} (iFs : List F) {uFs : List F} (h : uFs ≠ []) : redundancy iFs uFs = uFs

def Minimalist.Coordination.realizeAll {F : Type u_1} {E : Type u_2} [DecidableEq E] (realize : List F → Option E) : List (List F) → Option E

Realization of a family of feature sets: the exponent they all receive, if they agree.

Equations

• Minimalist.Coordination.realizeAll realize [] = none
• Minimalist.Coordination.realizeAll realize (s :: ss) = if ∀ t ∈ ss, realize t = realize s then realize s else none

@[simp]

theorem Minimalist.Coordination.realizeAll_singleton {F : Type u_1} {E : Type u_2} [DecidableEq E] (realize : List F → Option E) (s : List F) : realizeAll realize [s] = realize s

theorem Minimalist.Coordination.realizeAll_pair {F : Type u_1} {E : Type u_2} [DecidableEq E] (realize : List F → Option E) (s t : List F) : realizeAll realize [s, t] = if realize t = realize s then realize s else none

def Minimalist.Coordination.conversion {F : Type u_1} [DecidableEq F] (xs ys : List F) : List F

Conversion: the values shared by two percolated sets, in the order of the first.

Equations

• Minimalist.Coordination.conversion xs ys = List.filter (fun (x : F) => decide (x ∈ ys)) xs

theorem Minimalist.Coordination.mem_conversion {F : Type u_1} [DecidableEq F] {xs ys : List F} {v : F} : v ∈ conversion xs ys ↔ v ∈ xs ∧ v ∈ ys

@[simp]

theorem Minimalist.Coordination.conversion_self {F : Type u_1} [DecidableEq F] (xs : List F) : conversion xs xs = xs

def Minimalist.Coordination.resolve {F : Type u_1} [DecidableEq F] (fs gs : Bundle F) : Option (List F)

Resolution of two conjuncts: the shared interpretable values, none if there are none.

Equations

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

def Minimalist.Coordination.resolveN {F : Type u_1} [DecidableEq F] (bundles : List (Bundle F)) : Option (List F)

Resolution of a family of conjuncts by iterated conversion.

Equations

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

theorem Minimalist.Coordination.resolveN_binary {F : Type u_1} [DecidableEq F] (fs gs : Bundle F) : resolveN [fs, gs] = resolve fs gs

theorem Minimalist.Coordination.resolve_self {F : Type u_1} [DecidableEq F] (fs : Bundle F) (h : percolate fs ≠ []) : resolve fs fs = some (percolate fs)

Uniform conjuncts resolve to their shared features.

theorem Minimalist.Coordination.resolve_singleton {F : Type u_1} [DecidableEq F] (x y : F) (i j : Interpretability) : resolve [{ value := x, interp := i }] [{ value := y, interp := j }] = if i = Interpretability.interpretable ∧ j = Interpretability.interpretable ∧ x = y then some [x] else none

Single-feature conjuncts resolve to their feature exactly when both are interpretable and match.

def Minimalist.Coordination.MismatchResolutionOn {F : Type u_1} [DecidableEq F] (bundles : List (Bundle F)) : Prop

Every pair of bundles resolves without default insertion.

Equations

• Minimalist.Coordination.MismatchResolutionOn bundles = ∀ a ∈ bundles, ∀ b ∈ bundles, (Minimalist.Coordination.resolve a b).isSome = true

@[instance_reducible]

instance Minimalist.Coordination.instDecidableMismatchResolutionOn {F : Type u_1} [DecidableEq F] (bundles : List (Bundle F)) : Decidable (MismatchResolutionOn bundles)

Equations

• Minimalist.Coordination.instDecidableMismatchResolutionOn bundles = Minimalist.Coordination.instDecidableMismatchResolutionOn._aux_1 bundles

structure Minimalist.Coordination.Geometry (F : Type u_3) : Type u_3

A feature geometry: for each node, the nodes it entails, itself included.

• nodes : List F

  The nodes.

• above : F → List F

  The closure of a node under entailment.

def Minimalist.Coordination.Geometry.Entails {F : Type u_1} (G : Geometry F) (a b : F) : Prop

a entails b when b's closure lies within a's.

Equations

• G.Entails a b = (G.above b).Subset (G.above a)

@[instance_reducible]

instance Minimalist.Coordination.Geometry.instDecidableEntails {F : Type u_1} [DecidableEq F] (G : Geometry F) (a b : F) : Decidable (G.Entails a b)

Equations

• G.instDecidableEntails a b = Minimalist.Coordination.Geometry.instDecidableEntails._aux_1 G a b

def Minimalist.Coordination.Geometry.MismatchResolution {F : Type u_1} [DecidableEq F] (G : Geometry F) : Prop

Every pair of nodes resolves without default insertion.

Equations

• G.MismatchResolution = Minimalist.Coordination.MismatchResolutionOn (List.map (fun (a : F) => Minimalist.Coordination.interpretable (G.above a)) G.nodes)

@[instance_reducible]

instance Minimalist.Coordination.Geometry.instDecidableMismatchResolution {F : Type u_1} [DecidableEq F] (G : Geometry F) : Decidable G.MismatchResolution

Equations

• G.instDecidableMismatchResolution = Minimalist.Coordination.Geometry.instDecidableMismatchResolution._aux_1 G