Cumming (2026): Tense and evidence — verification theorems #

[Cum26]

Verification theorems for the cross-linguistic nonfuture-downstream generalization of [Cum26]. Paradigm data (the paper's tables (17)–(20) and (22)) lives in the Fragment files; this file imports them and proves the empirical predictions.

Main results #

nonfuture_downstream: any paradigm entry whose EP constraint is nonfuture entails T ≤ A (downstream evidence), with per-entry verification anchors and corollaries
future_no_downstream: future entries impose no downstream requirement
korean_te_ney_up_diverge: -te and -ney present share one EP constraint but differ in UP — EP and UP factorize independently in the morphology
tense_modal_evidential_parallel: the tense constraint and [vFG10]'s kernelMust presupposition hold jointly in the [Zhe25] raincoat scenario

Cross-linguistic collection #

source

def Cumming2026.allParadigms :

List Tense.Evidential.TAMEEntry

All paradigm entries across the three languages.

Equations

Cumming2026.allParadigms = English.Tense.allEntries ++ Korean.Evidentials.allEntries ++ Bulgarian.Evidentials.allEntries

Instances For

source

def Cumming2026.nonfutureParadigms :

List Tense.Evidential.TAMEEntry

Nonfuture paradigm entries (across all languages).

Equations

Cumming2026.nonfutureParadigms = List.filter (fun (x : Tense.Evidential.TAMEEntry) => decide x.IsNonfuture) Cumming2026.allParadigms

Instances For

source

def Cumming2026.futureParadigms :

List Tense.Evidential.TAMEEntry

Future paradigm entries (across all languages).

Equations

Cumming2026.futureParadigms = List.filter (fun (x : Tense.Evidential.TAMEEntry) => decide ¬x.IsNonfuture) Cumming2026.allParadigms

Instances For

Per-entry nonfuture verification #

source

theorem Cumming2026.simplePast_nonfuture :

English.Tense.simplePast.IsNonfuture

English simple past is nonfuture (EP = downstream).

source

theorem Cumming2026.presentProg_nonfuture :

English.Tense.presentProg.IsNonfuture

English present progressive is nonfuture (EP = downstream).

source

theorem Cumming2026.tePast_nonfuture :

Korean.Evidentials.tePast.IsNonfuture

Korean -te PAST is nonfuture (EP = strictDownstream).

source

theorem Cumming2026.tePresent_nonfuture :

Korean.Evidentials.tePresent.IsNonfuture

Korean -te PRESENT is nonfuture (EP = contemporaneous).

source

theorem Cumming2026.neyPast_nonfuture :

Korean.Evidentials.neyPast.IsNonfuture

Korean -ney PAST is nonfuture (EP = strictDownstream).

source

theorem Cumming2026.neyPresent_nonfuture :

Korean.Evidentials.neyPresent.IsNonfuture

Korean -ney PRESENT is nonfuture (EP = contemporaneous).

source

theorem Cumming2026.nfutL_nonfuture :

Bulgarian.Evidentials.nfutL.IsNonfuture

Bulgarian NFUT + -l is nonfuture (EP = downstream).

Master downstream theorem #

source

theorem Cumming2026.nonfuture_downstream (p : Tense.Evidential.TAMEEntry) (f : Tense.Evidential.EvidentialFrame ℤ) (h_nf : p.IsNonfuture) (h_ep : p.epConstraint f) :

Tense.Evidential.downstreamEvidence f

Any paradigm entry whose EP constraint is nonfuture entails T ≤ A (downstream evidence).

Per-entry downstream corollaries #

source

theorem Cumming2026.simplePast_downstream (f : Tense.Evidential.EvidentialFrame ℤ) :

English.Tense.simplePast.epConstraint f → Tense.Evidential.downstreamEvidence f

English simple past EP entails downstream evidence.

source

theorem Cumming2026.presentProg_downstream (f : Tense.Evidential.EvidentialFrame ℤ) :

English.Tense.presentProg.epConstraint f → Tense.Evidential.downstreamEvidence f

English present progressive EP entails downstream evidence.

source

theorem Cumming2026.tePast_downstream (f : Tense.Evidential.EvidentialFrame ℤ) :

Korean.Evidentials.tePast.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -te PAST EP entails downstream evidence.

source

theorem Cumming2026.tePresent_downstream (f : Tense.Evidential.EvidentialFrame ℤ) :

Korean.Evidentials.tePresent.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -te PRESENT EP entails downstream evidence.

source

theorem Cumming2026.neyPast_downstream (f : Tense.Evidential.EvidentialFrame ℤ) :

Korean.Evidentials.neyPast.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -ney PAST EP entails downstream evidence.

source

theorem Cumming2026.neyPresent_downstream (f : Tense.Evidential.EvidentialFrame ℤ) :

Korean.Evidentials.neyPresent.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -ney PRESENT EP entails downstream evidence.

source

theorem Cumming2026.nfutL_downstream (f : Tense.Evidential.EvidentialFrame ℤ) :

Bulgarian.Evidentials.nfutL.epConstraint f → Tense.Evidential.downstreamEvidence f

Bulgarian NFUT + -l EP entails downstream evidence.

Future counterexample #

source

theorem Cumming2026.future_no_downstream :

English.Tense.future.epConstraint { speechTime := 10, perspectiveTime := 10, referenceTime := 0, eventTime := 5, acquisitionTime := 0 } ∧ ¬Tense.Evidential.downstreamEvidence { speechTime := 10, perspectiveTime := 10, referenceTime := 0, eventTime := 5, acquisitionTime := 0 }

Future entries do not require downstream evidence: the EP constraint is either trivially true (English bare future) or imposes A < T (prospective), which is the opposite of T ≤ A.

Korean EP/UP factorization #

source

theorem Cumming2026.korean_te_ney_up_diverge :

Korean.Evidentials.tePresent.ep = Korean.Evidentials.neyPresent.ep ∧ (∃ (f : Tense.Evidential.EvidentialFrame ℤ), Korean.Evidentials.tePresent.upConstraint f ∧ ¬Korean.Evidentials.neyPresent.upConstraint f) ∧ ∃ (f : Tense.Evidential.EvidentialFrame ℤ), Korean.Evidentials.neyPresent.upConstraint f ∧ ¬Korean.Evidentials.tePresent.upConstraint f

The two present-tense evidentials impose the same EP constraint (T = A) but different UP constraints (-te: T < S; -ney: T = S), witnessed in both directions: EP and UP vary independently in the morphology ([Cum26], tables (18)–(19)).

[Cum26] observes that the "fake future" will-forms closely resemble epistemic must: both require the prejacent to follow from the evidence rather than being directly observed. The [vFG10] kernel semantics states the modal side as a presupposition that the kernel does not directly settle the prejacent; the tense side is the nonfuture downstream constraint (T ≤ A). The [Zhe25] dripping-raincoat scenario (from Studies/Zheng2025.lean) witnesses both at once: the raincoat evidence is causally downstream of the rain, and the kernel {wearingRaincoat} does not settle isRaining.

source

def Cumming2026.raincoatFrame :

Tense.Evidential.EvidentialFrame ℤ

A concrete evidential frame for the raincoat scenario: S = 0 (speech time now), T = -2 (rain event in the past), R = 0, A = -1 (evidence acquired between event and speech).

Equations

Cumming2026.raincoatFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := -2, acquisitionTime := -1 }

Instances For

source

theorem Cumming2026.raincoat_downstream :

Tense.Evidential.downstreamEvidence raincoatFrame

The raincoat evidence is downstream: T ≤ A (-2 ≤ -1).

source

theorem Cumming2026.raincoat_not_settled :

¬Zheng2025.raincoatK.directlySettles Zheng2025.isRaining

The raincoat kernel doesn't settle isRaining — the third conjunct of [Zhe25]'s nandao-felicity theorem.

source

theorem Cumming2026.downstream_implies_must_defined :

Tense.Evidential.downstreamEvidence raincoatFrame ∧ (Modality.kernelMust Zheng2025.raincoatK Zheng2025.isRaining).presup Zheng2025.World.rain

In the raincoat scenario, downstream evidence (T ≤ A) co-occurs with the kernel not settling the prejacent.

source

theorem Cumming2026.tense_modal_evidential_parallel :

Tense.Evidential.downstreamEvidence raincoatFrame ∧ (Modality.kernelMust Zheng2025.raincoatK Zheng2025.isRaining).presup Zheng2025.World.rain ∧ ¬(Modality.kernelMust Zheng2025.raincoatK Zheng2025.isRaining).assertion Zheng2025.World.rain

Both Cumming's nonfuture constraint and VF&G's kernelMust presupposition hold simultaneously for the same scenario: the raincoat evidence is downstream (T ≤ A) and the kernel does not settle isRaining.

source

theorem Cumming2026.direct_evidence_blocks_both :

have directK := { props := [Zheng2025.isRaining] }; directK.directlySettles Zheng2025.isRaining ∧ ¬(Modality.kernelMust directK Zheng2025.isRaining).presup Zheng2025.World.rain ∧ have directFrame := { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := -1, acquisitionTime := -1 }; Tense.Evidential.downstreamEvidence directFrame

When evidence is direct, the kernel settles the prejacent — kernelMust is undefined — and downstream is trivially satisfied (T = A); the speaker uses bare assertion, not must.

Epistemic authority bridge #

source

theorem Cumming2026.strong_assertion_settles :

Semantics.Epistemicity.strongAssertion.source = Semantics.Evidential.CoarseSource.direct ∧ Semantics.Epistemicity.strongAssertion.authority = Semantics.Epistemicity.EpistemicAuthority.ego ∧ have directK := { props := [Zheng2025.isRaining] }; directK.directlySettles Zheng2025.isRaining

Strong assertions (ego + direct) correspond to settling kernels. When the speaker has privileged access AND direct evidence, the kernel settles the prejacent — 'must' is infelicitous, bare assertion is used.

source

theorem Cumming2026.inferential_claim_must_profile :