Kaqchikel Focus Fragment

Realization data for the Kaqchikel focus construction, from the Patzún variety described by [Erl16]: a focused argument fronts to immediately preverbal position marked by the particle ja, and a focused transitive subject (A) additionally switches the verb to Agent Focus (Extraction.lean) — the ergative split, since S fronts like A but intransitive verbs have no AF form.

Main declarations

• Kaqchikel.focusRealize: focus realization by focused argument position, as a Features.Marking reflex list.
• Kaqchikel.af_reflex_iff: the verb-hosted AF reflex appears exactly under transitive-subject (A) focus.
• Kaqchikel.marked_subject_is_A_not_S: the A-focus vs S-focus split that Extraction.ExtractionTarget cannot draw.

Implementation notes

Focus fronting is one of four AF triggers ([Erl16] §2.2); the others (wh-questions, relative clauses, argument existentials) differ only in the fronted phrase's own marking and are not separately encoded. Preverbal subject-initial orders are topicalization, not focus (no ja, no AF). Across Mayan, information focus stays in situ and unmarked except for the transitive subject, which in AF-languages must front and trigger AF ([Ais17]); Kaqchikel-specific in-situ data are not in the sources here, so focusRealize covers the fronted construction only and no EveryTargetOvert claim is made.

Sites

inductive Kaqchikel.FocusSite : Type

The constituents a Kaqchikel focus reflex attaches to: the fronted focus phrase itself (hosting ja and the fronting) or the verbal complex (hosting the AF morpheme).

• focusPhrase : FocusSite
• verb : FocusSite

@[implicit_reducible]

instance Kaqchikel.instDecidableEqFocusSite : DecidableEq FocusSite

Equations

• Kaqchikel.instDecidableEqFocusSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Kaqchikel.instReprFocusSite : Repr FocusSite

Equations

• Kaqchikel.instReprFocusSite = { reprPrec := Kaqchikel.instReprFocusSite.repr }

def Kaqchikel.instReprFocusSite.repr : FocusSite → ℕ → Std.Format

Equations

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

Realization

def Kaqchikel.focusRealize : ArgPosition → Features.Marking FocusSite

Focus realization by focused argument position ([Erl16] §2.2): every focused argument fronts (VOS base order, so fronting is never string-vacuous) and hosts ja; a focused transitive subject (A) additionally switches the verb to AF — the ergative split, since S fronts like A but intransitive verbs have no AF form. Ditransitive R/T focus is unattested in the source and falls to the A-less default.

Equations

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

theorem Kaqchikel.af_reflex_iff (p : ArgPosition) : Features.Reflex.morpheme FocusSite.verb ∈ (focusRealize p).reflexes ↔ p = Features.Prominence.ArgumentRole.A

The verb-hosted reflex (AF) appears under transitive-subject focus only.

theorem Kaqchikel.marked_subject_is_A_not_S : Features.Reflex.morpheme FocusSite.verb ∈ (focusRealize Features.Prominence.ArgumentRole.A).reflexes ∧ Features.Reflex.morpheme FocusSite.verb ∉ (focusRealize Features.Prominence.ArgumentRole.S).reflexes

The ergative split in focus marking: A-focus switches the verb to AF while S-focus does not, although Extraction.ExtractionTarget maps both to .subject — the verb reflex of Extraction.realize .subject (Extraction.lean) marks transitive subjects only.