Overt reflexes of a designated constituent

Observation vocabulary for the perceptible traces a grammar produces because a constituent bears a designated status — a focus ([HZ04] Tangale, [HZ07] Hausa, [BE23]), an A′-extraction site (Syntax/Extraction.lean, the Mayan fragments), an intermediate landing site of successive-cyclic movement ([mccloskey-2002], [georgi-2017]). A Marking pairs the target with its list of Reflexes, each a marking Modality at a host constituent; the modalities classify by Channel — the literature's phonological vs morphological vs syntactic reflex cut — with the process supplying the unity. Like Features.Judgment for acceptability, this is a prediction-target vocabulary: theories never consume it as machinery; studies translate theory-native predictions into it.

Scope: perceptible traces only. Semantic reflexes of movement (intermediate scope/reconstruction effects) share the site indexing but are interpretation facts, formalized in their studies. A default exponent that surfaces regardless of the designation (Wolof expletive l-, [georgi-2017]) is not a reflex — reflexes covary with the target — and zero is never a reflex: covert marking is exponence-side competition (blocking), not a marking modality.

Implementation notes

String-vacuous operations (Hausa subject fronting) contribute no reflex: the reflex list carries only perceptible alternants — including paradigmatic ones such as deletion of otherwise-expected material (Malay voice-marker deletion) — which is what makes IsOvert honest. With constituents ordered by containment, each reflex host stands in exactly one HostRelation to the target; ExactlyTargets, PiedPipes, and [BE23]'s AntiPiedPipes are derived from that classification. The overlap-weakening of [HZ07]'s Ex-Situ Generalisation remains deferred; note Mereology.Overlap is vacuous over orders with a bottom, so that member must use ¬ Disjoint or bot-free carriers.

inductive Features.Channel : Type

The channel of a reflex: the literature's phonological vs morphological vs syntactic reflex cut (reflexes of one process are individuated by the module whose output carries the trace).

• phonological : Channel
• morphological : Channel
• syntactic : Channel

@[implicit_reducible]

instance Features.instDecidableEqChannel : DecidableEq Channel

Equations

• Features.instDecidableEqChannel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprChannel.repr : Channel → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Features.instReprChannel.repr Features.Channel.syntactic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Channel.syntactic")).group prec✝

@[implicit_reducible]

instance Features.instReprChannel : Repr Channel

Equations

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

@[implicit_reducible]

instance Features.instFintypeChannel : Fintype Channel

Equations

• Features.instFintypeChannel = { elems := { val := ↑Features.Channel.enumList, nodup := Features.Channel.enumList_nodup }, complete := Features.instFintypeChannel._proof_1 }

inductive Features.Modality : Type

A marking modality: the kind of perceptible perturbation. The two prosodic cases keep the demarcative vs culminative cut visible.

• displacement : Modality

  Syntactic: an exponent constituent surfaces displaced from its base position (movement that is not string-vacuous).

• morpheme : Modality

  Morphological: a dedicated morpheme — affix, particle, or form alternation — at a host constituent.

• boundary : Modality

  Phonological, demarcative: a phrase-edge at a host constituent (the Tangale/Chadic pattern).

• prominence : Modality

  Phonological, culminative: metrical prominence on a host (the English pattern).

@[implicit_reducible]

instance Features.instDecidableEqModality : DecidableEq Modality

Equations

• Features.instDecidableEqModality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprModality.repr : Modality → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Features.instReprModality.repr Features.Modality.morpheme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Modality.morpheme")).group prec✝
• Features.instReprModality.repr Features.Modality.boundary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Features.Modality.boundary")).group prec✝

@[implicit_reducible]

instance Features.instReprModality : Repr Modality

Equations

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

@[implicit_reducible]

instance Features.instFintypeModality : Fintype Modality

Equations

• Features.instFintypeModality = { elems := { val := ↑Features.Modality.enumList, nodup := Features.Modality.enumList_nodup }, complete := Features.instFintypeModality._proof_1 }

def Features.Modality.channel : Modality → Channel

The channel a modality marks in.

Equations

• Features.Modality.displacement.channel = Features.Channel.syntactic
• Features.Modality.morpheme.channel = Features.Channel.morphological
• Features.Modality.boundary.channel = Features.Channel.phonological
• Features.Modality.prominence.channel = Features.Channel.phonological

structure Features.Reflex (C : Type u_2) : Type u_2

A single overt reflex: a marking modality at a host constituent.

• modality : Modality
• host : C

@[implicit_reducible]

instance Features.instDecidableEqReflex {C✝ : Type u_2} [DecidableEq C✝] : DecidableEq (Reflex C✝)

Equations

• Features.instDecidableEqReflex = Features.instDecidableEqReflex.decEq

def Features.instDecidableEqReflex.decEq {C✝ : Type u_2} [DecidableEq C✝] (x✝ x✝¹ : Reflex C✝) : Decidable (x✝ = x✝¹)

Equations

• Features.instDecidableEqReflex.decEq { modality := a, host := a_1 } { modality := b, host := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Features.instReprReflex.repr {C✝ : Type u_2} [Repr C✝] : Reflex C✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprReflex {C✝ : Type u_2} [Repr C✝] : Repr (Reflex C✝)

Equations

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

def Features.Reflex.displacement {C : Type u_1} (exponent : C) : Reflex C

An exponent constituent surfaces displaced from its base position.

Equations

• Features.Reflex.displacement exponent = { modality := Features.Modality.displacement, host := exponent }

def Features.Reflex.morpheme {C : Type u_1} (host : C) : Reflex C

A dedicated morpheme at a host constituent.

Equations

• Features.Reflex.morpheme host = { modality := Features.Modality.morpheme, host := host }

def Features.Reflex.boundary {C : Type u_1} (edge : C) : Reflex C

A demarcative prosodic event: a phrase-edge at a host constituent.

Equations

• Features.Reflex.boundary edge = { modality := Features.Modality.boundary, host := edge }

def Features.Reflex.prominence {C : Type u_1} (host : C) : Reflex C

A culminative prosodic event: metrical prominence on a host.

Equations

• Features.Reflex.prominence host = { modality := Features.Modality.prominence, host := host }

def Features.Reflex.Overt {C : Type u_1} (rs : List (Reflex C)) : Prop

Some reflex surfaces: the list carries perceptible material.

Equations

• Features.Reflex.Overt rs = (rs ≠ [])

@[implicit_reducible]

instance Features.Reflex.instDecidableOvert {C : Type u_1} (rs : List (Reflex C)) : Decidable (Overt rs)

Equations

• Features.Reflex.instDecidableOvert rs = decidable_of_iff (¬rs.isEmpty = true) ⋯

structure Features.Marking (C : Type u_2) : Type u_2

A marking: the designated target constituent and the grammatical reflexes marking it.

• target : C
• reflexes : List (Reflex C)

@[implicit_reducible]

instance Features.instReprMarking {C✝ : Type u_2} [Repr C✝] : Repr (Marking C✝)

Equations

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

def Features.instReprMarking.repr {C✝ : Type u_2} [Repr C✝] : Marking C✝ → ℕ → Std.Format

Equations

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

def Features.Marking.IsOvert {C : Type u_1} (m : Marking C) : Prop

Overt marking, derived: some reflex surfaces.

Equations

• m.IsOvert = Features.Reflex.Overt m.reflexes

@[implicit_reducible]

instance Features.instDecidableIsOvert {C : Type u_1} (m : Marking C) : Decidable m.IsOvert

Equations

• Features.instDecidableIsOvert m = Features.instDecidableIsOvert._aux_1 m

Host–target containment

With constituents ordered by containment, each reflex host stands in exactly one relation to the target: exact targeting, pied-piping (host properly contains the target), [BE23]'s anti-pied-piping (host properly contained in the target, attested in over sixty languages), or external hosting (host incomparable to the target — e.g. verb-hosted extraction morphology marking an extracted argument, the Mayan Agent Focus configuration).

inductive Features.HostRelation : Type

Where a reflex host sits relative to the target in the containment order.

• exact : HostRelation
• piedPiping : HostRelation
• antiPiedPiping : HostRelation
• external : HostRelation

@[implicit_reducible]

instance Features.instDecidableEqHostRelation : DecidableEq HostRelation

Equations

• Features.instDecidableEqHostRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprHostRelation.repr : HostRelation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprHostRelation : Repr HostRelation

Equations

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

@[implicit_reducible]

instance Features.instFintypeHostRelation : Fintype HostRelation

Equations

• Features.instFintypeHostRelation = { elems := { val := ↑Features.HostRelation.enumList, nodup := Features.HostRelation.enumList_nodup }, complete := Features.instFintypeHostRelation._proof_1 }

def Features.Reflex.relationTo {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] (ρ : Reflex C) (t : C) : HostRelation

Classify a reflex host's position relative to a target. Total by construction: the four HostRelation cells partition the possibilities.

Equations

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

def Features.Marking.PiedPipes {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] (m : Marking C) : Prop

Some reflex targets a constituent properly containing the target — Ross's pied-piping, generalized from movement to all marking morphosyntax by [BE23].

Equations

• m.PiedPipes = ∃ ρ ∈ m.reflexes, ρ.relationTo m.target = Features.HostRelation.piedPiping

def Features.Marking.AntiPiedPipes {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] (m : Marking C) : Prop

Some reflex targets a proper subconstituent of the target — [BE23]'s anti-pied-piping.

Equations

• m.AntiPiedPipes = ∃ ρ ∈ m.reflexes, ρ.relationTo m.target = Features.HostRelation.antiPiedPiping

def Features.Marking.ExactlyTargets {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] (m : Marking C) : Prop

Every reflex targets the designated constituent itself.

Equations

• m.ExactlyTargets = ∀ ρ ∈ m.reflexes, ρ.relationTo m.target = Features.HostRelation.exact

@[implicit_reducible]

instance Features.instDecidablePiedPipes {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] (m : Marking C) : Decidable m.PiedPipes

Equations

• Features.instDecidablePiedPipes m = Features.instDecidablePiedPipes._aux_1 m

@[implicit_reducible]

instance Features.instDecidableAntiPiedPipes {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] (m : Marking C) : Decidable m.AntiPiedPipes

Equations

• Features.instDecidableAntiPiedPipes m = Features.instDecidableAntiPiedPipes._aux_1 m

@[implicit_reducible]

instance Features.instDecidableExactlyTargets {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] (m : Marking C) : Decidable m.ExactlyTargets

Equations

• Features.instDecidableExactlyTargets m = Features.instDecidableExactlyTargets._aux_1 m

theorem Features.Marking.PiedPipes.not_exactlyTargets {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] {m : Marking C} (h : m.PiedPipes) : ¬m.ExactlyTargets

A pied-piping marking does not exactly target its designee.

theorem Features.Marking.AntiPiedPipes.not_exactlyTargets {C : Type u_1} [PartialOrder C] [DecidableEq C] [DecidableLT C] {m : Marking C} (h : m.AntiPiedPipes) : ¬m.ExactlyTargets

An anti-pied-piping marking does not exactly target its designee.

def Features.EveryTargetOvert {C : Type u_1} {I : Type u_2} (realize : I → Marking C) : Prop

The universalist claim over a marking system realize: every designated target receives an overt reflex. Refutation target: Hausa and Tangale focus each refute their instance ([HZ04], [HZ07]).

Equations

• Features.EveryTargetOvert realize = ∀ (i : I), (realize i).IsOvert