Docs / Phonology / FeatureGeometry

Feature geometry

import Linglib.Phonology.FeatureGeometry · namespace Phonology.FeatureGeometry

A feature geometry over a feature type F places each feature below at most one node of a rooted tree of class nodes, a map node : F → Option N, and the feature class of a node is the set of features placed at or below it. The tree is mathlib's, a partial order with a bottom, a predecessor and archimedean descent, so feature classes are the preimages of principal upper sets: they shrink along dominance and are disjoint across incomparable nodes. Spreading a class from one segment onto another is Finset.piecewise on it, and agreement on a class is Set.EqOn. The trees of Clements, Sagey and Halle, Vaux and Wolfe are built in their studies.

Main definitions

FeatureGeometry.featureClass — the features a placement puts at or below a node.

Main results

antitone_featureClass, disjoint_featureClass — feature classes shrink along dominance and are disjoint across incomparable nodes.
eqOn_piecewise_of_le, eqOn_piecewise_of_incompRel — spreading a node carries every class it dominates and leaves every incomparable class untouched.

Implementation notes

The placement is Option-valued so that a geometry may leave features of the inventory unplaced. A study orders its tree by the parent map, a ≤ b when a lies on the walk from b up to the root, the root as ⊥ and the parent as Order.pred, every axiom decided. Spreading any set of terminals, Halle, Vaux and Wolfe's partial spreading, is Finset.piecewise on that set, and single-feature spreading is Function.update.

References

Feature classes

The feature class of a node is the set of features placed at or below it.

def featureClass L57–59

{F : Type u_1} {N : Type u_2} [Fintype F] [Preorder N] [DecidableLE N] (node : F → Option N) (a : N) :

Finset F

featureClass node a = {f : F | ∃ m ∈ node f, a ≤ m}

Used by mem_featureClass, le_of_mem_featureClass, mem_featureClass_bot, antitone_featureClass, disjoint_featureClass, eqOn_piecewise_of_le, eqOn_piecewise_of_incompRel

Used in Clements1985, HalleVauxWolfe2000, Jacobs2026, Padgett2002, Sagey1986

L63–64

L66–68

L70–71

Feature classes shrink along dominance.

theorem antitone_featureClass L73–77

{F : Type u_1} {N : Type u_2} [Fintype F] [Preorder N] [DecidableLE N] {node : F → Option N} :

Antitone (featureClass node)

Built from

Incomparable nodes have disjoint feature classes, since their subtrees are disjoint.

theorem disjoint_featureClass L79–90

{F : Type u_1} {N : Type u_2} [Fintype F] [Preorder N] [DecidableLE N] {node : F → Option N} {a b : N} [PredOrder N] [IsPredArchimedean N] (h : IncompRel (fun (x1 x2 : N) => x1 ≤ x2) a b) :

Disjoint (featureClass node a) (featureClass node b)

Built from

Spreading

Spreading node a from src onto tgt carries every class a dominates.

theorem eqOn_piecewise_of_le L96–99

{F : Type u_1} {N : Type u_2} [Fintype F] [Preorder N] [DecidableLE N] {node : F → Option N} {a b : N} [DecidableEq F] {β : Type u_3} (src tgt : F → β) (h : a ≤ b) :

Set.EqOn ((featureClass node a).piecewise src tgt) src ↑(featureClass node b)

Built from

Spreading node a leaves every class incomparable with a untouched.

theorem eqOn_piecewise_of_incompRel L101–106

{F : Type u_1} {N : Type u_2} [Fintype F] [Preorder N] [DecidableLE N] {node : F → Option N} {a b : N} [DecidableEq F] {β : Type u_3} (src tgt : F → β) [PredOrder N] [IsPredArchimedean N] (h : IncompRel (fun (x1 x2 : N) => x1 ≤ x2) a b) :

Set.EqOn ((featureClass node a).piecewise src tgt) tgt ↑(featureClass node b)

Built from