[Cum26] Verification Theorems

[Cum26]

Verification theorems for the cross-linguistic nonfuture downstream generalization from [Cum26]. Paradigm data lives in Fragment files; this file imports them and proves the empirical predictions.

Key Results

1. nonfuture_downstream: generic master theorem — any paradigm entry whose EP constraint is nonfuture entails T ≤ A (downstream evidence)
2. Per-entry corollaries: one-liner applications of the generic lemma
3. Per-entry isNonfuture verification: breaks if EP changed
4. future_no_downstream: future entries do not require downstream evidence
5. korean_te_ney_ep_diverge: EP and UP factorize independently in Korean

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

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

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

theorem Cumming2026.simplePast_nonfuture : English.Tense.simplePast.IsNonfuture

English simple past is nonfuture (EP = downstream).

theorem Cumming2026.presentProg_nonfuture : English.Tense.presentProg.IsNonfuture

English present progressive is nonfuture (EP = downstream).

theorem Cumming2026.tePast_nonfuture : Korean.Evidentials.tePast.IsNonfuture

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

theorem Cumming2026.tePresent_nonfuture : Korean.Evidentials.tePresent.IsNonfuture

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

theorem Cumming2026.neyPast_nonfuture : Korean.Evidentials.neyPast.IsNonfuture

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

theorem Cumming2026.neyPresent_nonfuture : Korean.Evidentials.neyPresent.IsNonfuture

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

theorem Cumming2026.nfutL_nonfuture : Bulgarian.Evidentials.nfutL.IsNonfuture

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

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

Generic nonfuture downstream: any paradigm entry whose EP constraint is nonfuture entails T ≤ A (downstream evidence). Delegates to EPCondition.nonfuture_implies_downstream.

theorem Cumming2026.simplePast_downstream (f : Tense.Evidential.EvidentialFrame ℤ) : English.Tense.simplePast.epConstraint f → Tense.Evidential.downstreamEvidence f

English simple past EP entails downstream evidence.

theorem Cumming2026.presentProg_downstream (f : Tense.Evidential.EvidentialFrame ℤ) : English.Tense.presentProg.epConstraint f → Tense.Evidential.downstreamEvidence f

English present progressive EP entails downstream evidence.

theorem Cumming2026.tePast_downstream (f : Tense.Evidential.EvidentialFrame ℤ) : Korean.Evidentials.tePast.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -te PAST EP entails downstream evidence.

theorem Cumming2026.tePresent_downstream (f : Tense.Evidential.EvidentialFrame ℤ) : Korean.Evidentials.tePresent.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -te PRESENT EP entails downstream evidence.

theorem Cumming2026.neyPast_downstream (f : Tense.Evidential.EvidentialFrame ℤ) : Korean.Evidentials.neyPast.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -ney PAST EP entails downstream evidence.

theorem Cumming2026.neyPresent_downstream (f : Tense.Evidential.EvidentialFrame ℤ) : Korean.Evidentials.neyPresent.epConstraint f → Tense.Evidential.downstreamEvidence f

Korean -ney PRESENT EP entails downstream evidence.

theorem Cumming2026.nfutL_downstream (f : Tense.Evidential.EvidentialFrame ℤ) : Bulgarian.Evidentials.nfutL.epConstraint f → Tense.Evidential.downstreamEvidence f

Bulgarian NFUT + -l EP entails downstream evidence.

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.

theorem Cumming2026.korean_te_ney_ep_diverge : (∃ (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

Korean -te and -ney EP diverge on the same tense: for present tense, -te requires T = A (contemporaneous evidence) while -ney requires T = A ∧ T = S (contemporaneous + speech-time present). The UP constraints differ: -te has T < S, -ney has T = S. This shows EP and UP factorize independently in the morphology.

[Cum26]'s tense evidential constraint and [vFG10]'s kernel semantics for epistemic must reflect the same underlying requirement: the speaker's evidence is indirect — causally downstream of the target event but not directly settling it.

| Cumming (tense)                   | VF&G (modals)                       |
|-----------------------------------|-------------------------------------|
| T ≤ A (downstream evidence)       | K doesn't settle φ                  |
| Nonfuture → downstream required   | must → indirectness presupposition  |
| Future → no constraint            | Bare assertion → no presupposition  |
| Direct observation → bare past ok | Direct evidence → must infelicitous |

The dripping-raincoat scenario ([zheng-2025], used in
`Modality/Kernel.lean`) provides a concrete bridge: the raincoat
evidence is causally downstream of rain (T ≤ A), and the kernel
{wearingRaincoat} doesn't settle isRaining. 

@[reducible, inline]

abbrev Cumming2026.World : Type

Equations

• Cumming2026.World = Fin 4

def Cumming2026.allWorlds : List World

Equations

• Cumming2026.allWorlds = [0, 1, 2, 3]

The kernel defs in Modality/Kernel.lean are private. We redefine equivalent propositions over World4 for the bridge. World interpretation: w0 = raining, w1 = sprinkler (wet but not rain), w2 = dry, w3 = unknown.

def Cumming2026.wearingRaincoat : World → Prop

Wearing a raincoat: true in w0 (rain) and w1 (sprinkler).

Equations

• Cumming2026.wearingRaincoat 0 = True
• Cumming2026.wearingRaincoat 1 = True
• Cumming2026.wearingRaincoat x✝ = False

@[implicit_reducible]

instance Cumming2026.instDecidablePredWorldWearingRaincoat : DecidablePred wearingRaincoat

Equations

• Cumming2026.instDecidablePredWorldWearingRaincoat 0 = isTrue Cumming2026.instDecidablePredWorldWearingRaincoat._proof_1
• Cumming2026.instDecidablePredWorldWearingRaincoat 1 = isTrue Cumming2026.instDecidablePredWorldWearingRaincoat._proof_2
• Cumming2026.instDecidablePredWorldWearingRaincoat 2 = isFalse Cumming2026.instDecidablePredWorldWearingRaincoat._proof_3
• Cumming2026.instDecidablePredWorldWearingRaincoat 3 = isFalse Cumming2026.instDecidablePredWorldWearingRaincoat._proof_4

def Cumming2026.isRaining : World → Prop

It is raining: true only in w0.

Equations

• Cumming2026.isRaining 0 = True
• Cumming2026.isRaining x✝ = False

@[implicit_reducible]

instance Cumming2026.instDecidablePredWorldIsRaining : DecidablePred isRaining

Equations

• Cumming2026.instDecidablePredWorldIsRaining 0 = isTrue Cumming2026.instDecidablePredWorldIsRaining._proof_1
• Cumming2026.instDecidablePredWorldIsRaining 1 = isFalse Cumming2026.instDecidablePredWorldIsRaining._proof_2
• Cumming2026.instDecidablePredWorldIsRaining 2 = isFalse Cumming2026.instDecidablePredWorldIsRaining._proof_3
• Cumming2026.instDecidablePredWorldIsRaining 3 = isFalse Cumming2026.instDecidablePredWorldIsRaining._proof_4

def Cumming2026.raincoatK : Semantics.Modality.Kernel World

The raincoat kernel: K = {wearingRaincoat}.

Equations

• Cumming2026.raincoatK = { props := [Cumming2026.wearingRaincoat] }

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 }

theorem Cumming2026.raincoat_downstream : Tense.Evidential.downstreamEvidence raincoatFrame

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

theorem Cumming2026.raincoat_not_settled : ¬Semantics.Modality.directlySettlesExplicit raincoatK isRaining

The raincoat kernel doesn't settle isRaining: K = {wearingRaincoat}, and wearingRaincoat neither entails nor excludes isRaining.

theorem Cumming2026.downstream_implies_must_defined : Tense.Evidential.downstreamEvidence raincoatFrame ∧ (Semantics.Modality.kernelMust raincoatK isRaining).presup 0

Downstream implies must-defined: in the raincoat scenario, downstream evidence (T ≤ A) co-occurs with the kernel not settling the prejacent.

theorem Cumming2026.tense_modal_evidential_parallel : Tense.Evidential.downstreamEvidence raincoatFrame ∧ (Semantics.Modality.kernelMust raincoatK isRaining).presup 0 ∧ ¬(Semantics.Modality.kernelMust raincoatK isRaining).assertion 0

Tense-modal evidential parallel: 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 doesn't settle isRaining.

theorem Cumming2026.direct_evidence_blocks_both : have directK := { props := [isRaining] }; Semantics.Modality.directlySettlesExplicit directK isRaining ∧ ¬(Semantics.Modality.kernelMust directK isRaining).presup 0 ∧ have directFrame := { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := -1, acquisitionTime := -1 }; Tense.Evidential.downstreamEvidence directFrame

Direct evidence blocks both: when evidence is direct, the kernel settles the prejacent → kernelMust is undefined and downstream is trivially satisfied (T = A). Speaker uses bare assertion, not must.

theorem Cumming2026.strong_assertion_settles : Semantics.Epistemicity.strongAssertion.source = Features.Evidentiality.CoarseSource.direct ∧ Semantics.Epistemicity.strongAssertion.authority = Semantics.Epistemicity.EpistemicAuthority.ego ∧ have directK := { props := [isRaining] }; Semantics.Modality.directlySettlesExplicit directK 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.

theorem Cumming2026.inferential_claim_must_profile : Semantics.Epistemicity.inferentialClaim.source = Features.Evidentiality.CoarseSource.inference ∧ Semantics.Epistemicity.inferentialClaim.authority = Semantics.Epistemicity.EpistemicAuthority.nonparticipant ∧ ¬Semantics.Modality.directlySettlesExplicit raincoatK isRaining ∧ (Semantics.Modality.kernelMust raincoatK isRaining).presup 0

Inferential claims (nonparticipant + inference) correspond to non-settling kernels with must-defined presuppositions — the canonical 'must' profile.

theorem Cumming2026.authority_source_correlation : Semantics.Epistemicity.strongAssertion.authority = Semantics.Epistemicity.EpistemicAuthority.ego ∧ Semantics.Epistemicity.strongAssertion.source = Features.Evidentiality.CoarseSource.direct ∧ Semantics.Epistemicity.inferentialClaim.authority = Semantics.Epistemicity.EpistemicAuthority.nonparticipant ∧ Semantics.Epistemicity.inferentialClaim.source = Features.Evidentiality.CoarseSource.inference

Ego↔direct and nonparticipant↔indirect form natural pairs. Epistemic authority and evidential source are orthogonal dimensions that correlate but don't reduce.