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

[MV26] [MV24] [MVC25] [Fal02] [Fal19] [Mur14] [Mur17] [Tel14] [Grz20] [Ben23] [San10] [HH17] [Col82] [RvG10] [RF15] [STBR10] [Kri14] [Roo85] [Roo92] [Hir17] [Hoh92] [RH04] [EK98] [Mat21] [Mat04] [BM15] [GHM20] [Goo22a] [Roc18]

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 ([Roc18], [Hir17]).

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 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 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 (CommonGround-modal verum operator) split visible at the type level.

Substrate consumed

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

Methodological note

The paper's data is original fieldwork with six Saraguro speakers, following [Mat04], [BM15]. 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.

§ 0. Evidential illocutionary operators (Faller / Murray)

Substrate previously hosted at Discourse/EvidentialIllocution.lean, inlined here per anchoring rule (sole consumer is this study file). The assert/present distinction is [Fal02] / [Mur14]; the raisedPropositions projection drives [MV26]'s salience updates downstream.

structure MartinezVera2026.EvidentialAct (W : Type u_2) : Type u_2

Result of applying an illocutionary operator: speaker, addressee, scope proposition, evidential (not-at-issue) proposition, and commits-to-scope flag (true for assert, false for present).

• speaker : Discourse.DiscourseRole
• addressee : Discourse.DiscourseRole
• scope : Set W
• evidentialContent : Set W
• commitsToScope : Bool

def MartinezVera2026.assert {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : EvidentialAct W

[Fal02]/[Fal19]: assert(⟨A, N⟩) commits the speaker to both A and N. Used with direct evidentials.

Equations

• MartinezVera2026.assert s a β = { speaker := s, addressee := a, scope := {w : W | β.atIssue w}, evidentialContent := {w : W | β.notAtIssue w}, commitsToScope := true }

def MartinezVera2026.present {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : EvidentialAct W

[Mur14]/[Fal19]: present(⟨A, N⟩) brings A to attention but does NOT commit to A; commits only to N. Used with reportative/inferential evidentials.

Equations

• MartinezVera2026.present s a β = { speaker := s, addressee := a, scope := {w : W | β.atIssue w}, evidentialContent := {w : W | β.notAtIssue w}, commitsToScope := false }

@[simp]

theorem MartinezVera2026.assert_commitsToScope {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : (assert s a β).commitsToScope = true

@[simp]

theorem MartinezVera2026.present_commitsToScope {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : (present s a β).commitsToScope = false

theorem MartinezVera2026.assert_present_differ_only_in_scope_commitment {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : (assert s a β).scope = (present s a β).scope ∧ (assert s a β).evidentialContent = (present s a β).evidentialContent ∧ (assert s a β).commitsToScope ≠ (present s a β).commitsToScope

def MartinezVera2026.EvidentialAct.raisedPropositions {W : Type u_1} (a : EvidentialAct W) : Set (Set W)

Propositions an act puts forward to the addressee. assert raises the scope; present raises both scope and its complement (the open polar issue).

Equations

• a.raisedPropositions = if a.commitsToScope = true then {a.scope} else {a.scope, a.scopeᶜ}

@[simp]

theorem MartinezVera2026.assert_raisedPropositions {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : (assert s a β).raisedPropositions = {{w : W | β.atIssue w}}

@[simp]

theorem MartinezVera2026.present_raisedPropositions {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : (present s a β).raisedPropositions = {{w : W | β.atIssue w}, {w : W | β.atIssue w}ᶜ}

theorem MartinezVera2026.present_raises_polar_negation {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : {w : W | β.atIssue w}ᶜ ∈ (present s a β).raisedPropositions

theorem MartinezVera2026.assert_does_not_raise_polar_negation {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) (hne : ∃ (w : W), β.atIssue w) : {w : W | β.atIssue w}ᶜ ∉ (assert s a β).raisedPropositions

inductive MartinezVera2026.IllocutionaryFlavour : Type

Typological mapping from evidential source to illocutionary operator flavour.

• assertFlavour : IllocutionaryFlavour
• presentFlavour : IllocutionaryFlavour

@[implicit_reducible]

instance MartinezVera2026.instDecidableEqIllocutionaryFlavour : DecidableEq IllocutionaryFlavour

Equations

• MartinezVera2026.instDecidableEqIllocutionaryFlavour x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MartinezVera2026.instReprIllocutionaryFlavour.repr : IllocutionaryFlavour → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MartinezVera2026.instReprIllocutionaryFlavour : Repr IllocutionaryFlavour

Equations

• MartinezVera2026.instReprIllocutionaryFlavour = { reprPrec := MartinezVera2026.instReprIllocutionaryFlavour.repr }

@[implicit_reducible]

instance MartinezVera2026.instInhabitedIllocutionaryFlavour : Inhabited IllocutionaryFlavour

Equations

• MartinezVera2026.instInhabitedIllocutionaryFlavour = { default := MartinezVera2026.instInhabitedIllocutionaryFlavour.default }

def MartinezVera2026.IllocutionaryFlavour.ofCoarseSource : Features.Evidentiality.CoarseSource → IllocutionaryFlavour

Equations

• MartinezVera2026.IllocutionaryFlavour.ofCoarseSource Features.Evidentiality.CoarseSource.direct = MartinezVera2026.IllocutionaryFlavour.assertFlavour
• MartinezVera2026.IllocutionaryFlavour.ofCoarseSource Features.Evidentiality.CoarseSource.hearsay = MartinezVera2026.IllocutionaryFlavour.presentFlavour
• MartinezVera2026.IllocutionaryFlavour.ofCoarseSource Features.Evidentiality.CoarseSource.inference = MartinezVera2026.IllocutionaryFlavour.presentFlavour

@[simp]

theorem MartinezVera2026.flavour_direct : IllocutionaryFlavour.ofCoarseSource Features.Evidentiality.CoarseSource.direct = IllocutionaryFlavour.assertFlavour

@[simp]

theorem MartinezVera2026.flavour_hearsay : IllocutionaryFlavour.ofCoarseSource Features.Evidentiality.CoarseSource.hearsay = IllocutionaryFlavour.presentFlavour

@[simp]

theorem MartinezVera2026.flavour_inference : IllocutionaryFlavour.ofCoarseSource Features.Evidentiality.CoarseSource.inference = IllocutionaryFlavour.presentFlavour

def MartinezVera2026.applyDefault {W : Type u_1} (src : Features.Evidentiality.CoarseSource) (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : EvidentialAct W

Equations

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

@[simp]

theorem MartinezVera2026.applyDefault_direct {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : applyDefault Features.Evidentiality.CoarseSource.direct s a β = assert s a β

@[simp]

theorem MartinezVera2026.applyDefault_hearsay {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : applyDefault Features.Evidentiality.CoarseSource.hearsay s a β = present s a β

@[simp]

theorem MartinezVera2026.applyDefault_inference {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : applyDefault Features.Evidentiality.CoarseSource.inference s a β = present s a β

theorem MartinezVera2026.direct_commits_indirect_does_not {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : (applyDefault Features.Evidentiality.CoarseSource.direct s a β).commitsToScope = true ∧ (applyDefault Features.Evidentiality.CoarseSource.hearsay s a β).commitsToScope = false ∧ (applyDefault Features.Evidentiality.CoarseSource.inference s a β).commitsToScope = false

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

def MartinezVera2026.miFelicitous {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (alts : Set (Set W)) (S : Semantics.ContentLayer.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 Semantics/Exhaustification.Excluder machinery.

Equations

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

§ 2. The polar QUD setup

def 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 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

• MartinezVera2026.polarQUD p = { salient := ∅, qud := Question.polar p }

theorem MartinezVera2026.mem_alt_polar {W : Type u_1} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : p ∈ (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 Question.alt_polar_of_nontrivial.

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

theorem 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 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 MartinezVera2026.updateAfterAct {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (a : 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

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

@[simp]

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

@[simp]

theorem MartinezVera2026.qud_updateAfterAct {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (a : 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 MartinezVera2026.mi_felicitous_after_present {W : Type u_1} (s a : Discourse.DiscourseRole) (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : miFelicitous (updateAfterAct (polarQUD p) (present s a (Semantics.ContentLayer.BiLayered.ofProp fun (x : W) => x ∈ p))) {p, pᶜ} (Semantics.ContentLayer.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 MartinezVera2026.mi_infelicitous_after_assert {W : Type u_1} (s a : Discourse.DiscourseRole) (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : ¬miFelicitous (updateAfterAct (polarQUD p) (assert s a (Semantics.ContentLayer.BiLayered.ofProp fun (x : W) => x ∈ p))) {p, pᶜ} (Semantics.ContentLayer.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 [RH04]'s CommonGround-modal verum surfaces as the partition divergence in §6 below.

theorem MartinezVera2026.mi_polar_iff_verumFelicitous {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.ContentLayer.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 MartinezVera2026.miAsVerumOperatorPolar {W : Type u_1} : Hohle1992.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 MartinezVera2026.miAsVerumOperatorPolar_apply {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.ContentLayer.BiLayered W) : miAsVerumOperatorPolar.felicitous c β = miFelicitous c {{w : W | β.atIssue w}, {w : W | β.atIssue w}ᶜ} β

theorem MartinezVera2026.mi_eq_hohle_as_verumOperator {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (β : Semantics.ContentLayer.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.

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

Romero & Han 2004 analyse verum as a CommonGround-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 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 MartinezVera2026.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 MartinezVera2026.direct_commits_reportative_does_not {W : Type u_1} (s a : Discourse.DiscourseRole) (β : Semantics.ContentLayer.BiLayered W) : (assert s a β).commitsToScope = true ∧ (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 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 [MV26]).

• verumPlusContrast : MiAnalysis

  Verum + corrective contrast (Conchucos Quechua per [Ben23]).

• directEvidentialOnly : MiAnalysis

  Pure (best-possible-grounds) direct evidential (Cuzco Quechua per [Fal02], [San10]).

• pureEvidentialNoFocus : MiAnalysis

  Pure evidential, no focus role (Imbabura Kichwa per [Tel14]).

• epistemicAuthority : MiAnalysis

  Epistemic-authority marker (Upper Napo Kichwa per [Grz20]).

@[implicit_reducible]

instance MartinezVera2026.instDecidableEqMiAnalysis : DecidableEq MiAnalysis

Equations

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

def MartinezVera2026.instReprMiAnalysis.repr : MiAnalysis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MartinezVera2026.instReprMiAnalysis : Repr MiAnalysis

Equations

• MartinezVera2026.instReprMiAnalysis = { reprPrec := MartinezVera2026.instReprMiAnalysis.repr }

@[implicit_reducible]

instance MartinezVera2026.instInhabitedMiAnalysis : Inhabited MiAnalysis

Equations

• MartinezVera2026.instInhabitedMiAnalysis = { default := MartinezVera2026.instInhabitedMiAnalysis.default }

def 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 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.