Phi lattices and their operations

[Har16a]

The person lattices of [Har16a] and the operations on them, factored out as reusable substrate. A phi lattice is a collection of feature denotations — each denotation a nonempty set of atoms (Finset (Finset α), the powerset of an atomic participant domain, p. 73: the author lattice ℒau, participant lattice ℒpt, and π lattice ℒπ). Features denote operations on these lattices, not predicates: ⊕ (oplus, disjoint addition) and ⊖ (ominus, joint subtraction), with Lexical Complementarity (lexComp) the elsewhere-style restriction that keeps sibling denotations disjoint (p. 80).

This is the shared origin substrate for [Har16a]'s person partition (Studies.Harbour2016, which builds the partition construction on top) and for [Too23]'s animacy account (Studies.Toosarvandani2023, which reuses oplus/nePowerset/lexComp for heterogeneous pluralities such as oplus SPEAKER ANIMATE). Generic over the atom type α. Sits beside Phi.Geometry (the person feature geometry) and Phi.Recursion (the number calculus).

Main declarations

• nePowerset — the nonempty powerset (a phi lattice generated from an atom set).
• oplus — disjoint addition (⊕): pointwise lattice join of two denotations ([Har16a] (17); = Finset.image₂ (· ∪ ·)).
• ominus — joint subtraction (⊖): strip a feature lattice's maximum from each element ([Har16a] (19)).
• lexComp — Lexical Complementarity: G \ F, restricting G away from a more specified sibling F ([Har16a] (31)).
• act — apply a signed feature (lattice F) to a collection G: +F is oplus, −F is ominus. The ± sign is genuine bivalent data ([Har16a]'s bivalence thesis).

The lattice constructor

def Minimalist.Phi.Lattice.nePowerset {α : Type u_1} [DecidableEq α] (atoms : Finset α) : Finset (Finset α)

Nonempty powerset: all nonempty subsets of atoms. The phi lattice generated from an atom set — every nonempty sum of atoms (ℒπ when atoms is the full participant domain). Mathlib has no such operation; this mirrors the definitional shape of Finset.ssubsets (= powerset.erase s, the proper subsets — removing the top), removing the bottom ∅ instead.

Equations

• Minimalist.Phi.Lattice.nePowerset atoms = atoms.powerset.erase ∅

theorem Minimalist.Phi.Lattice.nePowerset_mono {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) : nePowerset s ⊆ nePowerset t

Monotonicity of nePowerset.

theorem Minimalist.Phi.Lattice.nePowerset_union_mem {α : Type u_1} [DecidableEq α] {X s t : Finset α} (hs : s ∈ nePowerset X) (ht : t ∈ nePowerset X) : s ∪ t ∈ nePowerset X

nePowerset X is closed under nonempty union.

⊕ — disjoint addition ([Har16a] (17))

def Minimalist.Phi.Lattice.oplus {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : Finset (Finset α)

Disjoint addition ⊕ (oplus): the pointwise lattice join of two feature denotations ([Har16a] (17)) — the Linkian join operator [Lin83] (cf. [Chi98]'s sum). Generates heterogeneous pluralities: oplus SPEAKER ANIMATE includes {speaker, animal}. The body (F ×ˢ G).image (· ∪ ·) is mathlib's own unfolding of Finset.image₂ (· ∪ ·) (see oplus_eq_image₂), so the image₂_* lemmas transfer by rfl.

Equations

• Minimalist.Phi.Lattice.oplus F G = Finset.image (fun (yz : Finset α × Finset α) => yz.1 ∪ yz.2) (F ×ˢ G)

theorem Minimalist.Phi.Lattice.oplus_eq_image₂ {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : oplus F G = Finset.image₂ (fun (x1 x2 : Finset α) => x1 ∪ x2) F G

oplus agrees with Finset.image₂ (· ∪ ·) definitionally.

theorem Minimalist.Phi.Lattice.mem_oplus_iff {α : Type u_1} [DecidableEq α] {F G : Finset (Finset α)} {z : Finset α} : z ∈ oplus F G ↔ ∃ x ∈ F, ∃ y ∈ G, x ∪ y = z

Membership in oplus.

theorem Minimalist.Phi.Lattice.mem_oplus_of_mem {α : Type u_1} [DecidableEq α] {F G : Finset (Finset α)} {x y : Finset α} (hx : x ∈ F) (hy : y ∈ G) : x ∪ y ∈ oplus F G

Constructor form of oplus membership.

theorem Minimalist.Phi.Lattice.oplus_subset {α : Type u_1} [DecidableEq α] {F F' G G' : Finset (Finset α)} (hF : F ⊆ F') (hG : G ⊆ G') : oplus F G ⊆ oplus F' G'

Monotonicity of ⊕.

theorem Minimalist.Phi.Lattice.oplus_assoc {α : Type u_1} [DecidableEq α] (F G H : Finset (Finset α)) : oplus (oplus F G) H = oplus F (oplus G H)

Associativity of ⊕.

theorem Minimalist.Phi.Lattice.oplus_subset_nePowerset {α : Type u_1} [DecidableEq α] {X : Finset α} {F G : Finset (Finset α)} (hF : F ⊆ nePowerset X) (hG : G ⊆ nePowerset X) : oplus F G ⊆ nePowerset X

⊕ of two sub-lattices of nePowerset X lands back in nePowerset X.

theorem Minimalist.Phi.Lattice.oplus_nePowerset_self_subset {α : Type u_1} [DecidableEq α] (X : Finset α) : oplus (nePowerset X) (nePowerset X) ⊆ nePowerset X

nePowerset X is closed under self-⊕.

⊖ — joint subtraction ([Har16a] (19))

def Minimalist.Phi.Lattice.ominus {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : Finset (Finset α)

Joint subtraction ⊖ (ominus): strip the feature lattice F's maximum (F.sup id, its generating set) from every element of the collection G. Cumulative subtraction reduces to subtracting the maximum, since the feature lattices have a unique maximal element ([Har16a] (19)). The empty set may appear and is winnowed downstream by the variable head φ.

Equations

• Minimalist.Phi.Lattice.ominus F G = Finset.image (fun (x : Finset α) => x \ F.sup id) G

theorem Minimalist.Phi.Lattice.mem_ominus_iff {α : Type u_1} [DecidableEq α] {F G : Finset (Finset α)} {z : Finset α} : z ∈ ominus F G ↔ ∃ g ∈ G, g \ F.sup id = z

Membership in ominus.

theorem Minimalist.Phi.Lattice.ominus_subset {α : Type u_1} [DecidableEq α] {F G G' : Finset (Finset α)} (h : G ⊆ G') : ominus F G ⊆ ominus F G'

Monotonicity of ⊖ in the acted-on collection.

Lexical Complementarity ([Har16a] (31))

def Minimalist.Phi.Lattice.lexComp {α : Type u_1} [DecidableEq α] (G F : Finset (Finset α)) : Finset (Finset α)

Lexical Complementarity: when ⟦F⟧ ⊂ ⟦G⟧, use of G is restricted to ⟦G⟧ \ ⟦F⟧, forestalling a denotation from covering individuals a more featurally specified sibling already picks out ([Har16a] (31), p. 80).

Equations

• Minimalist.Phi.Lattice.lexComp G F = G \ F

theorem Minimalist.Phi.Lattice.lexComp_subset {α : Type u_1} [DecidableEq α] (G F : Finset (Finset α)) : lexComp G F ⊆ G

theorem Minimalist.Phi.Lattice.mem_lexComp_iff {α : Type u_1} [DecidableEq α] {G F : Finset (Finset α)} {z : Finset α} : z ∈ lexComp G F ↔ z ∈ G ∧ z ∉ F

Membership in lexComp.

theorem Minimalist.Phi.Lattice.lexComp_disjoint {α : Type u_1} [DecidableEq α] (G F : Finset (Finset α)) : Disjoint (lexComp G F) F

A lexComp result is disjoint from the more-specified sibling it excludes.

theorem Minimalist.Phi.Lattice.lexComp_subset_nePowerset {α : Type u_1} [DecidableEq α] {X : Finset α} {G F : Finset (Finset α)} (hG : G ⊆ nePowerset X) : lexComp G F ⊆ nePowerset X

lexComp stays within nePowerset X (it only removes elements).

Signed feature application

def Minimalist.Phi.Lattice.act {α : Type u_1} [DecidableEq α] (sign : Bool) (F G : Finset (Finset α)) : Finset (Finset α)

Apply a signed feature (lattice F) to a collection G: +F is oplus, −F is ominus. The sign : Bool is genuine bivalent feature polarity ([Har16a] treats ± as bivalent values), not predicate-shape data.

Equations

• Minimalist.Phi.Lattice.act sign F G = if sign = true then Minimalist.Phi.Lattice.oplus F G else Minimalist.Phi.Lattice.ominus F G

@[simp]

theorem Minimalist.Phi.Lattice.act_true {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : act true F G = oplus F G

@[simp]

theorem Minimalist.Phi.Lattice.act_false {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : act false F G = ominus F G