Aissen & Polian 2025: Possessor Extraction and Categorical Subject in Tseltalan

@cite{aissen-polian-2025}

Natural Language & Linguistic Theory 43:63--113.

Overview

Tseltalan languages (Tsotsil, Tseltal) have two possessor extraction strategies — pied-piping and stranding — whose availability depends on nominal size (= specificity) and intervention by A-positioned DPs.

The analysis rests on two independent mechanisms:

1. Selective opacity (@cite{keine-2019}): N⁰ is a horizon for wh-probes on C° — Ā-subextraction from within ANY nominal is impossible, regardless of size. This forces all possessor extraction to proceed via external possession.

2. D-layer shielding (Attract Closest): in specific DPs, D° is closer to T°'s [EPP:D] probe than the possessor inside Spec,PossP. Non-specific nominals (PossP/nP) lack a D layer, so T°'s probe reaches the possessor.

Together these derive:

• Stranding: possessor A-moves out of non-specific nominal (D-probe sees through nominal, no D-layer shields), then Ā-moves from external position
• Pied-piping: whole DP moves to Spec,CP (DP is visible to wh-probe as a unit; subextraction from within is blocked by selective opacity)
• Why extracted possessors are ALWAYS external (claim (3) on p. 65): follows from selective opacity — not stipulated

Stranding is further constrained by intervention: an A-positioned DP (agent or S_A) between the possessor and T°'s [EPP:D] probe blocks possessor raising via Attract Closest.

ψ-Subject Constructions

A&P identify a family of constructions in which a possessor is interpreted as ψ-subject (categorical-judgment subject in Spec,TP, @cite{kuroda-1972}). §5 focuses on three intransitive unaccusative cases: predicative possession (§5.2), experiential collocations (§5.3), and ordinary lexical unaccusatives (§5.4). §6.2 extends the analysis to configurations where the ψ-subject possessor originates inside a PP: path verbs (§6.2.1), locative existentials (§6.2.2), and two-argument experiential collocations (§6.2.3). §7.1 further notes that even Psr-A can serve as ψ-subject in broad-predicate expressions like x's fleas landed on me. The ψConstruction enumeration below covers the §5 intransitive subset; §6.2 / §7.1 cases are noted but not enumerated.

Predecessor Accounts and Comparative Engagement

A&P §4 contests @cite{little-2020a} / @cite{little-2020b}, the proximate Ch'ol analysis that derives possessor-extraction asymmetries from a Diesing-style specificity restriction combined with the Freezing Principle (Object Shift of specific objects → frozen for Ā-subextraction). A&P argue Little's account fails to extend to non-specific cases: Ā-subextraction is blocked from non-specifics as well, so a blanket nominal-opacity ban (selective opacity) is needed instead.

The escape-hatch view of @cite{gavruseva-2000} (Spec,DP as left-edge position parallel to Spec,CP) is the older predecessor view A&P reject: their analysis derives extraction without any DP-internal subextraction step. @cite{aissen-1996} is the earlier Tsotsil pied-piping analysis; @cite{aissen-1999a} establishes that Tseltalan A's extract freely (used in §6.2 to motivate why intervention is by A-position not Ā-extraction). @cite{coon-baier-levin-2021} on Mayan agent focus is contested in §6.1 (the file currently does not formalize this).

@cite{coon-henderson-2011} and @cite{aissen-1987} are the two competing analyses of the Tseltalan possessive applicative (control vs raising); A&P adopt the raising analysis, which the file's DProbeHead.appl slot implicitly assumes.

@cite{heycock-doron-2003} on Hebrew broad subjects is A&P's primary cross-linguistic typological precedent for ψ-subjects (cited p. 86 fn 22 alongside Tz'utujil, Chickasaw, Sinitic double-unaccusative).

Integration Points

• NominalPosition / PossessionType from NominalStructure.lean
• SpecificityCondition from Core/SpecificityCondition.lean
• JudgmentType from Core/Discourse/InformationStructure.lean
• GramFunction, absPosition from Fragments/Mayan/Tseltalan.lean
• ABSPosition from Fragments/Mayan/Params.lean
• ProbeProfile, closestGoalB, behindHorizonB, liftFM from Theories/Syntax/Minimalist/{Agree, Basic}.lean

inductive AissenPolian2025.NominalSize : Type

Nominal projections in Tseltalan, determining extractability. @cite{aissen-polian-2025} §3.2, (11)/(18): specific indefinites and definites project to DP; non-specific indefinites project only to nP (if non-possessive) or PossP (if possessive).

Derived from the nominal spine in NominalStructure.lean: √ROOT < n < (Poss) < D.

• dp : NominalSize
• possP : NominalSize
• nP : NominalSize

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqNominalSize : DecidableEq NominalSize

Equations

• AissenPolian2025.instDecidableEqNominalSize x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AissenPolian2025.instReprNominalSize.repr : NominalSize → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AissenPolian2025.instReprNominalSize : Repr NominalSize

Equations

• AissenPolian2025.instReprNominalSize = { reprPrec := AissenPolian2025.instReprNominalSize.repr }

def AissenPolian2025.NominalSize.highestProjection : NominalSize → Morphology.DM.NominalPosition

The highest position projected in the nominal spine. For DPs, the highest position is D (which shields the possessor from external D-probes). For non-specific nominals, the highest position IS the possessor's specifier position, making the possessor directly accessible.

Equations

• AissenPolian2025.NominalSize.dp.highestProjection = Morphology.DM.NominalPosition.d
• AissenPolian2025.NominalSize.possP.highestProjection = Morphology.DM.NominalPosition.specPoss
• AissenPolian2025.NominalSize.nP.highestProjection = Morphology.DM.NominalPosition.specN

def AissenPolian2025.NominalSize.IsSpecific : NominalSize → Prop

Specific nominals project to DP; non-specific nominals do not. @cite{aissen-polian-2025} §3.2.

Equations

• AissenPolian2025.NominalSize.dp.IsSpecific = True
• AissenPolian2025.NominalSize.possP.IsSpecific = False
• AissenPolian2025.NominalSize.nP.IsSpecific = False

@[implicit_reducible]

instance AissenPolian2025.instDecidablePredNominalSizeIsSpecific : DecidablePred NominalSize.IsSpecific

Equations

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

inductive AissenPolian2025.ArgumentStructureClass : Type

Clause types in Tseltalan, classified by whether the verb projects an external argument (vP layer). This is a theoretical classification from Minimalist syntax, used here to derive intervention effects.

@cite{aissen-polian-2025} (9):

• Unaccusative: no vP layer (sole argument is complement of V)
• Transitive: vP layer with agent in Spec,vP
• Unergative: vP layer with agentive S in Spec,vP

• unaccusative : ArgumentStructureClass
• transitive : ArgumentStructureClass
• unergative : ArgumentStructureClass

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqArgumentStructureClass : DecidableEq ArgumentStructureClass

Equations

• AissenPolian2025.instDecidableEqArgumentStructureClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AissenPolian2025.instReprArgumentStructureClass : Repr ArgumentStructureClass

Equations

• AissenPolian2025.instReprArgumentStructureClass = { reprPrec := AissenPolian2025.instReprArgumentStructureClass.repr }

def AissenPolian2025.instReprArgumentStructureClass.repr : ArgumentStructureClass → ℕ → Std.Format

Equations

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

def AissenPolian2025.ArgumentStructureClass.HasVP : ArgumentStructureClass → Prop

Whether a clause type projects a vP layer (= has an external argument position that could host an intervening DP). @cite{aissen-polian-2025} (9): transitives and unergatives have vP; unaccusatives do not.

Equations

• AissenPolian2025.ArgumentStructureClass.unaccusative.HasVP = False
• AissenPolian2025.ArgumentStructureClass.transitive.HasVP = True
• AissenPolian2025.ArgumentStructureClass.unergative.HasVP = True

@[implicit_reducible]

instance AissenPolian2025.instDecidablePredArgumentStructureClassHasVP : DecidablePred ArgumentStructureClass.HasVP

Equations

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

theorem AissenPolian2025.unaccusative_no_vP : ¬ArgumentStructureClass.unaccusative.HasVP

Unaccusatives lack a vP layer; transitives and unergatives have one. The positive directions are immediate from the def; this lemma names the negative direction for stranding-intervention proofs to consume.

inductive AissenPolian2025.ProbeType : Type

Probe types that trigger movement in Tseltalan. @cite{aissen-polian-2025} §3.1, (10):

• [EPP:D] on T° and Appl°: triggers A-movement of a DP to the probe's specifier. T° and Appl° take rightside specifiers.
• [EPP:WH] on D° (secondary wh-movement) and C° (primary wh-movement): triggers Ā-movement of a wh-phrase.

• dProbe : ProbeType
• whProbe : ProbeType

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqProbeType : DecidableEq ProbeType

Equations

• AissenPolian2025.instDecidableEqProbeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AissenPolian2025.instReprProbeType.repr : ProbeType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AissenPolian2025.instReprProbeType : Repr ProbeType

Equations

• AissenPolian2025.instReprProbeType = { reprPrec := AissenPolian2025.instReprProbeType.repr }

def AissenPolian2025.SelectivelyOpaque : ProbeType → Prop

Selective opacity (@cite{keine-2019}, @cite{aissen-polian-2025} (33)): N⁰ is a horizon for wh-probes on C°. Elements inside the extended projection of N⁰ are invisible to wh-probes, blocking Ā-subextraction.

Crucially, this does NOT apply to D-probes: A-movement of a possessor DP out of a nominal is permitted. The opacity is selective — it depends on the probe type, not on nominal size.

[wh]_{C°} -|| N (A&P's (33))

Equations

• AissenPolian2025.SelectivelyOpaque AissenPolian2025.ProbeType.whProbe = True
• AissenPolian2025.SelectivelyOpaque AissenPolian2025.ProbeType.dProbe = False

@[implicit_reducible]

instance AissenPolian2025.instDecidablePredProbeTypeSelectivelyOpaque : DecidablePred SelectivelyOpaque

Equations

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

theorem AissenPolian2025.wh_probes_blocked : SelectivelyOpaque ProbeType.whProbe

theorem AissenPolian2025.d_probes_pass : ¬SelectivelyOpaque ProbeType.dProbe

def AissenPolian2025.CanĀSubextract : Prop

Ā-subextraction from within a nominal is impossible. Derived from selective opacity: wh-probes cannot see into nominals, regardless of nominal size. The proposition does not depend on NominalSize — @cite{aissen-polian-2025} (33) is the universal nominal-opacity ban A&P argue against the size-relative Diesing/Freezing predecessor of @cite{little-2020a} / @cite{little-2020b}.

Equations

• AissenPolian2025.CanĀSubextract = ¬AissenPolian2025.SelectivelyOpaque AissenPolian2025.ProbeType.whProbe

@[implicit_reducible]

instance AissenPolian2025.instDecidableCanĀSubextract : Decidable CanĀSubextract

Equations

• AissenPolian2025.instDecidableCanĀSubextract = id inferInstance

theorem AissenPolian2025.subextraction_impossible : ¬CanĀSubextract

def AissenPolian2025.ProbeType.toProfile : ProbeType → Minimalist.ProbeProfile

Convert a ProbeType to a ProbeProfile from @cite{keine-2019}.

• dProbe (A-movement, on T°/Appl°) maps to an A-probe on T° with horizon C — the same profile as keineAProbe.
• whProbe (Ā-movement, on D°/C°) maps to an Ā-probe on C° with no horizon — the same profile as keineĀProbe.

Equations

• AissenPolian2025.ProbeType.dProbe.toProfile = Minimalist.keineAProbe
• AissenPolian2025.ProbeType.whProbe.toProfile = Minimalist.keineĀProbe

theorem AissenPolian2025.dProbe_is_A : ProbeType.dProbe.toProfile.isAProbe = true

D-probes are A-probes in Keine's classification.

theorem AissenPolian2025.whProbe_is_Ā : ProbeType.whProbe.toProfile.isĀProbe = true

Wh-probes are Ā-probes in Keine's classification.

theorem AissenPolian2025.probe_type_keine_consistency : ProbeType.dProbe.toProfile.transparentTo Minimalist.Cat.C = false ∧ ProbeType.whProbe.toProfile.transparentTo Minimalist.Cat.C = true

Selective opacity is consistent with Keine's transparency: wh-probes (Ā, no horizon) are transparent to all clause types including CP, while d-probes (A, horizon C) cannot search into CP or TP.

The selectivelyOpaque predicate captures a different facet — opacity of nominals (N° as horizon), not opacity of clauses. But both derive from the same underlying mechanism: probes differ in their horizons.

def AissenPolian2025.DLayerShields (size : NominalSize) : Prop

D-layer shielding: in a specific nominal (DP), D° is closer to an external D-probe (T°'s [EPP:D]) than the possessor inside Spec,PossP or Spec,nP. Attract Closest causes the probe to find D° first, preventing it from reaching the possessor.

Non-specific nominals (PossP/nP) lack a D layer, so T°'s probe reaches the possessor directly.

This is independent of selective opacity: D-probes CAN see into nominals (selectivelyOpaque .dProbe = false), but D° intervenes when present.

Derived from IsSpecific: D-layer shielding ↔ specificity.

Equations

• AissenPolian2025.DLayerShields size = size.IsSpecific

@[implicit_reducible]

instance AissenPolian2025.instDecidablePredNominalSizeDLayerShields : DecidablePred DLayerShields

Equations

• AissenPolian2025.instDecidablePredNominalSizeDLayerShields s = id inferInstance

theorem AissenPolian2025.dp_shields : DLayerShields NominalSize.dp

theorem AissenPolian2025.possP_no_shield : ¬DLayerShields NominalSize.possP

theorem AissenPolian2025.nP_no_shield : ¬DLayerShields NominalSize.nP

inductive AissenPolian2025.ExtractionMode : Type

Two possessor extraction strategies in Tseltalan. @cite{aissen-polian-2025} §3.

• piedPiping : ExtractionMode

  Pied-piping: the entire nominal (including possessor) moves to Spec,CP. Requires D projection: only DPs can be targeted by a wh-probe as a unit.

• stranding : ExtractionMode

  Stranding: the possessor first A-moves out of the nominal via T°'s or Appl°'s [EPP:D] probe, then Ā-moves from the external position. Requires the nominal to be transparent to D-probes (always true) AND no D-layer shielding (non-specific).

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqExtractionMode : DecidableEq ExtractionMode

Equations

• AissenPolian2025.instDecidableEqExtractionMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AissenPolian2025.instReprExtractionMode.repr : ExtractionMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AissenPolian2025.instReprExtractionMode : Repr ExtractionMode

Equations

• AissenPolian2025.instReprExtractionMode = { reprPrec := AissenPolian2025.instReprExtractionMode.repr }

def AissenPolian2025.ExtractionAvailable (mode : ExtractionMode) (size : NominalSize) : Prop

Whether a given extraction mode is available for a nominal of given size, ignoring clause-level intervention.

• Pied-piping: the whole DP moves via wh-probe → requires D projection (specific). Non-DPs cannot undergo wh-movement.
• Stranding: possessor A-moves out via D-probe → requires no D-layer shielding. D-probes see through nominals (selective opacity doesn't apply), but D° intervenes in specific DPs.

@cite{aissen-polian-2025} §3.2.

Equations

• AissenPolian2025.ExtractionAvailable AissenPolian2025.ExtractionMode.piedPiping size = size.IsSpecific
• AissenPolian2025.ExtractionAvailable AissenPolian2025.ExtractionMode.stranding size = ¬AissenPolian2025.DLayerShields size

@[implicit_reducible]

instance AissenPolian2025.instDecidableExtractionAvailable (m : ExtractionMode) (s : NominalSize) : Decidable (ExtractionAvailable m s)

Equations

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

theorem AissenPolian2025.piedPiping_requires_specific : ExtractionAvailable ExtractionMode.piedPiping NominalSize.dp ∧ ¬ExtractionAvailable ExtractionMode.piedPiping NominalSize.possP ∧ ¬ExtractionAvailable ExtractionMode.piedPiping NominalSize.nP

Pied-piping requires specificity (D projection).

theorem AissenPolian2025.stranding_requires_nonspecific : ¬ExtractionAvailable ExtractionMode.stranding NominalSize.dp ∧ ExtractionAvailable ExtractionMode.stranding NominalSize.possP ∧ ExtractionAvailable ExtractionMode.stranding NominalSize.nP

Stranding requires non-specificity (no D-layer shielding).

theorem AissenPolian2025.extraction_always_possible (size : NominalSize) : ExtractionAvailable ExtractionMode.piedPiping size ∨ ExtractionAvailable ExtractionMode.stranding size

Every nominal size admits at least one extraction mode. Possessor extraction is never fully blocked — the available strategy depends on specificity.

theorem AissenPolian2025.extraction_complementary (size : NominalSize) : ExtractionAvailable ExtractionMode.piedPiping size ↔ ¬ExtractionAvailable ExtractionMode.stranding size

Complementary distribution: pied-piping and stranding are mutually exclusive — exactly one is available for each nominal size. Specific nominals admit only pied-piping; non-specific nominals admit only stranding. Both reduce to IsSpecific.

theorem AissenPolian2025.extracted_always_external : ¬CanĀSubextract

Possessor extraction in Tseltalan never involves Ā-subextraction. This follows from selective opacity: wh-probes cannot see into nominals, so the possessor cannot be extracted from within.

Since subextraction is impossible, extraction requires either: (a) moving the whole nominal (pied-piping) — possessor at clause level (b) first A-moving the possessor out (stranding) — possessor external

In both cases, the extracted possessor is external at the point of Ā-movement. This is A&P's claim (3): "An extracted possessor in Tseltalan is always an external possessor."

def AissenPolian2025.NominalSize.toPossessionType : NominalSize → Option Morphology.DM.PossessionType

Map nominal size to possession type from NominalStructure.lean.

• nP-internal possessors (Spec,nP) → inalienable
• PossP-level possessors (Spec,PossP) → alienable
• DP subsumes both; the type depends on internal structure.

Equations

• AissenPolian2025.NominalSize.nP.toPossessionType = some Morphology.DM.PossessionType.inalienable
• AissenPolian2025.NominalSize.possP.toPossessionType = some Morphology.DM.PossessionType.alienable
• AissenPolian2025.NominalSize.dp.toPossessionType = none

theorem AissenPolian2025.inalienable_at_nP : NominalSize.nP.toPossessionType = some Morphology.DM.PossessionType.inalienable

theorem AissenPolian2025.alienable_at_possP : NominalSize.possP.toPossessionType = some Morphology.DM.PossessionType.alienable

theorem AissenPolian2025.highest_agrees_inalienable : NominalSize.nP.highestProjection = Morphology.DM.PossessionType.inalienable.possessorPosition

For non-specific nominals, the highest projection IS the possessor's position, agreeing with PossessionType.possessorPosition from NominalStructure.lean. For DPs, the highest projection is D (the possessor is shielded below).

theorem AissenPolian2025.highest_agrees_alienable : NominalSize.possP.highestProjection = Morphology.DM.PossessionType.alienable.possessorPosition

theorem AissenPolian2025.specificity_convergence_on_stranding : ¬ExtractionAvailable ExtractionMode.stranding NominalSize.dp ∧ Syntax.Binding.SpecificityCondition.blocked Syntax.Binding.SpecificityCondition.ExternalOperator.whTrace Features.Definiteness.Definiteness.definite

Convergence: both A&P's D-layer shielding and the Specificity Condition (see Syntax.Binding.SpecificityCondition) predict that specific DPs resist possessor extraction by stranding/binding into the DP.

Divergence: A&P predict pied-piping IS available for specific DPs (whole DP moves, no subextraction); the Specificity Condition blocks ALL operator binding into specific DPs. The two constraints operate at different levels — D-layer shielding targets A-movement (D-probes), the Specificity Condition targets operator-variable binding.

theorem AissenPolian2025.specificity_divergence_on_piedpiping : ExtractionAvailable ExtractionMode.piedPiping NominalSize.dp ∧ Syntax.Binding.SpecificityCondition.blocked Syntax.Binding.SpecificityCondition.ExternalOperator.whTrace Features.Definiteness.Definiteness.definite

def AissenPolian2025.ψSubjectGramFunction : Fragments.Mayan.Tseltalan.GramFunction

The grammatical function of a ψ-subject. ψ-subjects are always intransitive subjects — they raise from unaccusative clauses where the sole argument is S_O (patientive).

@cite{aissen-polian-2025} §5, Table 1: all ψ-subject constructions are structurally unaccusative, so the ψ-subject is always S_O.

Equations

• AissenPolian2025.ψSubjectGramFunction = Fragments.Mayan.Tseltalan.GramFunction.S_O

def AissenPolian2025.ψSubjectMarkerSet : Fragments.Mayan.MarkerSet

ψ-subject agreement is DERIVED from GramFunction.markerSet: ψ-subjects are S_O, and S_O maps to Set B (absolutive).

Equations

• AissenPolian2025.ψSubjectMarkerSet = AissenPolian2025.ψSubjectGramFunction.markerSet

theorem AissenPolian2025.ψSubject_is_absolutive : ψSubjectMarkerSet = Fragments.Mayan.MarkerSet.setB

ψ-subjects receive Set B (absolutive) agreement — derived from the fact that they are S_O, and S_O maps to Set B.

theorem AissenPolian2025.categorical_has_ψSubject : Features.InformationStructure.JudgmentType.categorical.HasψSubject

theorem AissenPolian2025.thetic_no_ψSubject : ¬Features.InformationStructure.JudgmentType.thetic.HasψSubject

def AissenPolian2025.CanBeψSubject (size : NominalSize) : Prop

A ψ-subject must be specific (= project to DP) to raise to Spec,TP. @cite{aissen-polian-2025} §5.1, p. 85: "the subject of a clause which expresses a categorical judgment cannot be non-specific."

This connects the specificity system to the ψ-subject system: T°'s [EPP:D] probe searches for a DP. If the highest nominal in T°'s domain is non-specific (PossP/nP), it is not a DP, and T°'s probe passes over it. Only a specific DP satisfies the [EPP:D] requirement and raises to Spec,TP as ψ-subject.

Equations

• AissenPolian2025.CanBeψSubject size = size.IsSpecific

@[implicit_reducible]

instance AissenPolian2025.instDecidablePredNominalSizeCanBeψSubject : DecidablePred CanBeψSubject

Equations

• AissenPolian2025.instDecidablePredNominalSizeCanBeψSubject s = id inferInstance

theorem AissenPolian2025.specific_can_be_ψSubject : CanBeψSubject NominalSize.dp

theorem AissenPolian2025.nonspecific_cannot_be_ψSubject_possP : ¬CanBeψSubject NominalSize.possP

theorem AissenPolian2025.nonspecific_cannot_be_ψSubject_nP : ¬CanBeψSubject NominalSize.nP

inductive AissenPolian2025.ψConstruction : Type

The three intransitive-unaccusative ψ-subject constructions of @cite{aissen-polian-2025} §5. Not exhaustive: §6.2 adds path verbs, locative existentials, and two-argument experiential collocations (where the ψ-subject possessor originates inside a PP — see ψPPConstruction below); §7.1 admits Psr-A as ψ-subject in broad-predicate expressions like x's fleas landed on me (not enumerated here, as those are transitive). p. 91 fn 29 / p. 102 fn 34 also note transitive/causative versions of experiential collocations where the possessor externalizes to Spec,ApplP rather than Spec,TP — by definition not ψ-subject constructions.

• predicativePossession : ψConstruction

  Predicative possession: 'X has Y' via existential construction (Tsotsil oy, Tseltal ay). ψ-subject = possessor of pivot. Structure (44): [TP T° [VP V° PossP]] — V° is the existential.

• experientialCollocation : ψConstruction

  Experiential collocation (intransitive, §5.3): 'X is angry' (lit: 'x's head gets mixed up'). ψ-subject = experiencer-possessor. Structure (52): [TP T° [VP V° PossP]].

• lexicalUnaccusative : ψConstruction

  Lexical unaccusative (§5.4): 'X's money was lost.' ψ-subject = possessor of theme (S_O), present only on the non-specific reading where PossP remains.

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqψConstruction : DecidableEq ψConstruction

Equations

• AissenPolian2025.instDecidableEqψConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AissenPolian2025.instReprψConstruction : Repr ψConstruction

Equations

• AissenPolian2025.instReprψConstruction = { reprPrec := AissenPolian2025.instReprψConstruction.repr }

def AissenPolian2025.instReprψConstruction.repr : ψConstruction → ℕ → Std.Format

Equations

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

inductive AissenPolian2025.ψPPConstruction : Type

Additional ψ-subject configurations from @cite{aissen-polian-2025} §6.2 in which the ψ-subject possessor originates as the object of an internal PP (Psr-OP) rather than as a possessor of the verb's direct internal argument. The clauses are still unaccusative (no vP), but the ψ-subject reaches Spec,TP via raising from inside a PP rather than a PossP. These are ψ-subjects in the same sense as ψConstruction above; they are kept in a separate enumeration only because the geometry of extraction (PP-internal origin, locative co-argument) differs from the simple V° + PossP cases of §5.

• pathVerb : ψPPConstruction

  Path verb (§6.2.1): intransitive motion verb (V° + Theme + PP_loc), e.g. (75a) Mach'a och wakax [ta s-na]? 'Who had a cow enter his house?' — ψ-subject = possessor of locative PP, raised over non-specific Theme.

• locativeExistential : ψPPConstruction

  Locative existential (§6.2.2): same predicative oy/ay as predicative possession but with PP rather than PossP, e.g. (77b) Much'u oy ixim [ta s-na]? 'Who has corn in his/her house?' — ψ-subject = possessor of locative PP, Theme is non-specific.

• twoArgExperiential : ψPPConstruction

  Two-argument experiential collocation (§6.2.3): experiencer introduced in PP whose object is the experiential PossP, e.g. (81) Mach'u k'ux-at [ta y-o'tan]? 'Who loves you?' (lit. 'who are you painful in their heart?') — ψ-subject = possessor of PP-experiencer, can extract regardless of Theme specificity.

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqψPPConstruction : DecidableEq ψPPConstruction

Equations

• AissenPolian2025.instDecidableEqψPPConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AissenPolian2025.instReprψPPConstruction.repr : ψPPConstruction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AissenPolian2025.instReprψPPConstruction : Repr ψPPConstruction

Equations

• AissenPolian2025.instReprψPPConstruction = { reprPrec := AissenPolian2025.instReprψPPConstruction.repr }

def AissenPolian2025.ψConstruction.clauseType : ψConstruction → ArgumentStructureClass

The clause type for every §5 ψ-construction is unaccusative (@cite{aissen-polian-2025} p. 83 verbatim: "three unaccusative constructions"). The function is constant over its domain — the constraint is intrinsic to membership in ψConstruction.

Equations

• x✝.clauseType = AissenPolian2025.ArgumentStructureClass.unaccusative

def AissenPolian2025.ψConstruction.PiedPipingPossible : ψConstruction → Prop

Whether pied-piping is possible for a given ψ-construction.

In predicative possession (§5.2, (48a/48b)) and experiential collocations (§5.3, (55a/55b)), the possessor and possessum do NOT form a constituent that can undergo wh-movement: the predicative element (oy/ay, or the verb) intervenes. Only stranding works.

In lexical unaccusatives (§5.4, (62a/62b)), the entire possessive phrase IS the internal argument and can be pied-piped.

Equations

• AissenPolian2025.ψConstruction.predicativePossession.PiedPipingPossible = False
• AissenPolian2025.ψConstruction.experientialCollocation.PiedPipingPossible = False
• AissenPolian2025.ψConstruction.lexicalUnaccusative.PiedPipingPossible = True

@[implicit_reducible]

instance AissenPolian2025.instDecidablePredψConstructionPiedPipingPossible : DecidablePred ψConstruction.PiedPipingPossible

Equations

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

theorem AissenPolian2025.pred_poss_no_piedpiping : ¬ψConstruction.predicativePossession.PiedPipingPossible

theorem AissenPolian2025.exp_coll_no_piedpiping : ¬ψConstruction.experientialCollocation.PiedPipingPossible

theorem AissenPolian2025.lex_unacc_piedpiping_ok : ψConstruction.lexicalUnaccusative.PiedPipingPossible

theorem AissenPolian2025.ψ_constructions_unaccusative (c : ψConstruction) : c.clauseType = ArgumentStructureClass.unaccusative

Every §5 ψ-construction is structurally unaccusative (true by the type signature of clauseType).

theorem AissenPolian2025.ψ_constructions_no_vP (c : ψConstruction) : ¬c.clauseType.HasVP

Every §5 ψ-construction lacks a vP layer. Derived from ψ_constructions_unaccusative and unaccusative_no_vP.

def AissenPolian2025.ψConstruction.ψSubjectFunction : ψConstruction → Fragments.Mayan.Tseltalan.GramFunction

The ψ-subject grammatical function in every §5 construction is S_O (@cite{aissen-polian-2025} §5: in all three, the ψ-subject raises from an unaccusative-internal-argument position).

Equations

• x✝.ψSubjectFunction = Fragments.Mayan.Tseltalan.GramFunction.S_O

theorem AissenPolian2025.ψ_constructions_all_S_O (c : ψConstruction) : c.ψSubjectFunction = Fragments.Mayan.Tseltalan.GramFunction.S_O

Every §5 ψ-construction assigns S_O to its ψ-subject.

theorem AissenPolian2025.ψ_constructions_setB (c : ψConstruction) : c.ψSubjectFunction.markerSet = Fragments.Mayan.MarkerSet.setB

ψ-subject agreement in every §5 construction is Set B, derived from the S_O grammatical function via the shared Tseltalan paradigm.

§6.2 PP-internal ψ-subjects

def AissenPolian2025.ψPPConstruction.clauseType : ψPPConstruction → ArgumentStructureClass

§6.2 PP-internal ψ-constructions are all unaccusative as well: path verbs, locative existentials, and two-arg experiential collocations project no vP layer (the Theme/co-argument may sit in VP but the ψ-subject possessor raises from inside a PP).

Equations

• x✝.clauseType = AissenPolian2025.ArgumentStructureClass.unaccusative

theorem AissenPolian2025.ψ_pp_constructions_unaccusative (c : ψPPConstruction) : c.clauseType = ArgumentStructureClass.unaccusative

For PP-internal ψ-subjects the extracted possessor is Psr-OP (possessor of object of preposition). The §6.2 cases differ from §5 in that the ψ-subject originates inside a PP rather than a PossP, but the grammatical function on the verb tracks the Theme not the extracted possessor. We do not assign a GramFunction here for the extracted Psr-OP because Psr-OP has no per-verb agreement slot in the Tseltalan paradigm.

theorem AissenPolian2025.ψ_pp_constructions_no_vP (c : ψPPConstruction) : ¬c.clauseType.HasVP

inductive AissenPolian2025.DProbeHead : Type

Functional heads that carry [EPP:D] probes triggering A-movement. @cite{aissen-polian-2025} §4.2, §6, Table 4.

• t : DProbeHead
• appl : DProbeHead

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqDProbeHead : DecidableEq DProbeHead

Equations

• AissenPolian2025.instDecidableEqDProbeHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AissenPolian2025.instReprDProbeHead : Repr DProbeHead

Equations

• AissenPolian2025.instReprDProbeHead = { reprPrec := AissenPolian2025.instReprDProbeHead.repr }

def AissenPolian2025.instReprDProbeHead.repr : DProbeHead → ℕ → Std.Format

Equations

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

def AissenPolian2025.HasIntervener (head : DProbeHead) (ct : ArgumentStructureClass) (thematicAppl : Bool) : Prop

Does a clause type have an A-positioned DP that could intervene between a given probe and a lower possessor?

Derived from ArgumentStructureClass.HasVP for T° probes: if there is a vP layer, its specifier hosts an A-positioned DP (agent or S_A). For Appl° probes, intervention occurs when Spec,ApplP is filled by a thematic applied argument (goal, recipient, etc.).

Equations

• AissenPolian2025.HasIntervener AissenPolian2025.DProbeHead.t ct thematicAppl = ct.HasVP
• AissenPolian2025.HasIntervener AissenPolian2025.DProbeHead.appl ct thematicAppl = (thematicAppl = true)

@[implicit_reducible]

instance AissenPolian2025.instDecidableHasIntervener (h : DProbeHead) (c : ArgumentStructureClass) (ta : Bool) : Decidable (HasIntervener h c ta)

Equations

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

def AissenPolian2025.InterventionBlocks (head : DProbeHead) (ct : ArgumentStructureClass) (mode : ExtractionMode) (thematicAppl : Bool := false) : Prop

Possessor stranding is blocked when an A-positioned DP intervenes between the [EPP:D] probe and the possessor. Pied-piping is unaffected: the whole DP moves to Spec,CP via wh-probe, bypassing A-positions entirely.

Equations

• AissenPolian2025.InterventionBlocks head ct AissenPolian2025.ExtractionMode.stranding thematicAppl = AissenPolian2025.HasIntervener head ct thematicAppl
• AissenPolian2025.InterventionBlocks head ct AissenPolian2025.ExtractionMode.piedPiping thematicAppl = False

@[implicit_reducible]

instance AissenPolian2025.instDecidableInterventionBlocks (h : DProbeHead) (c : ArgumentStructureClass) (m : ExtractionMode) (ta : Bool) : Decidable (InterventionBlocks h c m ta)

Equations

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

structure AissenPolian2025.InterventionDatum : Type

An intervention datum for Table 4.

• probe : DProbeHead
• clauseType : ArgumentStructureClass
• mode : ExtractionMode
• thematicAppl : Bool

  Is Spec,ApplP filled by a thematic applied argument?

• blocked : Bool

  Is extraction blocked?

@[implicit_reducible]

instance AissenPolian2025.instDecidableEqInterventionDatum : DecidableEq InterventionDatum

Equations

• AissenPolian2025.instDecidableEqInterventionDatum = AissenPolian2025.instDecidableEqInterventionDatum.decEq

def AissenPolian2025.instDecidableEqInterventionDatum.decEq (x✝ x✝¹ : InterventionDatum) : Decidable (x✝ = x✝¹)

Equations

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

def AissenPolian2025.instReprInterventionDatum.repr : InterventionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AissenPolian2025.instReprInterventionDatum : Repr InterventionDatum

Equations

• AissenPolian2025.instReprInterventionDatum = { reprPrec := AissenPolian2025.instReprInterventionDatum.repr }

def AissenPolian2025.table4 : List InterventionDatum

A re-tabulation of @cite{aissen-polian-2025} Table 4 (p. 103) along a different axis. A&P's Table 4 has 10 rows indexed by (Probe, A-Intervener, Clause Type, Intended Goal) with a yes/no/yes-no Ā-movement? column; it covers Psr-S_O, Psr-O, and Psr-OP goals. Our table re-indexes by (Probe, Clause Type, Mode, ThematicAppl) and tracks blocked per extraction mode. Only the Probe × Clause Type × ThematicAppl rows that fall out of InterventionBlocks are captured here; the Psr-OP / locative-PP rows from A&P's Table 4 (rows for path verbs (75), locative existentials (77b/78), PP-island (67-69)) are not yet modelled because the file currently formalizes only PossP-internal possessors as goals. The ψPPConstruction enumeration above marks the §6.2 cases as a deferred extension target.

Probe	Clause Type	Thematic Appl	Pied-piping	Stranding
T°	unaccusative	—	ok	ok
T°	transitive	—	ok	blocked
T°	unergative	—	ok	blocked
Appl°	(raising appl)	no	ok	ok
Appl°	(thematic appl)	yes	ok	blocked

Equations

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

theorem AissenPolian2025.table4_derived : (table4.all fun (d : InterventionDatum) => d.blocked == decide (InterventionBlocks d.probe d.clauseType d.mode d.thematicAppl)) = true

Table 4 is derivable: every cell matches InterventionBlocks.

theorem AissenPolian2025.piedPiping_never_blocked (head : DProbeHead) (ct : ArgumentStructureClass) (ta : Bool) : ¬InterventionBlocks head ct ExtractionMode.piedPiping ta

Pied-piping is never blocked by intervention (Ā-movement bypasses A-positions).

theorem AissenPolian2025.t_stranding_blocked_iff_vP (ct : ArgumentStructureClass) : InterventionBlocks DProbeHead.t ct ExtractionMode.stranding ↔ ct.HasVP

For T° probes, stranding is blocked iff there is a vP layer.

theorem AissenPolian2025.appl_stranding_blocked_iff_thematic (ct : ArgumentStructureClass) (ta : Bool) : InterventionBlocks DProbeHead.appl ct ExtractionMode.stranding ta ↔ ta = true

For Appl° probes, stranding is blocked iff Spec,ApplP is filled by a thematic applied argument.

Specifier directionality (deferred)

@cite{aissen-polian-2025} §3.1, (10) parameterizes specifier direction per functional head: the Tseltalan default is leftside, but T°, Appl°, and possibly Poss° take rightside specifiers (yielding post-verbal ψ-subjects and external possessors). The previous version of this file defined inductive SpecDirection + tseltalanTSpec / tseltalanApplSpec inline, but these were unused and constituted Fragment-style typological data outside Fragments/. When a downstream consumer needs them, they should land in Fragments/Mayan/Tseltalan.lean (subgroup-shared) or in Core/Word.lean next to HeadDirection (the analogous head-vs- complement axis), not here.

def AissenPolian2025.CanExtractPossessor (size : NominalSize) (head : DProbeHead) (ct : ArgumentStructureClass) (mode : ExtractionMode) (thematicAppl : Bool := false) : Prop

Combining extraction mode availability (§4) with intervention effects (§10): is possessor extraction ultimately possible for a given nominal size, clause type, and probe?

Equations

• AissenPolian2025.CanExtractPossessor size head ct mode thematicAppl = (AissenPolian2025.ExtractionAvailable mode size ∧ ¬AissenPolian2025.InterventionBlocks head ct mode thematicAppl)

@[implicit_reducible]

instance AissenPolian2025.instDecidableCanExtractPossessor (s : NominalSize) (h : DProbeHead) (c : ArgumentStructureClass) (m : ExtractionMode) (ta : Bool) : Decidable (CanExtractPossessor s h c m ta)

Equations

• AissenPolian2025.instDecidableCanExtractPossessor x✝⁴ x✝³ x✝² x✝¹ x✝ = id inferInstance

theorem AissenPolian2025.unaccusative_both_modes : CanExtractPossessor NominalSize.dp DProbeHead.t ArgumentStructureClass.unaccusative ExtractionMode.piedPiping ∧ CanExtractPossessor NominalSize.possP DProbeHead.t ArgumentStructureClass.unaccusative ExtractionMode.stranding ∧ CanExtractPossessor NominalSize.nP DProbeHead.t ArgumentStructureClass.unaccusative ExtractionMode.stranding

In unaccusative clauses via T°, both modes are available.

theorem AissenPolian2025.transitive_only_piedpiping : CanExtractPossessor NominalSize.dp DProbeHead.t ArgumentStructureClass.transitive ExtractionMode.piedPiping ∧ ¬CanExtractPossessor NominalSize.possP DProbeHead.t ArgumentStructureClass.transitive ExtractionMode.stranding ∧ ¬CanExtractPossessor NominalSize.nP DProbeHead.t ArgumentStructureClass.transitive ExtractionMode.stranding

In transitive clauses via T°, only pied-piping works.

theorem AissenPolian2025.raising_appl_stranding : CanExtractPossessor NominalSize.possP DProbeHead.appl ArgumentStructureClass.transitive ExtractionMode.stranding ∧ CanExtractPossessor NominalSize.nP DProbeHead.appl ArgumentStructureClass.transitive ExtractionMode.stranding

Via Appl° raising applicative (no thematic arg), stranding works.

theorem AissenPolian2025.thematic_appl_blocked : ¬CanExtractPossessor NominalSize.possP DProbeHead.appl ArgumentStructureClass.transitive ExtractionMode.stranding true ∧ ¬CanExtractPossessor NominalSize.nP DProbeHead.appl ArgumentStructureClass.transitive ExtractionMode.stranding true

Via Appl° thematic applicative (Goal fills Spec,ApplP), blocked.

theorem AissenPolian2025.ψ_constructions_permit_both_modes (c : ψConstruction) : CanExtractPossessor NominalSize.dp DProbeHead.t c.clauseType ExtractionMode.piedPiping ∧ CanExtractPossessor NominalSize.possP DProbeHead.t c.clauseType ExtractionMode.stranding ∧ CanExtractPossessor NominalSize.nP DProbeHead.t c.clauseType ExtractionMode.stranding

ψ-subject constructions (all unaccusative) permit both extraction modes via T°.

theorem AissenPolian2025.table2_psr_S_O : CanExtractPossessor NominalSize.possP DProbeHead.t ArgumentStructureClass.unaccusative ExtractionMode.stranding ∧ CanExtractPossessor NominalSize.dp DProbeHead.t ArgumentStructureClass.unaccusative ExtractionMode.piedPiping

Table 2 of @cite{aissen-polian-2025} (p. 77): possessor extraction and grammatical function in Ch'ol and Tseltalan.

Mode	Psr-S_O	Psr-O
Stranding	✓	*
Pied-piping	✓	✓

Derived: Psr-S_O is the possessor of the internal argument of an unaccusative clause (no vP → no intervener → stranding OK). Psr-O is the possessor of the internal argument of a transitive clause (vP layer → agent intervenes → stranding blocked).

theorem AissenPolian2025.table2_psr_O : ¬CanExtractPossessor NominalSize.possP DProbeHead.t ArgumentStructureClass.transitive ExtractionMode.stranding ∧ CanExtractPossessor NominalSize.dp DProbeHead.t ArgumentStructureClass.transitive ExtractionMode.piedPiping

theorem AissenPolian2025.stranding_asymmetry_is_vP : CanExtractPossessor NominalSize.possP DProbeHead.t ArgumentStructureClass.unaccusative ExtractionMode.stranding ∧ ¬CanExtractPossessor NominalSize.possP DProbeHead.t ArgumentStructureClass.transitive ExtractionMode.stranding

The stranding asymmetry between Psr-S_O and Psr-O reduces to whether the clause type has a vP layer.

@[reducible, inline]

abbrev AissenPolian2025.tseltalanABSPosition : Fragments.Mayan.ABSPosition

Tseltalan is LOW-ABS: absolutive agreement follows the verb stem. @cite{aissen-polian-2025} p. 97 quotes @cite{aissen-1999a} and @cite{polian-2013} p. 272: "A's extract freely" — there are no syntactic ergativity effects in Tseltalan. The LOW-ABS / HIGH-ABS parameterization (whether Infl° or v° licenses absolutive case) is associated with a robust extraction-asymmetry generalization in the Mayan literature: HIGH-ABS languages exhibit syntactic ergativity (cf. @cite{coon-mateo-pedro-preminger-2014}); LOW-ABS languages do not. The shared Fragments.Mayan.Tseltalan.absPosition constant is the per-subgroup source of truth, definitionally equal to the Tsotsil and Tseltal per-language values.

The intervention effects in Table 4 are NOT about Ā-movement being blocked by A-positioned DPs (as in HIGH-ABS/syntactically ergative languages). Rather, they are about A-movement (possessor raising) being blocked by a closer A-positioned DP, preventing the possessor from reaching an external position from which it could Ā-extract.

Equations

• AissenPolian2025.tseltalanABSPosition = Fragments.Mayan.Tseltalan.absPosition

theorem AissenPolian2025.tseltalan_is_low_abs : tseltalanABSPosition = Fragments.Mayan.ABSPosition.low

theorem AissenPolian2025.tseltalan_case_locus : Fragments.Mayan.toCaseLocus tseltalanABSPosition = Fragments.Mayan.CaseLocus.absDef

LOW-ABS languages have ABS=DEF (v° assigns case to transitive object), not ABS=NOM (Infl° assigns case).

Attract Closest on Concrete Trees

The boolean functions dLayerShields, hasIntervener, and canExtractPossessor above capture the paper's predictions but stipulate them directly. Here we derive them from Attract Closest applied to concrete SyntacticObject trees (@cite{aissen-polian-2025} (9a-c)), using closestGoalB from Minimalist.Agree.

Key derivation: T°'s [EPP:D] probe searches its c-command domain for the closest D-bearing element. The result depends only on tree geometry and which nodes carry D features:

Tree configuration	Closest D-bearer	Possessor reachable?
Unaccusative + PossP	Psr	✓ (stranding)
Unaccusative + DP	D°	✗ (D-layer shields)
Transitive + PossP	Agent	✗ (agent intervenes)
Transitive + DP	Agent	✗ (double blocking)

Leaf Nodes

Clause Trees (@cite{aissen-polian-2025} (9a-c))

(9a) Unaccusative: [TP T° [VP V° OBJECT]] No vP layer — sole argument is complement of V.

(9b) Transitive: [TP T° [vP Agent [v' v° [VP V° OBJECT]]]] Agent in Spec,vP — creates potential intervener.

Object is PossP (non-specific) or DP (specific).

Core Predictions

Each theorem shows that closestGoalB computes the correct result for T°'s [EPP:D] probe searching for the possessor.

theorem AissenPolian2025.unacc_possP_psr_closest : Minimalist.closestGoalB AissenPolian2025.treeUnaccPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = true

Unaccusative + PossP: possessor IS the closest D-bearer to T°. No D-layer, no agent → T°'s probe reaches possessor directly. This is why stranding is available.

theorem AissenPolian2025.unacc_dp_psr_blocked : Minimalist.closestGoalB AissenPolian2025.treeUnaccDP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = false

Unaccusative + DP: possessor is NOT the closest D-bearer. D° is closer to T° than the possessor inside Spec,PossP. This is D-layer shielding — stranding is blocked.

theorem AissenPolian2025.unacc_dp_dHead_closest : Minimalist.closestGoalB AissenPolian2025.treeUnaccDP✝ AissenPolian2025.T₀✝ AissenPolian2025.D₀✝ AissenPolian2025.hasDFeatures✝ = true

Unaccusative + DP: D° IS the closest D-bearer to T°. The whole DP is what T°'s probe attracts — basis for pied-piping.

theorem AissenPolian2025.trans_possP_psr_blocked : Minimalist.closestGoalB AissenPolian2025.treeTransPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = false

Transitive + PossP: possessor is NOT the closest D-bearer. Agent in Spec,vP is closer — the agent intervenes. This is why stranding is blocked in transitives.

theorem AissenPolian2025.trans_possP_agt_closest : Minimalist.closestGoalB AissenPolian2025.treeTransPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Agt✝ AissenPolian2025.hasDFeatures✝ = true

Transitive + PossP: agent IS the closest D-bearer to T°. T°'s probe attracts the agent, not the possessor.

theorem AissenPolian2025.trans_dp_psr_blocked : Minimalist.closestGoalB AissenPolian2025.treeTransDP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = false

Transitive + DP: double blocking — both agent AND D° shield the possessor from T°'s probe.

Bridge Theorems

The tree-geometric derivation agrees with the boolean stipulations from §§3-4. Each conjunction pairs a tree prediction with the corresponding boolean function, showing they make identical claims.

theorem AissenPolian2025.bridge_dLayer_dp : Minimalist.closestGoalB AissenPolian2025.treeUnaccDP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = false ∧ DLayerShields NominalSize.dp

D-layer shielding: tree geometry matches DLayerShields .dp.

theorem AissenPolian2025.bridge_no_dLayer_possP : Minimalist.closestGoalB AissenPolian2025.treeUnaccPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = true ∧ ¬DLayerShields NominalSize.possP

No D-layer for PossP: tree geometry matches DLayerShields .possP.

theorem AissenPolian2025.bridge_intervention_trans : Minimalist.closestGoalB AissenPolian2025.treeTransPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = false ∧ HasIntervener DProbeHead.t ArgumentStructureClass.transitive false

Agent intervention: tree geometry matches HasIntervener .t .transitive.

theorem AissenPolian2025.bridge_no_intervention_unacc : Minimalist.closestGoalB AissenPolian2025.treeUnaccPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = true ∧ ¬HasIntervener DProbeHead.t ArgumentStructureClass.unaccusative false

No intervention in unaccusative: tree geometry matches HasIntervener .t .unaccusative.

Selective Opacity as a Tree Constraint

Selective opacity (@cite{keine-2019}, @cite{aissen-polian-2025} (33)) states that N° is a horizon for wh-probes: C°'s [EPP:WH] probe cannot see elements c-commanded by N° (= inside the nominal's lexical projection). Here we derive this from behindHorizonB applied to concrete trees.

The key geometric fact: in [PossP Psr N°], N° and Psr are sisters, so N° c-commands Psr. This makes Psr invisible to any probe for which N° is a horizon. But D° (sister of PossP, NOT c-commanded by N°) remains visible — which is why pied-piping works.

Together with § 15 (Attract Closest), both pillars of A&P's analysis are now derived from tree geometry:

• D-layer shielding / intervention → closestGoalB (§ 15)
• Selective opacity → behindHorizonB (§ 16)

Core Predictions

theorem AissenPolian2025.psr_behind_horizon_dp : Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccDP✝ AissenPolian2025.C₀✝ AissenPolian2025.Psr✝ Minimalist.Cat.N = true

Psr is behind the N-horizon in the DP tree: C°'s wh-probe cannot subextract the possessor from inside the DP. N° (Psm) c-commands Psr (they are sisters in PossP), so Psr is in N°'s opaque domain.

theorem AissenPolian2025.psr_behind_horizon_possP : Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccPossP✝ AissenPolian2025.C₀✝ AissenPolian2025.Psr✝ Minimalist.Cat.N = true

Psr is behind the N-horizon in the PossP tree: selective opacity applies regardless of nominal size. Even without a D layer, N° c-commands Psr.

theorem AissenPolian2025.dHead_not_behind_horizon : Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccDP✝ AissenPolian2025.C₀✝ AissenPolian2025.D₀✝ Minimalist.Cat.N = false

D° is NOT behind the N-horizon: N° (Psm) does not c-command D°. D° is a sister of PossP, not inside N°'s c-command domain. This is why pied-piping (whole DP movement to Spec,CP) is available: the wh-probe can see D° even though it cannot see inside PossP.

theorem AissenPolian2025.horizon_present_but_dprobe_ignores : Minimalist.behindHorizonB AissenPolian2025.treeUnaccPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ Minimalist.Cat.N = true ∧ ¬SelectivelyOpaque ProbeType.dProbe

The N-horizon is geometrically present even for D-probes — N° c-commands Psr regardless of probe type. The difference is that D-probes IGNORE the horizon (¬ SelectivelyOpaque .dProbe). This is the "selective" in selective opacity: the same tree geometry produces different results for different probe types.

Bridge Theorems

theorem AissenPolian2025.bridge_selective_opacity : Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccDP✝ AissenPolian2025.C₀✝ AissenPolian2025.Psr✝ Minimalist.Cat.N = true ∧ Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccPossP✝ AissenPolian2025.C₀✝ AissenPolian2025.Psr✝ Minimalist.Cat.N = true ∧ ¬CanĀSubextract

Selective opacity from tree geometry: the N-horizon blocks wh-subextraction of Psr from both DP and PossP nominals, agreeing with CanĀSubextract (which is size-independent).

theorem AissenPolian2025.bridge_piedpiping_ok : Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccDP✝ AissenPolian2025.C₀✝ AissenPolian2025.D₀✝ Minimalist.Cat.N = false ∧ ExtractionAvailable ExtractionMode.piedPiping NominalSize.dp

D° visible despite N-horizon: pied-piping is available because D° is outside N°'s c-command domain. Agrees with ExtractionAvailable .piedPiping .dp.

Unified Derivation

theorem AissenPolian2025.unified_tree_derivation : Minimalist.closestGoalB AissenPolian2025.treeUnaccDP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = false ∧ Minimalist.closestGoalB AissenPolian2025.treeTransPossP✝ AissenPolian2025.T₀✝ AissenPolian2025.Psr✝ AissenPolian2025.hasDFeatures✝ = false ∧ Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccDP✝ AissenPolian2025.C₀✝ AissenPolian2025.Psr✝ Minimalist.Cat.N = true ∧ Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccPossP✝ AissenPolian2025.C₀✝ AissenPolian2025.Psr✝ Minimalist.Cat.N = true ∧ Minimalist.behindHorizonB AissenPolian2025.treeCPUnaccDP✝ AissenPolian2025.C₀✝ AissenPolian2025.D₀✝ Minimalist.Cat.N = false

Both pillars from tree geometry: D-layer shielding, agent intervention, selective opacity, and pied-piping availability all follow from Attract Closest + N-horizons on concrete trees.

(a) D-layer shielding: D° closer to T° than Psr (closestGoalB) (b) Agent intervention: Agt closer to T° than Psr (closestGoalB) (c) Selective opacity: N° c-commands Psr (behindHorizonB) (d) Pied-piping: D° NOT c-commanded by N° (behindHorizonB)