Person Feature Geometry @cite{preminger-2014}

@cite{bejar-rezac-2009} @cite{pancheva-zubizarreta-2018}

@cite{preminger-2014} decomposes phi-features into a hierarchical geometry where person sub-features are organized in a containment hierarchy:

[φ] → [PERSON] → [participant] → [author]
[φ] → [NUMBER] → [plural]

This decomposition drives relativized probing: a probe seeking [participant] skips DPs that lack it (3rd person), targeting only 1st/2nd person DPs. A separate probe seeking [plural] skips DPs that lack it (singulars), targeting only plurals.

The two-probe system derives the omnivorous agreement hierarchy in Kaqchikel Agent Focus:

[+participant] (π⁰) > [+plural] (#⁰) > default (3SG)

π⁰ outranks #⁰ because person probing takes priority over number probing. If π⁰ succeeds, its target determines the marker; if it fails, #⁰ provides the result; if both fail, the default surfaces.

Extended Geometry: [±proximate]

@cite{pancheva-zubizarreta-2018} extend the hierarchy with a [±proximate] feature for the Person Case Constraint:

[+author] ⊂ [+participant] ⊂ [+proximate]

1P and 2P are inherently [+proximate]. 3P arguments are [-proximate] by default but can be contextually marked [+proximate] (when co-occurring with another 3P). The [±proximate] distinction also captures the 3P proximate/obviative split in direct/inverse alignment systems (@cite{pancheva-zubizarreta-2018}, §2.1 (11)).

Relationship to Core PersonFeatures

DecomposedPerson extends Core.Person.Features (the framework-neutral [±participant, ±author] decomposition) with the Minimalism-specific [±proximate] feature. The two-feature core is shared across all theoretical frameworks; [±proximate] is specific to @cite{pancheva-zubizarreta-2018}'s P-Constraint.

Person Type

decomposePerson takes Core.Prominence.PersonLevel (.first | .second |.third) — the canonical person type shared across the library — rather than a raw Nat. This eliminates meaningless person values and grounds the decomposition in the same type used by DifferentialIndexing, Prominence.PersonLevel.isSAP, etc.

structure Minimalism.DecomposedPersonextends Core.Person.Features : Type

Person features decomposed according to @cite{preminger-2014}'s geometry, extended with [±proximate] from @cite{pancheva-zubizarreta-2018}.

Extends Core.Person.Features (the framework-neutral [±participant, ±author] core) with the Minimalism-specific [±proximate] feature:

• [proximate] marks potential point-of-view centers. 1P/2P are inherently [+proximate]; 3P can be contextually [+proximate].
• [participant] distinguishes 1st/2nd from 3rd person.
• [author] distinguishes 1st from 2nd person.

The geometry imposes a containment hierarchy: [+author] → [+participant] → [+proximate]

Note: The paper treats these as privative features: 3rd person simply LACKS [participant], rather than bearing [−participant]. We encode this as Bool for computational convenience; the well-formedness constraint wellFormed ensures the privative entailments are maintained.

• hasParticipant : Bool
• hasAuthor : Bool
• hasProximate : Bool

  Bears [proximate]? SAPs inherently; 3P contextually.

instance Minimalism.instDecidableEqDecomposedPerson : DecidableEq DecomposedPerson

Equations

• Minimalism.instDecidableEqDecomposedPerson = Minimalism.instDecidableEqDecomposedPerson.decEq

def Minimalism.instDecidableEqDecomposedPerson.decEq (x✝ x✝¹ : DecomposedPerson) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalism.instBEqDecomposedPerson.beq : DecomposedPerson → DecomposedPerson → Bool

Equations

• Minimalism.instBEqDecomposedPerson.beq { toFeatures := a, hasProximate := a_1 } { toFeatures := b, hasProximate := b_1 } = (a == b && a_1 == b_1)
• Minimalism.instBEqDecomposedPerson.beq x✝¹ x✝ = false

instance Minimalism.instBEqDecomposedPerson : BEq DecomposedPerson

Equations

• Minimalism.instBEqDecomposedPerson = { beq := Minimalism.instBEqDecomposedPerson.beq }

def Minimalism.instReprDecomposedPerson.repr : DecomposedPerson → Nat → Std.Format

Equations

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

instance Minimalism.instReprDecomposedPerson : Repr DecomposedPerson

Equations

• Minimalism.instReprDecomposedPerson = { reprPrec := Minimalism.instReprDecomposedPerson.repr }

def Minimalism.DecomposedPerson.wellFormed (dp : DecomposedPerson) : Bool

Geometry well-formedness: [author] → [participant] → [proximate]. Each feature entails the next in the containment hierarchy.

Equations

• dp.wellFormed = ((!dp.hasAuthor || dp.hasParticipant) && (!dp.hasParticipant || dp.hasProximate))

def Minimalism.decomposePerson : Core.Prominence.PersonLevel → DecomposedPerson

Decompose a person value into sub-features.

• 1st person: [+proximate, +participant, +author]
• 2nd person: [+proximate, +participant, −author]
• 3rd person: [−proximate, −participant, −author]

3rd person is [-proximate] by default; contextual [+proximate] marking is handled by the P-Constraint evaluation.

Equations

• Minimalism.decomposePerson Core.Prominence.PersonLevel.first = { hasParticipant := true, hasAuthor := true, hasProximate := true }
• Minimalism.decomposePerson Core.Prominence.PersonLevel.second = { hasParticipant := true, hasAuthor := false, hasProximate := true }
• Minimalism.decomposePerson Core.Prominence.PersonLevel.third = { hasParticipant := false, hasAuthor := false, hasProximate := false }

inductive Minimalism.ProbeTarget : Type

What a phi-probe seeks.

In the AF construction, two probes operate:

• π⁰ seeks [participant]: targets 1st/2nd person DPs
• #⁰ seeks [plural]: targets plural DPs

π⁰ structurally outranks #⁰ (person probing > number probing).

• participant : ProbeTarget

  π⁰: person probe, seeks [participant].

• plural : ProbeTarget

  #⁰: number probe, seeks [plural].

instance Minimalism.instDecidableEqProbeTarget : DecidableEq ProbeTarget

Equations

• Minimalism.instDecidableEqProbeTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instBEqProbeTarget.beq : ProbeTarget → ProbeTarget → Bool

Equations

• Minimalism.instBEqProbeTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqProbeTarget : BEq ProbeTarget

Equations

• Minimalism.instBEqProbeTarget = { beq := Minimalism.instBEqProbeTarget.beq }

def Minimalism.instReprProbeTarget.repr : ProbeTarget → Nat → Std.Format

Equations

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

instance Minimalism.instReprProbeTarget : Repr ProbeTarget

Equations

• Minimalism.instReprProbeTarget = { reprPrec := Minimalism.instReprProbeTarget.repr }

def Minimalism.probeVisible (target : ProbeTarget) (person : Core.Prominence.PersonLevel) (isPlural : Bool) : Bool

Is a DP visible to this probe? Relativized probing: probes skip DPs that lack the feature they seek.

A DP with person value person and number isPlural is visible to the probe iff it bears the probe's target feature.

Equations

• Minimalism.probeVisible Minimalism.ProbeTarget.participant person isPlural = (Minimalism.decomposePerson person).hasParticipant
• Minimalism.probeVisible Minimalism.ProbeTarget.plural person isPlural = isPlural

def Minimalism.probeResolutionRank (person : Core.Prominence.PersonLevel) (isPlural : Bool) : Nat

Omnivorous probe resolution rank for a DP.

Determines which DP an omnivorous probe targets when multiple DPs are in its domain. Higher rank = more likely to be targeted.

• Rank 2: visible to π⁰ ([+participant]) — highest priority
• Rank 1: visible to #⁰ but not π⁰ ([+plural, −participant])
• Rank 0: invisible to both probes (3SG default)

This rank is derived from the probing mechanism, not stipulated: π⁰ outranks #⁰, and each probe targets any DP bearing the sought feature. The rank captures the combined effect.

Equations

• Minimalism.probeResolutionRank person isPlural = if (Minimalism.decomposePerson person).hasParticipant = true then 2 else if isPlural = true then 1 else 0

theorem Minimalism.first_person_decomposition : (decomposePerson Core.Prominence.PersonLevel.first).hasProximate = true ∧ (decomposePerson Core.Prominence.PersonLevel.first).hasParticipant = true ∧ (decomposePerson Core.Prominence.PersonLevel.first).hasAuthor = true

1st person is [+proximate, +participant, +author].

theorem Minimalism.second_person_decomposition : (decomposePerson Core.Prominence.PersonLevel.second).hasProximate = true ∧ (decomposePerson Core.Prominence.PersonLevel.second).hasParticipant = true ∧ (decomposePerson Core.Prominence.PersonLevel.second).hasAuthor = false

2nd person is [+proximate, +participant, −author].

theorem Minimalism.third_person_decomposition : (decomposePerson Core.Prominence.PersonLevel.third).hasProximate = false ∧ (decomposePerson Core.Prominence.PersonLevel.third).hasParticipant = false ∧ (decomposePerson Core.Prominence.PersonLevel.third).hasAuthor = false

3rd person is [−proximate, −participant, −author].

theorem Minimalism.all_decompositions_wellFormed (p : Core.Prominence.PersonLevel) : (decomposePerson p).wellFormed = true

All person values yield well-formed decompositions.

theorem Minimalism.decomposePerson_toFeatures_eq (p : Core.Prominence.PersonLevel) : (decomposePerson p).toFeatures = p.toFeatures

decomposePerson is consistent with the framework-neutral PersonLevel.toFeatures: the [±participant, ±author] core of the Minimalist decomposition agrees with Core Person.Features.

theorem Minimalism.first_visible_to_pi : probeVisible ProbeTarget.participant Core.Prominence.PersonLevel.first false = true

1st person is visible to the person probe (π⁰).

theorem Minimalism.third_invisible_to_pi : probeVisible ProbeTarget.participant Core.Prominence.PersonLevel.third false = false

3rd person is invisible to the person probe.

theorem Minimalism.third_plural_visible_to_hash : probeVisible ProbeTarget.plural Core.Prominence.PersonLevel.third true = true

3rd plural is visible to the number probe (#⁰).

theorem Minimalism.third_sg_invisible_to_both : probeVisible ProbeTarget.participant Core.Prominence.PersonLevel.third false = false ∧ probeVisible ProbeTarget.plural Core.Prominence.PersonLevel.third false = false

3rd singular is invisible to both probes.

theorem Minimalism.participant_rank : probeResolutionRank Core.Prominence.PersonLevel.first false = 2 ∧ probeResolutionRank Core.Prominence.PersonLevel.second false = 2 ∧ probeResolutionRank Core.Prominence.PersonLevel.first true = 2 ∧ probeResolutionRank Core.Prominence.PersonLevel.second true = 2

1st/2nd person get rank 2 (visible to π⁰).

theorem Minimalism.plural_rank : probeResolutionRank Core.Prominence.PersonLevel.third true = 1

3rd plural gets rank 1 (visible to #⁰ only).

theorem Minimalism.default_rank : probeResolutionRank Core.Prominence.PersonLevel.third false = 0

3rd singular gets rank 0 (invisible to both probes = default).

theorem Minimalism.rank_hierarchy : probeResolutionRank Core.Prominence.PersonLevel.first false > probeResolutionRank Core.Prominence.PersonLevel.third true ∧ probeResolutionRank Core.Prominence.PersonLevel.third true > probeResolutionRank Core.Prominence.PersonLevel.third false

Rank is monotone in the probe hierarchy: any DP visible to π⁰ (rank 2) outranks any DP visible only to #⁰ (rank 1), which outranks any DP invisible to both (rank 0).