Containment Feature Pairs

A pair of bivalent features whose inner member entails the outer ([+inner] → [+outer]): the two-feature dependency skeleton of the feature-geometric tradition ([HR02]), stated over bivalent values with the dependency carried as a cooccurrence filter — what [AH08] call a "filter system … designating some semantically possible [combinations] as geometrically illicit" (their Structure theme).

The pattern recurs across φ-feature domains:

• Person: [±author] (inner) ⊂ [±participant] (outer)
• Number: [±atomic] (inner) ⊂ [±minimal] (outer)
• Gender: [±neuter] (inner) ⊂ [±feminine] (outer)

with honorific-level and animacy instances joining the same skeleton. The filter cuts the four bivalent cells to three, linearly ordered by specification (the "size of structure" markedness metric of [AH08]):

outer	inner	Status	Person	Number
+	+	most specified	1st person	singular
+	−	intermediate	2nd person	dual
−	−	least specified	3rd person	plural
−	+	filtered	—	—

Main declarations

• ContainmentPair — the bivalent pair carrier (all four cells)
• ContainmentPair.WellFormed — the containment filter, as the Bool order fact inner ≤ outer; the well-formed cells carry a LinearOrder (specification chain) and have Fintype.card three
• ContainmentPairLike — injective presentation of a carrier type as containment pairs (the SetLike pattern); no_four_way, specLevel, and WellFormed are inherited through it
• ContainmentPairLike.ofEquiv — instance constructor for carriers that are outright equivalent to the pair (person, number, gender features)

Implementation notes

Well-formedness is order theory, not stipulation: writing the valuation as a map from the two-element dependency chain {outer < inner} to Bool, WellFormed says the valuation is antitone in dependency — equivalently, the positively-valued features form a lower set of the chain. Lower sets of an n-chain form an (n+1)-chain, whence three cells from two features, the LinearOrder, and the impossibility of a fourth cell; longer dependency chains (e.g. [±proximate] above person, Phi/Geometry.lean) yield n+1 cells the same way.

This skeleton is not [Har16a]'s system (which this file's docstring previously claimed). Impossible Persons argues against both ingredients: against cooccurrence filters (ch. 9.4 — "missing feature combinations are not to be reified as universal principles"; feature cooccurrence is free, constrained only by the logic of the semantics) and for semantically active bivalence with order-of-composition effects (ch. 9.2, 9.5). In Harbour's calculus the filtered cell is used: +author(−participant(π)) is the exclusive in the quadripartition and an available representation of Germanic third person in the tripartition (ch. 8.3.1, 9.2). The Harbour calculus proper lives at Syntax/Minimalist/Phi/ (lattice operations ⊕/⊖) and Studies/Harbour2016.lean (signOf); this file is the descriptive containment skeleton that calculus refines and in part rejects.

structure Features.ContainmentPair : Type

A pair of bivalent features with a containment (dependency) relation: bearing the inner feature entails bearing the outer one. The carrier holds all four bivalent cells; the filter is WellFormed.

Instances present their carriers via ContainmentPairLike: person (outer = participant, inner = author), number (outer = minimal, inner = atomic), gender, animacy, honorific level.

• outer : Bool

  The entailed (outer, dominating) feature.

• inner : Bool

  The entailing (inner, dependent) feature — implies outer.

def Features.instDecidableEqContainmentPair.decEq (x✝ x✝¹ : ContainmentPair) : Decidable (x✝ = x✝¹)

Equations

• Features.instDecidableEqContainmentPair.decEq { outer := a, inner := a_1 } { outer := b, inner := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instDecidableEqContainmentPair : DecidableEq ContainmentPair

Equations

• Features.instDecidableEqContainmentPair = Features.instDecidableEqContainmentPair.decEq

def Features.instReprContainmentPair.repr : ContainmentPair → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprContainmentPair : Repr ContainmentPair

Equations

• Features.instReprContainmentPair = { reprPrec := Features.instReprContainmentPair.repr }

@[implicit_reducible]

instance Features.instInhabitedContainmentPair : Inhabited ContainmentPair

Equations

• Features.instInhabitedContainmentPair = { default := Features.instInhabitedContainmentPair.default }

def Features.instBEqContainmentPair.beq : ContainmentPair → ContainmentPair → Bool

Equations

• Features.instBEqContainmentPair.beq { outer := a, inner := a_1 } { outer := b, inner := b_1 } = (a == b && a_1 == b_1)
• Features.instBEqContainmentPair.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Features.instBEqContainmentPair : BEq ContainmentPair

Equations

• Features.instBEqContainmentPair = { beq := Features.instBEqContainmentPair.beq }

@[implicit_reducible]

instance Features.instFintypeContainmentPair : Fintype ContainmentPair

Equations

• Features.instFintypeContainmentPair = Fintype.ofEquiv ((_ : Bool) × Bool) Features.ContainmentPair.proxyTypeEquiv

The containment filter

def Features.ContainmentPair.WellFormed (p : ContainmentPair) : Prop

Containment: the inner feature entails the outer — equivalently inner ≤ outer in Bool's order, so the valuation is antitone in dependency and the positive features form a lower set of the dependency chain.

Equations

• p.WellFormed = (p.inner = true → p.outer = true)

@[implicit_reducible]

instance Features.ContainmentPair.instDecidablePredWellFormed : DecidablePred WellFormed

Equations

• p.instDecidablePredWellFormed = Features.ContainmentPair.instDecidablePredWellFormed._aux_1 p

Canonical cells

def Features.ContainmentPair.maximal : ContainmentPair

Most specified cell: [+outer, +inner]. Person: 1st (speaker). Number: singular (atom).

Equations

• Features.ContainmentPair.maximal = { outer := true, inner := true }

def Features.ContainmentPair.intermediate : ContainmentPair

Intermediate cell: [+outer, −inner]. Person: 2nd (non-speaker participant). Number: dual (minimal non-atom).

Equations

• Features.ContainmentPair.intermediate = { outer := true, inner := false }

def Features.ContainmentPair.minimal : ContainmentPair

Least specified cell: [−outer, −inner]. Person: 3rd (non-participant). Number: plural (non-minimal non-atom).

Equations

• Features.ContainmentPair.minimal = { outer := false, inner := false }

@[simp]

theorem Features.ContainmentPair.maximal_wellFormed : maximal.WellFormed

@[simp]

theorem Features.ContainmentPair.intermediate_wellFormed : intermediate.WellFormed

@[simp]

theorem Features.ContainmentPair.minimal_wellFormed : minimal.WellFormed

theorem Features.ContainmentPair.illFormed_only : ¬{ outer := false, inner := true }.WellFormed

The unique filtered combination: [−outer, +inner].

theorem Features.ContainmentPair.classification (p : ContainmentPair) : p.WellFormed → p = maximal ∨ p = intermediate ∨ p = minimal

Every well-formed pair is one of the three canonical cells.

theorem Features.ContainmentPair.inner_implies_outer (p : ContainmentPair) : p.WellFormed → p.inner = true → p.outer = true

Inner entails outer on well-formed pairs.

The specification chain

The well-formed cells form a three-element linear order — the "size of structure" markedness chain ([AH08]): minimal < intermediate < maximal.

def Features.ContainmentPair.specLevel (p : ContainmentPair) : ℕ

Specification level: the number of positive features. maximal ↦ 2, intermediate ↦ 1, minimal ↦ 0. On well-formed pairs this is injective and realizes the markedness chain.

Equations

• p.specLevel = p.outer.toNat + p.inner.toNat

@[simp]

theorem Features.ContainmentPair.spec_maximal : maximal.specLevel = 2

@[simp]

theorem Features.ContainmentPair.spec_intermediate : intermediate.specLevel = 1

@[simp]

theorem Features.ContainmentPair.spec_minimal : minimal.specLevel = 0

theorem Features.ContainmentPair.spec_strict_order : maximal.specLevel > intermediate.specLevel ∧ intermediate.specLevel > minimal.specLevel

The chain in concrete form: specification strictly descends maximal > intermediate > minimal.

theorem Features.ContainmentPair.specLevel_injOn_wellFormed (p q : ContainmentPair) : p.WellFormed → q.WellFormed → p.specLevel = q.specLevel → p = q

specLevel separates well-formed pairs.

@[implicit_reducible]

instance Features.ContainmentPair.instLinearOrderSubtypeWellFormed : LinearOrder { p : ContainmentPair // p.WellFormed }

The markedness chain: well-formed pairs are linearly ordered by specification level.

Equations

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

theorem Features.ContainmentPair.card_wellFormed : Fintype.card { p : ContainmentPair // p.WellFormed } = 3

Two dependent bivalent features yield exactly three cells — lower sets of a 2-chain form a 3-chain.

theorem Features.ContainmentPair.no_four_way (a b c d : ContainmentPair) : a.WellFormed → b.WellFormed → c.WellFormed → d.WellFormed → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

No four-way distinction. Four distinct well-formed pairs are impossible — a corollary of card_wellFormed, checked directly.

For person: no language draws a 4-way distinction from one containment pair; for number: likewise for base number. (The filter, not the arithmetic, is the theoretical commitment — [Har16a] ch. 9.4 rejects it and generates a 4th person as the quadripartition exclusive; see the module docstring.)

Carrier presentation

class Features.ContainmentPairLike (α : Type u_1) : Type u_1

An injective presentation of α as containment pairs (the SetLike pattern: a coercion-like map plus injectivity, not a bijection — a three-valued carrier such as an honorific scale embeds onto the well-formed cells only). WellFormed, specLevel, and no_four_way are inherited through the embedding.

• toPair : α → ContainmentPair

  Present an element as a containment pair.

• toPair_injective : Function.Injective toPair

  The presentation is faithful.

@[reducible]

def Features.ContainmentPairLike.ofEquiv {β : Type u_2} (e : β ≃ ContainmentPair) : ContainmentPairLike β

Build an instance from an outright equivalence (person, number, and gender features are bivalent pair records, hence equivalent carriers).

Equations

• Features.ContainmentPairLike.ofEquiv e = { toPair := ⇑e, toPair_injective := ⋯ }

theorem Features.ContainmentPairLike.injective {α : Type u_1} [ContainmentPairLike α] : Function.Injective toPair

def Features.ContainmentPairLike.WellFormed {α : Type u_1} [ContainmentPairLike α] (a : α) : Prop

Well-formedness through the presentation.

Equations

• Features.ContainmentPairLike.WellFormed a = (Features.ContainmentPairLike.toPair a).WellFormed

@[implicit_reducible]

instance Features.ContainmentPairLike.instDecidablePredWellFormed {α : Type u_1} [ContainmentPairLike α] : DecidablePred WellFormed

Equations

• Features.ContainmentPairLike.instDecidablePredWellFormed a = Features.ContainmentPairLike.instDecidablePredWellFormed._aux_1 a

def Features.ContainmentPairLike.specLevel {α : Type u_1} [ContainmentPairLike α] (a : α) : ℕ

Specification level through the presentation.

Equations

• Features.ContainmentPairLike.specLevel a = (Features.ContainmentPairLike.toPair a).specLevel

theorem Features.ContainmentPairLike.no_four_way {α : Type u_1} [ContainmentPairLike α] [DecidableEq α] (a b c d : α) (ha : WellFormed a) (hb : WellFormed b) (hc : WellFormed c) (hd : WellFormed d) (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) : False

No four-way distinction for any presented carrier.

theorem Features.ContainmentPairLike.specLevel_strict_order {α : Type u_1} [ContainmentPairLike α] {a b c : α} (ha : toPair a = ContainmentPair.maximal) (hb : toPair b = ContainmentPair.intermediate) (hc : toPair c = ContainmentPair.minimal) : specLevel a > specLevel b ∧ specLevel b > specLevel c

The specification ordering transports to any presented triple landing on the three cells. Person (1 > 2 > 3), number (sg > du > pl), and gender inherit their hierarchy from this single chain fact rather than re-checking it per domain.