Martínez Vera (2026): Verum, contrast, and evidentiality in Saraguro Kichwa

@cite{martinez-vera-2026} @cite{martinez-vera-2024} @cite{martinez-vera-camacho-2025} @cite{faller-2002} @cite{faller-2019a} @cite{murray-2014} @cite{murray-2017} @cite{tellings-2014} @cite{grzech-2020} @cite{bendezu-2023} @cite{sanchez-2010} @cite{hintz-hintz-2017} @cite{cole-1982} @cite{roelofsen-vangool-2010} @cite{roelofsen-farkas-2015} @cite{simons-tonhauser-beaver-roberts-2010} @cite{krifka-2014} @cite{rooth-1985} @cite{rooth-1992} @cite{hirsch-2017} @cite{hohle-1992} @cite{romero-han-2004} @cite{kiss-1998} @cite{matthewson-2021} @cite{matthewson-2004} @cite{bochnak-matthewson-2015} @cite{gutzmann-hartmann-matthewson-2020} @cite{goodhue-2022a} @cite{rochemont-2018}

Saraguro Kichwa (qvj) marker =mi is analysed as a focus marker whose felicity presupposes a highlighted, strengthened alternative that entails the negation of the scope proposition (paper's def. 37).

Three empirical signatures:

1. =mi is licensed when ¬p is salient (biased question, assertion of ¬p, or a reportative-evidential antecedent).
2. =mi is licensed in matrix declaratives following a reportative evidential -shka, but NOT following a direct evidential -rka.
3. =mi surfaces in contrastive (corrective) uses, sister to focus strategies like English only (@cite{rochemont-2018}, @cite{hirsch-2017}).

What this study formalises

• miFelicitous — paper eq. (37), reduced to the polar alternative-set case (innocently excludable alternatives are absent from polar partitions, so exhaustification collapses to identity).
• polarQUD p — the QUD over which a verum-marker felicity question is settled, built from Core.Question.polar. Its alt = {p, pᶜ}, so Highlighting.AddressesQUD does real filtering work.
• updateAfterAct — generic discourse update that adds an act's EvidentialAct.raisedPropositions to the salient set. No match-on-commitsToScope here: the substrate-level theorems present_raises_polar_negation and assert_does_not_raise_polar_negation in Theories/Discourse/EvidentialIllocution carry the load.
• The headline contrast (paper exx. 47–50): =mi is felicitous after present (reportative -shka) and infelicitous after assert (direct -rka). Proofs project from substrate.
• mi_polar_iff_verumFelicitous — the cross-paper bridge theorem showing MV's polar-reduction miFelicitous is equivalent to Höhle's verumFelicitous on the same input.
• mv_partition_neq_romeroHan_partition — the cross-framework divergence theorem showing MV's polar partition {p, pᶜ} is in general distinct from Romero & Han's verum partition {forSureCG p, ¬forSureCG p}. Makes the line-a (focus) vs line-b (CG-modal verum operator) split visible at the type level.

Substrate consumed

Substrate	Provides
Theories/Semantics/Composition/Layered	BiLayered W ⟨A, N⟩ pair, three composition rules
Theories/Semantics/Highlighting	HighlightingContext, Highlighted, AddressesQUD
Theories/Discourse/EvidentialIllocution	assert, present, EvidentialAct, raisedPropositions
Features/Evidentiality	EvidentialSource (direct, hearsay, inference)
Core/Question/Hamblin	Question.polar for the polar QUD

Methodological note

The paper's data is original fieldwork with six Saraguro speakers, following @cite{matthewson-2004}, @cite{bochnak-matthewson-2015}. Per CLAUDE.md (per-language paper-specific data lives in Studies, not Fragments), the felicity-judgment apparatus stays in this file; the neutral consensus typology — that Saraguro Kichwa has a 3-way evidential paradigm with the discourse-sensitive enclitic =mi — lives in Fragments/Quechua/SaraguroKichwa/Evidentiality.lean.

§ 1. The =mi denotation (paper eq. 37, polar reduction)

def Phenomena.Verum.Studies.MartinezVera2026.miFelicitous {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (alts : Set (Set W)) (S : Semantics.Composition.Layered.BiLayered W) : Prop

Felicity condition for =mi attached to a scope expression S in context c, given a focus alternative set alts. This is paper eq. (37) for the case where alts is the polar partition {p, pᶜ}: polar partitions admit no innocently excludable alternatives (negating both gives {¬p, ¬pᶜ} = {¬p, p}, contradictory), so exhaustification collapses to identity, and the paper's "exh(q) entails ¬S.A" reduces to "q ⊆ S.atIssueᶜ".

Note: the polar reduction does NOT extend to constituent-focus contrast cases (paper §3 examples 22–28), where alts may include multiple elements with overlap. Those would consume the full Theories/Semantics/Exhaustification.Excluder machinery.

Equations

• Phenomena.Verum.Studies.MartinezVera2026.miFelicitous c alts S = ∃ q ∈ alts, Semantics.Highlighting.Highlighted c q ∧ q ⊆ {w : W | S.atIssue w}ᶜ

§ 2. The polar QUD setup

def Phenomena.Verum.Studies.MartinezVera2026.polarQUD {W : Type u_1} (p : Set W) : Semantics.Highlighting.HighlightingContext W

The polar QUD over a contingent proposition p: alternatives are {p, pᶜ}. Built from Core.Question.polar p. Used as the QUD slot in the discourse contexts that license a =mi follow-up.

With this (non-trivial) QUD, AddressesQUD does real filtering work: a proposition addresses polarQUD p iff it is comparable to p or to pᶜ. Both p and pᶜ themselves trivially address it (each is a subset of itself), so the highlighted alternatives in the headline contrast satisfy the QUD-addressing requirement of Highlighted.

Equations

• Phenomena.Verum.Studies.MartinezVera2026.polarQUD p = { salient := ∅, qud := Core.Question.polar p }

theorem Phenomena.Verum.Studies.MartinezVera2026.mem_alt_polar {W : Type u_1} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : p ∈ (Core.Question.polar p).alt

Either p or pᶜ is itself a maximal answer to polar p, when p is contingent (p ≠ ∅ and p ≠ Set.univ). This is the substrate fact Core.Question.alt_polar_of_nontrivial.

theorem Phenomena.Verum.Studies.MartinezVera2026.mem_alt_polar_compl {W : Type u_1} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : pᶜ ∈ (Core.Question.polar p).alt

theorem Phenomena.Verum.Studies.MartinezVera2026.addresses_polarQUD_self {W : Type u_1} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : Semantics.Highlighting.AddressesQUD (polarQUD p).qud p

p itself addresses the polar QUD over p: it equals one of the two alternatives. Requires p contingent so the polar partition is non-trivial.

theorem Phenomena.Verum.Studies.MartinezVera2026.addresses_polarQUD_compl {W : Type u_1} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : Semantics.Highlighting.AddressesQUD (polarQUD p).qud pᶜ

pᶜ addresses the polar QUD over p: it equals the other alternative. Requires p contingent.

§ 3. Discourse-update map (generic; consumes substrate)

updateAfterAct c a adds the propositions an act a raises to the salient set of c. The match-on-commitsToScope lives in the substrate (EvidentialAct.raisedPropositions), not here — verum studies, biased polar-question studies, and reportative-evidential studies all consume the same generic update.

def Phenomena.Verum.Studies.MartinezVera2026.updateAfterAct {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (a : Discourse.EvidentialIllocution.EvidentialAct W) : Semantics.Highlighting.HighlightingContext W

Generic discourse-update: an act adds the propositions it raises to the salient set. The behaviour-distinguishing match is delegated to the substrate's EvidentialAct.raisedPropositions.

Equations

• Phenomena.Verum.Studies.MartinezVera2026.updateAfterAct c a = { salient := c.salient ∪ a.raisedPropositions, qud := c.qud }

@[simp]

theorem Phenomena.Verum.Studies.MartinezVera2026.salient_updateAfterAct {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (a : Discourse.EvidentialIllocution.EvidentialAct W) : (updateAfterAct c a).salient = c.salient ∪ a.raisedPropositions

@[simp]

theorem Phenomena.Verum.Studies.MartinezVera2026.qud_updateAfterAct {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (a : Discourse.EvidentialIllocution.EvidentialAct W) : (updateAfterAct c a).qud = c.qud

§ 4. The headline contrast (paper exx. 47–50)

The proofs derive from the substrate facts present_raises_polar_negation and assert_does_not_raise_polar_negation. The match-on-commitsToScope is exercised once in the substrate; here the consequences fall out.

theorem Phenomena.Verum.Studies.MartinezVera2026.mi_felicitous_after_present {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : miFelicitous (updateAfterAct (polarQUD p) (Discourse.EvidentialIllocution.present s a (Semantics.Composition.Layered.BiLayered.ofProp fun (x : W) => x ∈ p))) {p, pᶜ} (Semantics.Composition.Layered.BiLayered.ofProp fun (x : W) => x ∈ p)

After a reportative-evidential present(p) update, a =mi-marked follow-up confirming p is felicitous: the witness is the highlighted pᶜ, which is raised by present (substrate: present_raises_polar_negation) and addresses the polar QUD over p (substrate: addresses_polarQUD_compl).

Paper exx. 21/48. Hypotheses hne and hnu are the contingency conditions on the scope: the paper assumes contingent scopes throughout. The alternative set is the polar partition {p, pᶜ}.

theorem Phenomena.Verum.Studies.MartinezVera2026.mi_infelicitous_after_assert {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : ¬miFelicitous (updateAfterAct (polarQUD p) (Discourse.EvidentialIllocution.assert s a (Semantics.Composition.Layered.BiLayered.ofProp fun (x : W) => x ∈ p))) {p, pᶜ} (Semantics.Composition.Layered.BiLayered.ofProp fun (x : W) => x ∈ p)

After a direct-evidential assert(p) update, a =mi-marked follow-up confirming p is NOT felicitous: only p itself is raised by assert (substrate: assert_does_not_raise_polar_negation), and p ⊆ pᶜ would force p = ∅, contradicting contingency.

Paper ex. 47 — the contrast that motivates the present/assert distinction.

§ 5. Cross-paper bridge: Höhle 1992 ↔ MV 2026 (polar reduction)

For the polar alternative-set case {β.atIssue, β.atIssueᶜ}, MV's miFelicitous reduces to Höhle's verumFelicitous: both demand that ¬β.atIssue be highlighted in the context. This makes the agreement between the focus-on-polarity (Höhle) and focus-marker (MV) accounts explicit at the type level. The disagreement with @cite{romero-han-2004}'s CG-modal verum surfaces as the partition divergence in §6 below.

theorem Phenomena.Verum.Studies.MartinezVera2026.mi_polar_iff_verumFelicitous {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.Composition.Layered.BiLayered W) (hne : ∃ (w : W), β.atIssue w) : miFelicitous c {{w : W | β.atIssue w}, {w : W | β.atIssue w}ᶜ} β ↔ Hohle1992.verumFelicitous c β

For the polar alternative-set case with contingent scope, MV's miFelicitous reduces to Höhle's verumFelicitous: both predicates demand that ¬β.atIssue (the scope's complement) be highlighted. The contingency hypothesis hne : ∃ w, β.atIssue w rules out the degenerate empty-scope case where every q ⊆ qᶜ vacuously and the bridge would require Highlighted c univ from Highlighted c ∅ — not generally derivable.

The mp direction: of the two polar alternatives, only β.atIssueᶜ can satisfy q ⊆ β.atIssueᶜ non-trivially (given contingent scope). The mpr direction packages the highlighted complement directly.

def Phenomena.Verum.Studies.MartinezVera2026.miAsVerumOperatorPolar {W : Type u_1} : Basic.VerumOperator W

The MV =mi denotation packaged as a VerumOperator over the polar alternative set {β.atIssue, β.atIssueᶜ}. The shared abstraction lets mi_polar_iff_verumFelicitous (above) be re-stated as a felicity equivalence between two VerumOperator W instances.

Equations

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

@[simp]

theorem Phenomena.Verum.Studies.MartinezVera2026.miAsVerumOperatorPolar_apply {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.Composition.Layered.BiLayered W) : miAsVerumOperatorPolar.felicitous c β = miFelicitous c {{w : W | β.atIssue w}, {w : W | β.atIssue w}ᶜ} β

theorem Phenomena.Verum.Studies.MartinezVera2026.mi_eq_hohle_as_verumOperator {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.Composition.Layered.BiLayered W) (hne : ∃ (w : W), β.atIssue w) : miAsVerumOperatorPolar.felicitous c β ↔ Hohle1992.hohleAsVerumOperator.felicitous c β

Cross-paper bridge restated at the VerumOperator level: under contingent scope, MV's polar-reduction operator and Höhle's verum-focus operator are extensionally equivalent. The first formal cross-paper agreement in the Verum/ directory.

§ 6. Cross-framework divergence: MV's partition vs R&H's verum partition

Romero & Han 2004 analyse verum as a CG-modal operator forSureCG producing an unbalanced polar partition {forSureCG p, ¬forSureCG p} (line-b account). MV implicitly takes a line-a (focus over polarity) position: the partition over which =mi operates is the standard polar {p, pᶜ}. These two partitions are in general distinct — the line-a/b debate (Goodhue 2022a §1) is non-vacuous.

theorem Phenomena.Verum.Studies.MartinezVera2026.mv_partition_can_diverge_from_romeroHan_partition : ∃ (W : Type) (p : Set W) (verumP : Set W), verumP ≠ p ∧ {p, pᶜ} ≠ {verumP, verumPᶜ}

The MV polar partition {p, pᶜ} and the R&H verum partition {forSureCG p, ¬forSureCG p} are in general distinct. There exist contexts (witness: any model where forSureCG p ≠ p) in which MV's line-a focus partition and R&H's line-b VERUM partition pick out different cells.

Witness construction: the forSureCG operator can fail to coincide with p whenever the speaker's epistemic state and conversational goals don't trivially settle p — which is the very case that makes verum interesting (cf. R&H §3 on biased polar questions).

§ 7. The defining commitment contrast (corollary of substrate)

Direct evidentials commit the speaker to scope; reportatives do not. This is Discourse.EvidentialIllocution.assert_commitsToScope and present_commitsToScope packaged as a single statement. The reason present highlights ¬p (and assert doesn't) is downstream of this commitment difference, formalised in the substrate's present_raises_polar_negation / assert_does_not_raise_polar_negation.

theorem Phenomena.Verum.Studies.MartinezVera2026.direct_commits_reportative_does_not {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (Discourse.EvidentialIllocution.assert s a β).commitsToScope = true ∧ (Discourse.EvidentialIllocution.present s a β).commitsToScope = false

§ 8. Cross-Quechuan family contrast (paper §5)

A label-only typology of published =mi analyses across Quechuan varieties. This is currently a decide-distinct enum, not a semantic taxonomy — each cell is a stand-in for a future per-paper study file (Faller2002, Tellings2014, Grzech2020, Bendezú2023). Once those exist, this enum should be replaced by MiSemantics W-shaped inhabitants whose pairwise distinctness becomes a substantive theorem about predicted felicity profiles, not an enum tautology.

Currently retained as a drift sentry: if a future formalisation collapses any two analyses into one (e.g. by treating "epistemic authority" as a sub-case of "verum + focus"), the pairwise_distinct proof fails and forces a re-evaluation of the paper's typological-divergence claim.

inductive Phenomena.Verum.Studies.MartinezVera2026.MiAnalysis : Type

Analytic stance taken on =mi in a given Quechuan variety, as surveyed in paper §5. Five mutually-incompatible claims, one per variety. Each is a label awaiting a future per-paper study.

• verumPlusFocus : MiAnalysis

  Verum + focus marker requiring discourse sensitivity to the QUD (Saraguro Kichwa per @cite{martinez-vera-2026}).

• verumPlusContrast : MiAnalysis

  Verum + corrective contrast (Conchucos Quechua per @cite{bendezu-2023}).

• directEvidentialOnly : MiAnalysis

  Pure (best-possible-grounds) direct evidential (Cuzco Quechua per @cite{faller-2002}, @cite{sanchez-2010}).

• pureEvidentialNoFocus : MiAnalysis

  Pure evidential, no focus role (Imbabura Kichwa per @cite{tellings-2014}).

• epistemicAuthority : MiAnalysis

  Epistemic-authority marker (Upper Napo Kichwa per @cite{grzech-2020}).

@[implicit_reducible]

instance Phenomena.Verum.Studies.MartinezVera2026.instDecidableEqMiAnalysis : DecidableEq MiAnalysis

Equations

• Phenomena.Verum.Studies.MartinezVera2026.instDecidableEqMiAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Verum.Studies.MartinezVera2026.instReprMiAnalysis.repr : MiAnalysis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Verum.Studies.MartinezVera2026.instReprMiAnalysis : Repr MiAnalysis

Equations

• Phenomena.Verum.Studies.MartinezVera2026.instReprMiAnalysis = { reprPrec := Phenomena.Verum.Studies.MartinezVera2026.instReprMiAnalysis.repr }

@[implicit_reducible]

instance Phenomena.Verum.Studies.MartinezVera2026.instInhabitedMiAnalysis : Inhabited MiAnalysis

Equations

• Phenomena.Verum.Studies.MartinezVera2026.instInhabitedMiAnalysis = { default := Phenomena.Verum.Studies.MartinezVera2026.instInhabitedMiAnalysis.default }

def Phenomena.Verum.Studies.MartinezVera2026.instInhabitedMiAnalysis.default : MiAnalysis

Equations

• Phenomena.Verum.Studies.MartinezVera2026.instInhabitedMiAnalysis.default = Phenomena.Verum.Studies.MartinezVera2026.MiAnalysis.verumPlusFocus

def Phenomena.Verum.Studies.MartinezVera2026.quechuanMiAnalyses : List (String × MiAnalysis)

The cross-Quechuan map from variety to published =mi analysis.

Equations

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

theorem Phenomena.Verum.Studies.MartinezVera2026.quechuanMiAnalyses_pairwise_distinct : List.Pairwise (fun (x1 x2 : MiAnalysis) => x1 ≠ x2) [MiAnalysis.verumPlusFocus, MiAnalysis.verumPlusContrast, MiAnalysis.directEvidentialOnly, MiAnalysis.pureEvidentialNoFocus, MiAnalysis.epistemicAuthority]

The five published analyses are pairwise distinct as labels. Drift sentry: collapsing two cases breaks this.