Documentation

Linglib.Phenomena.TenseAspect.Studies.Cumming2026

@cite{cumming-2026} Verification Theorems #

@cite{cumming-2026}

Verification theorems for the cross-linguistic nonfuture downstream generalization from @cite{cumming-2026}. 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
source
def Phenomena.TenseAspect.Studies.Cumming2026.allParadigms :
List Semantics.Tense.Evidential.TAMEEntry

All paradigm entries across the three languages.

Equations
Instances For
    source
    def Phenomena.TenseAspect.Studies.Cumming2026.nonfutureParadigms :
    List Semantics.Tense.Evidential.TAMEEntry

    Nonfuture paradigm entries (across all languages).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Phenomena.TenseAspect.Studies.Cumming2026.futureParadigms :
      List Semantics.Tense.Evidential.TAMEEntry

      Future paradigm entries (across all languages).

      Equations
      Instances For
        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.simplePast_nonfuture :
        Fragments.English.Tense.simplePast.isNonfuture = true

        English simple past is nonfuture (EP = downstream).

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.presentProg_nonfuture :
        Fragments.English.Tense.presentProg.isNonfuture = true

        English present progressive is nonfuture (EP = downstream).

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.tePast_nonfuture :
        Fragments.Korean.Evidentials.tePast.isNonfuture = true

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

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.tePresent_nonfuture :
        Fragments.Korean.Evidentials.tePresent.isNonfuture = true

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

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.neyPast_nonfuture :
        Fragments.Korean.Evidentials.neyPast.isNonfuture = true

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

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.neyPresent_nonfuture :
        Fragments.Korean.Evidentials.neyPresent.isNonfuture = true

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

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.nfutL_nonfuture :
        Fragments.Bulgarian.Evidentials.nfutL.isNonfuture = true

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

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.nonfuture_downstream (p : Semantics.Tense.Evidential.TAMEEntry) (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) (h_nf : p.isNonfuture = true) (h_ep : p.epConstraint f) :
        Semantics.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.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.simplePast_downstream (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) :
        Fragments.English.Tense.simplePast.epConstraint f → Semantics.Tense.Evidential.downstreamEvidence f

        English simple past EP entails downstream evidence.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.presentProg_downstream (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) :
        Fragments.English.Tense.presentProg.epConstraint f → Semantics.Tense.Evidential.downstreamEvidence f

        English present progressive EP entails downstream evidence.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.tePast_downstream (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) :
        Fragments.Korean.Evidentials.tePast.epConstraint f → Semantics.Tense.Evidential.downstreamEvidence f

        Korean -te PAST EP entails downstream evidence.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.tePresent_downstream (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) :
        Fragments.Korean.Evidentials.tePresent.epConstraint f → Semantics.Tense.Evidential.downstreamEvidence f

        Korean -te PRESENT EP entails downstream evidence.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.neyPast_downstream (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) :
        Fragments.Korean.Evidentials.neyPast.epConstraint f → Semantics.Tense.Evidential.downstreamEvidence f

        Korean -ney PAST EP entails downstream evidence.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.neyPresent_downstream (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) :
        Fragments.Korean.Evidentials.neyPresent.epConstraint f → Semantics.Tense.Evidential.downstreamEvidence f

        Korean -ney PRESENT EP entails downstream evidence.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.nfutL_downstream (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) :
        Fragments.Bulgarian.Evidentials.nfutL.epConstraint f → Semantics.Tense.Evidential.downstreamEvidence f

        Bulgarian NFUT + -l EP entails downstream evidence.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.future_no_downstream :
        Fragments.English.Tense.future.epConstraint { speechTime := 10, perspectiveTime := 10, referenceTime := 0, eventTime := 5, acquisitionTime := 0 } ∧ ¬Semantics.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.

        source
        theorem Phenomena.TenseAspect.Studies.Cumming2026.korean_te_ney_ep_diverge :
        (∃ (f : Semantics.Tense.Evidential.EvidentialFrame ℤ), Fragments.Korean.Evidentials.tePresent.upConstraint f ∧ ¬Fragments.Korean.Evidentials.neyPresent.upConstraint f) ∧ ∃ (f : Semantics.Tense.Evidential.EvidentialFrame ℤ), Fragments.Korean.Evidentials.neyPresent.upConstraint f ∧ ¬Fragments.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.