@cite{klecha-2016}: Modality and Embedded Temporal Operators

Klecha's central result: the temporal orientation of embedded clauses under attitude verbs is determined by the modal base pronoun (DOX vs. CIR), not by the modal or attitude verb per se.

Empirical puzzle

Under past-tense think (doxastic), embedded tense cannot be future-oriented:

• "Martina thought Carissa got pregnant" → RT ≤ thinking time

Under past-tense hope (preferential / CIR-compatible), embedded tense can be future-oriented:

• "Martina hoped Carissa got pregnant" → RT > hoping time (CIR reading)

Theoretical mechanism

1. DOX returns actual histories ending at the eval time → RT ≤ EvalT (Upper Limit Constraint derived from DOX's temporal character)
2. CIR returns future histories departing from the eval time → RT > EvalT (future orientation permitted)
3. Embedded tense (PAST or NPST) composes with the modal base constraint. The intersection determines what temporal orientations are available: DOX ∧ PAST = past; DOX ∧ NPST = simultaneous; CIR ∧ NPST = future; CIR ∧ PAST = impossible.

What this file verifies

• Attitude verb classifications from Fragments.English derive the correct modal base compatibility
• think/believe are DOX-only (block future)
• hope/pray permit CIR (allow future)
• The Upper Limit Constraint follows from doxastic temporal character
• Hacquard's positional analysis is complementary: position determines WHAT time; modal base kind determines WHICH DIRECTION
• Table 1 modal-temporal correspondence via ModalFlavor.toModalBaseKind
• NPST is strictly weaker than present (key to the analysis)
• Hope ambiguity: DOX → past, CIR → future

theorem Klecha2016.think_is_doxastic : Fragments.English.Predicates.Verbal.think.attitude = some (Features.Attitude.doxastic Features.Veridicality.nonVeridical)

think is classified as doxastic → DOX only.

theorem Klecha2016.believe_is_doxastic : Fragments.English.Predicates.Verbal.believe.attitude = some (Features.Attitude.doxastic Features.Veridicality.nonVeridical)

believe is classified as doxastic → DOX only.

theorem Klecha2016.hope_is_preferential : Fragments.English.Predicates.Verbal.hope.attitude = some (Features.Attitude.preferential (Features.Preferential.degreeComparison Features.AttitudeValence.positive))

hope is classified as preferential → can take CIR.

theorem Klecha2016.pray_is_preferential : Fragments.English.Predicates.Verbal.pray.attitude = some (Features.Attitude.preferential (Features.Preferential.degreeComparison Features.AttitudeValence.positive))

pray is classified as preferential → can take CIR.

theorem Klecha2016.think_blocks_cir : ¬(Features.Attitude.doxastic Features.Veridicality.nonVeridical).PermitsCircumstantial

think's attitude blocks circumstantial modal base.

theorem Klecha2016.believe_blocks_cir : ¬(Features.Attitude.doxastic Features.Veridicality.nonVeridical).PermitsCircumstantial

believe's attitude blocks circumstantial modal base.

theorem Klecha2016.hope_permits_cir : (Features.Attitude.preferential (Features.Preferential.degreeComparison Features.AttitudeValence.positive)).PermitsCircumstantial

hope's attitude permits circumstantial modal base.

theorem Klecha2016.pray_permits_cir : (Features.Attitude.preferential (Features.Preferential.degreeComparison Features.AttitudeValence.positive)).PermitsCircumstantial

pray's attitude permits circumstantial modal base.

theorem Klecha2016.think_modal_base : Semantics.Modality.TemporalConstraint.Attitude.toModalBaseKind (Features.Attitude.doxastic Features.Veridicality.nonVeridical) = Core.Modality.ModalBaseKind.doxastic

think's derived modal base kind is doxastic.

theorem Klecha2016.hope_modal_base : Semantics.Modality.TemporalConstraint.Attitude.toModalBaseKind (Features.Attitude.preferential (Features.Preferential.degreeComparison Features.AttitudeValence.positive)) = Core.Modality.ModalBaseKind.circumstantial

hope's derived modal base kind is circumstantial.

"Martina thought Carissa got pregnant"

Under think (DOX), the embedded past tense is genuine past: RT < thinking time. Future-oriented readings are blocked.

theorem Klecha2016.thought_pregnant_past (thinkTime embRT : ℤ) (h : embRT < thinkTime) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic thinkTime embRT

Past reading under think is compatible.

theorem Klecha2016.thought_pregnant_no_future (thinkTime embRT : ℤ) (h : embRT > thinkTime) : ¬Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic thinkTime embRT

Future reading under think is blocked.

"Martina hoped Carissa got pregnant"

Under hope (CIR), the "past" morphology on "got" is SOT agreement — the embedded tense can be future-oriented: RT > hoping time.

But hope can also take DOX, giving a past-oriented reading: "Martina hoped Carissa got pregnant" → RT < hoping time (DOX).

theorem Klecha2016.hoped_pregnant_future (hopeTime embRT : ℤ) (h : embRT > hopeTime) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial hopeTime embRT

Future reading under hope is permitted (via CIR).

theorem Klecha2016.hoped_pregnant_past (hopeTime embRT : ℤ) (h : embRT < hopeTime) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic hopeTime embRT

Past reading under hope is also permitted (via DOX).

theorem Klecha2016.ulc_derived_from_dox (evalTime refTime : ℤ) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic evalTime refTime ↔ refTime ≤ evalTime

The ULC is not a stipulated constraint — it follows from DOX's temporal character. Any doxastic attitude verb imposes RT ≤ EvalT, blocking future orientation.

theorem Klecha2016.cir_is_future (evalTime refTime : ℤ) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial evalTime refTime ↔ refTime > evalTime

The CIR temporal constraint is the complement: RT > EvalT.

The §5 theorems prove ULC via Iff.rfl against attitudeTemporalConstraint's definition. The two theorems below show the same fact via the substrate path that @cite{klecha-2016} actually uses: actualHistoryBase membership (Definition 3vi + eq 35a) → constraint, by .2 projection.

This is what differentiates Klecha's ULC from @cite{abusch-1997}'s stipulated one — the upper limit is a kernel-checked consequence of DOX-pronoun's lexical entry, not a separately-asserted presupposition on T-nodes. The substrate derivation lives in Core.Modality.HistoricalAlternatives (actualHistoryBase_time_actual, futureHistoryBase_time_future); the attitudeTemporalConstraint projection in Theories/Semantics/Modality/TemporalConstraint.lean delegates to it.

theorem Klecha2016.ulc_via_history_base {W : Type u_1} (history : Core.Modality.HistoricalAlternatives.WorldHistory W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) (h : embedded ∈ Core.Modality.HistoricalAlternatives.actualHistoryBase history matrix) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic matrix.time embedded.time

ULC at ℤ via actualHistoryBase membership: any embedded situation in the matrix evaluation point's actual-history base satisfies the doxastic temporal constraint. The proof is Klecha's eq 35a derivation specialized to ℤ.

theorem Klecha2016.future_via_history_base {W : Type u_1} (history : Core.Modality.HistoricalAlternatives.WorldHistory W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) (h : embedded ∈ Core.Modality.HistoricalAlternatives.futureHistoryBase history matrix) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial matrix.time embedded.time

Future orientation at ℤ via futureHistoryBase membership: any embedded situation in the matrix evaluation point's future-history base satisfies the circumstantial temporal constraint. Klecha eq 35b specialized to ℤ.

@cite{klecha-2016} §4.2 last paragraph: "[my] approach to the Upper Limit Constraint is identical in spirit, if not in implementation, to @cite{abusch-1997}'s. Abusch relies on the exact same motivation [...] the future viewed as inherently unsettled and therefore unknowable."

The theorem below makes the predicate-level convergence kernel-checked: Klecha's attitudeTemporalConstraint .doxastic and Abusch's upperLimitConstraint are definitionally equal (modulo argument order). Both reduce to refTime ≤ evalTime. The proof is Iff.rfl.

The substantive content is in the proof routes, not in the proposition:

• Klecha route (kernel-checked in §5b): the predicate reaches ≤ via actualHistoryBase_time_actual : s' ∈ actualHistoryBase history s → s'.time ≤ s.time, a .2-projection through the situation-base definition. The doxastic-alternative quantification is carried by WorldHistory W Time membership.

• Abusch route (in Theories/Semantics/Tense/Basic.lean): the predicate is stated directly as abbrev upperLimitConstraint embeddedR matrixE := embeddedR ≤ matrixE. @cite{abusch-1997} §7 states ULC informally; @cite{heim-1994-comments} formalizes it as a presupposition on T-nodes, endorsed by Abusch 1997 fn 20. The value-level reduction here strips the modal-alternative quantification ("now of an epistemic alternative").

So the equivalence is strict at the value level. It is not strict at the modal-layer level: Klecha's substrate carries doxastic alternatives via WorldHistory; Abusch's bare-≤ form has dropped them. A modal-layer upperLimitConstraint over WorldHistory W Time matching Abusch's original "now of an epistemic alternative" is deferred.

theorem Klecha2016.klecha_dox_iff_abusch_ulc {Time : Type u_1} [LinearOrder Time] (evalTime refTime : Time) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic evalTime refTime ↔ Semantics.Tense.upperLimitConstraint refTime evalTime

Klecha's attitudeTemporalConstraint .doxastic and Abusch's upperLimitConstraint are definitionally equal predicates (modulo argument order). Both reduce to refTime ≤ evalTime.

@cite{klecha-2016} §4.2: "identical in spirit, if not in implementation, to @cite{abusch-1997}'s [ULC]." This theorem makes the implementation-level equality kernel-checked. The substantive spirit-level difference (derivation vs. stipulation) is recorded in §5b above and in the docstring.

The central compositional predictions. Each cell in the 2×2 matrix (DOX/CIR × PAST/NPST) has a determinate temporal orientation. These theorems instantiate the general results from ModalTense at ℤ.

theorem Klecha2016.dox_past_gives_past (t r : ℤ) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic t r ∧ Core.Time.Tense.GramTense.past.constrains r t ↔ r < t

DOX + PAST = past: "Martina thought Carissa got pregnant" (genuine past reading). RT < thinking time.

theorem Klecha2016.dox_npst_gives_simultaneous (t r : ℤ) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic t r ∧ Core.Time.Tense.GramTense.nonpast.constrains r t ↔ r = t

DOX + NPST = simultaneous: "Martina thought Carissa was pregnant" where "was" = SOT agreement over NPST. RT = thinking time.

theorem Klecha2016.cir_npst_gives_future (t r : ℤ) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial t r ∧ Core.Time.Tense.GramTense.nonpast.constrains r t ↔ r > t

CIR + NPST = future: "Martina hoped Carissa got pregnant" where "got" = SOT agreement over NPST + CIR. RT > hoping time.

theorem Klecha2016.cir_past_is_impossible (t r : ℤ) : ¬(Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial t r ∧ Core.Time.Tense.GramTense.past.constrains r t)

CIR + PAST = impossible: no RT can be both > t (CIR) and < t (PAST).

A key theoretical innovation: NPST (u ≤ t, i.e., ref ≥ perspective) is strictly weaker than present (ref = perspective). This matters because NPST includes future-oriented readings that present would exclude.

theorem Klecha2016.present_implies_nonpast (r p : ℤ) (h : Core.Time.Tense.GramTense.present.constrains r p) : Core.Time.Tense.GramTense.nonpast.constrains r p

Present entails nonpast: if ref = persp, then ref ≥ persp.

theorem Klecha2016.nonpast_strictly_weaker : ∃ (r : ℤ) (p : ℤ), Core.Time.Tense.GramTense.nonpast.constrains r p ∧ ¬Core.Time.Tense.GramTense.present.constrains r p

Nonpast does not entail present: there exist r, p where ref ≥ persp but ref ≠ persp (namely, any future time).

@cite{klecha-2016} Table 1 shows that epistemic modals ("She has to be home by now") are past/present-oriented, while circumstantial/deontic/bouletic modals ("She has to be home tomorrow") are future-oriented. This follows from ModalFlavor.toModalBaseKind.

theorem Klecha2016.epistemic_haveto_no_future : (Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.epistemic).permitsOrientation Core.Time.Tense.GramTense.future = false

Epistemic "have to" blocks future orientation.

theorem Klecha2016.circumstantial_haveto_future : (Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.circumstantial).permitsOrientation Core.Time.Tense.GramTense.future = true

Circumstantial "have to" permits future orientation.

theorem Klecha2016.deontic_haveto_future : (Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.deontic).permitsOrientation Core.Time.Tense.GramTense.future = true

Deontic "have to" permits future orientation.

theorem Klecha2016.bouletic_modal_future : (Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.bouletic).permitsOrientation Core.Time.Tense.GramTense.future = true

Bouletic modals permit future orientation.

theorem Klecha2016.non_epistemic_all_cir (f : Core.Modality.ModalFlavor) (h : f ≠ Core.Modality.ModalFlavor.epistemic) : Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind f = Core.Modality.ModalBaseKind.circumstantial

All non-epistemic flavors are CIR-like.

@cite{klecha-2016} (80): "*I told John that it rains tomorrow" is unacceptable — tell imposes an upper limit, patterning with doxastic verbs. Reportatives use DOX, blocking future orientation.

theorem Klecha2016.reportative_blocks_future (tellTime embRT : ℤ) (h : embRT > tellTime) : ¬Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic tellTime embRT

Reportatives (tell, say) impose the upper limit like doxastics: the future reading is blocked.

structure Klecha2016.AttitudeOrientationDatum : Type

Klecha's classification: attitude verbs and their temporal orientation predictions, derived from Attitude.permitsCircumstantial.

• verb : String
• isDoxOnly : Bool
• permitsULC : Bool
• permitsFuture : Bool

def Klecha2016.instReprAttitudeOrientationDatum.repr : AttitudeOrientationDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Klecha2016.instReprAttitudeOrientationDatum : Repr AttitudeOrientationDatum

Equations

• Klecha2016.instReprAttitudeOrientationDatum = { reprPrec := Klecha2016.instReprAttitudeOrientationDatum.repr }

def Klecha2016.instDecidableEqAttitudeOrientationDatum.decEq (x✝ x✝¹ : AttitudeOrientationDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Klecha2016.instDecidableEqAttitudeOrientationDatum : DecidableEq AttitudeOrientationDatum

Equations

• Klecha2016.instDecidableEqAttitudeOrientationDatum = Klecha2016.instDecidableEqAttitudeOrientationDatum.decEq

def Klecha2016.thinkDatum : AttitudeOrientationDatum

Equations

• Klecha2016.thinkDatum = { verb := "think", isDoxOnly := true, permitsULC := true, permitsFuture := false }

def Klecha2016.believeDatum : AttitudeOrientationDatum

Equations

• Klecha2016.believeDatum = { verb := "believe", isDoxOnly := true, permitsULC := true, permitsFuture := false }

def Klecha2016.hopeDatum : AttitudeOrientationDatum

Equations

• Klecha2016.hopeDatum = { verb := "hope", isDoxOnly := false, permitsULC := true, permitsFuture := true }

def Klecha2016.prayDatum : AttitudeOrientationDatum

Equations

• Klecha2016.prayDatum = { verb := "pray", isDoxOnly := false, permitsULC := true, permitsFuture := true }

def Klecha2016.classificationTable : List AttitudeOrientationDatum

Equations

• Klecha2016.classificationTable = [Klecha2016.thinkDatum, Klecha2016.believeDatum, Klecha2016.hopeDatum, Klecha2016.prayDatum]

theorem Klecha2016.dox_only_block_future : ((List.filter (fun (x : AttitudeOrientationDatum) => x.isDoxOnly) classificationTable).all fun (x : AttitudeOrientationDatum) => x.permitsFuture == false) = true

DOX-only verbs all block future orientation.

theorem Klecha2016.cir_compat_permit_future : ((List.filter (fun (x : AttitudeOrientationDatum) => !x.isDoxOnly) classificationTable).all fun (x : AttitudeOrientationDatum) => x.permitsFuture) = true

CIR-compatible verbs all permit future orientation.

Klecha's central universal — epistemic modals are DOX, and DOX strictly blocks future orientation (§ 8) — predicts that no language will have a felicitous "epistemic modal + future orientation" configuration. @cite{matthewson-2013}'s Gitksan data is the obvious test case: the variable-force epistemic imaa combines with the prospective marker dim to produce future-oriented epistemic claims (Fig. 4, ex. 42 and 44). The cross-framework outcome is refutation, not reconciliation: the two analyses return different Bool values for the (epistemic, future) cell, and there is no flavor-keyed ProspectiveMarkerPolicy that would unify them.

theorem Klecha2016.klecha_predicts_imaa_no_future : (Fragments.Gitksan.Modals.imaa.meaning.all fun (ff : Core.Modality.ForceFlavor) => decide ((Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind ff.flavor).permitsOrientation Core.Time.Tense.GramTense.future = false)) = true

Klecha's universal applied to imaa: the flavor on every meaning cell of imaa is epistemic, so the modal base is DOX, so future orientation is blocked.

theorem Klecha2016.matthewson_imaa_future_attested : List.filter (fun (c : Matthewson2013.Fig4Cell) => c.orientation == Core.Modality.TemporalOrientation.future) Matthewson2013.fig4Cells = [{ perspective := Core.Modality.TemporalPerspective.present, orientation := Core.Modality.TemporalOrientation.future, exampleNum := 42 }, { perspective := Core.Modality.TemporalPerspective.past, orientation := Core.Modality.TemporalOrientation.future, exampleNum := 44 }]

@cite{matthewson-2013} Fig. 4 records two future-orientation cells for imaa: TP=PRESENT × TO=FUTURE (ex. 42) and TP=PAST × TO=FUTURE (ex. 44). Both require dim. The empirical claim is that these configurations are felicitous, not blocked.

theorem Klecha2016.gitksan_imaa_refutes_universal : (Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.epistemic).permitsOrientation Core.Time.Tense.GramTense.future ≠ Fragments.Gitksan.Modals.requiresDim Fragments.Gitksan.Modals.imaa Core.Modality.TemporalOrientation.future

The disagreement: Klecha predicts no felicitous future-oriented imaa configurations exist; Matthewson reports two (Fig. 4 cells ex. 42 and 44). The two frameworks return different Bool values for the (epistemic, future) cell — the disagreement is concrete and source-grounded.

Architectural consequence

A unified Theories-level ProspectiveMarkerPolicy : ModalFlavor → TemporalOrientation → Bool would have to pick one of the two values for the (epistemic, future) cell:

• Klecha's value: false (DOX cannot extend forward).
• Matthewson's value: true (Gitksan imaa + dim is felicitous).

The picking is a cross-linguistic theoretical commitment, not a structural primitive. Until other modal-system Fragments (Korean -keyss, Mandarin huì, etc.) supply additional data points that agree with one analysis or the other, the per-Fragment requiresDim in Fragments/Gitksan/Modals.lean should stay where it is. Promoting it to Theories would silently impose Klecha's universal on languages whose data refutes it.

@cite{sharvit-2014} derives the simultaneous reading of past-under-past in English attitudes via SOT-deletion of a pronominal past (LexicalType.pronominal + english.hasSOT = true → english.simultaneousAttitudeReading = true in Studies/Sharvit2014.lean). @cite{klecha-2016} derives the same reading via DOX + NPST modal-base composition (dox_npst_iff below).

Different mechanisms, same value-level prediction: embeddedEventTime = matrixEvalTime. The bridge below witnesses both halves: (a) Sharvit's typology Bool prediction for English, (b) Klecha's value-level Iff.

theorem Klecha2016.sharvit_klecha_agree_simultaneous_english (sayingTime sickTime : ℤ) : Phenomena.TenseAspect.Studies.Sharvit2014.english.simultaneousAttitudeReading = true ∧ (Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic sayingTime sickTime ∧ Core.Time.Tense.GramTense.nonpast.constrains sickTime sayingTime ↔ sickTime = sayingTime)

Phase F bridge — Klecha-Sharvit agreement on the simultaneous reading for English. @cite{sharvit-2014}'s english.simultaneousAttitudeReading Bool fact and @cite{klecha-2016}'s dox_npst_iff value-level equivalence both witness the same prediction by different mechanisms (Sharvit: SOT-deletion of pronominal past; Klecha: DOX + NPST composition).

@cite{condoravdi-2002}'s metaphysical modal base (formalized in Core/Modality/HistoricalAlternatives.lean as metaphysicalBase) quantifies over historical alternatives at the eval time. @cite{klecha-2016}'s CIR modal base (futureHistoryBase) quantifies over future-history situations whose world-component lies in the same historical-alternatives equivalence class. The world-component of Klecha's CIR is therefore a subset of Condoravdi's metaphysical base.

Klecha §1.1 (PDF p. 7) explicitly identifies metaphysical as a "special case of the circumstantial modal base"; the present bridge makes the world-component subset relation kernel-checked.

theorem Klecha2016.klecha_cir_world_in_condoravdi_metaphysical {W : Type u_1} (history : Core.Modality.HistoricalAlternatives.WorldHistory W ℤ) (s s' : Core.WorldTimeIndex W ℤ) (h : s' ∈ Core.Modality.HistoricalAlternatives.futureHistoryBase history s) : s'.world ∈ Core.Modality.HistoricalAlternatives.metaphysicalBase history s.world s.time

Phase F bridge — Klecha-Condoravdi: the world-component of any situation in @cite{klecha-2016}'s CIR (futureHistoryBase) lies in @cite{condoravdi-2002}'s metaphysical modal base (metaphysicalBase). The proof is .1 projection through the situation-base + structural unfolding of metaphysicalBase / histEquiv.

theorem Klecha2016.klecha_dox_world_in_condoravdi_metaphysical {W : Type u_1} (history : Core.Modality.HistoricalAlternatives.WorldHistory W ℤ) (s s' : Core.WorldTimeIndex W ℤ) (h : s' ∈ Core.Modality.HistoricalAlternatives.actualHistoryBase history s) : s'.world ∈ Core.Modality.HistoricalAlternatives.metaphysicalBase history s.world s.time

Phase F bridge — Klecha-Condoravdi: the world-component of any situation in @cite{klecha-2016}'s DOX (actualHistoryBase) lies in @cite{condoravdi-2002}'s metaphysical modal base. The proof is .1 projection (same as the CIR case).

The 0.230.451 klecha_dox_iff_abusch_ulc (§5c above) was honest about being shallow: both sides reduce to ≤ at the value level, but the modal layer — quantification over doxastic alternatives that @cite{abusch-1997}'s prose statement requires — was stripped on both sides. With the new upperLimitConstraintModal substrate primitive (in Core/Modality/HistoricalAlternatives.lean, F4), the modal-layer bridge becomes statable.

@cite{abusch-1997}'s modal-layer ULC: an embedded situation lies in the actual-history base of the matrix situation (actualHistoryBase membership). @cite{klecha-2016}'s modal-layer derivation: attitudeTemporalConstraint_derived_doxastic shows the same membership produces the value-level constraint via .2 projection.

The bridge: both predicates ARE the same membership-in-base claim (Iff.rfl), but the predicates' separate names carry their respective paper attributions. The substantive content over §5c is that both sides now carry the modal-alternative quantification (via s'.world ∈ history s), not just the time-component projection.

theorem Klecha2016.klecha_dox_iff_abusch_ulc_modal {W : Type u_1} (history : Core.Modality.HistoricalAlternatives.WorldHistory W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) : embedded ∈ Core.Modality.HistoricalAlternatives.actualHistoryBase history matrix ↔ Core.Modality.HistoricalAlternatives.upperLimitConstraintModal history matrix embedded

Phase F bridge — Klecha ↔ Abusch ULC at the modal layer: @cite{klecha-2016}'s modal-layer doxastic predicate (membership in actualHistoryBase) and @cite{abusch-1997}'s modal-layer ULC (upperLimitConstraintModal) are the same membership claim. Both carry the doxastic-alternative quantification at the modal layer, in contrast to §5c's value-level klecha_dox_iff_abusch_ulc which strips it.

theorem Klecha2016.abusch_modal_ulc_implies_klecha_dox {W : Type u_1} (history : Core.Modality.HistoricalAlternatives.WorldHistory W ℤ) (matrix embedded : Core.WorldTimeIndex W ℤ) (h : Core.Modality.HistoricalAlternatives.upperLimitConstraintModal history matrix embedded) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic matrix.time embedded.time

Phase F bridge — modal-layer ULC implies value-level constraint: if @cite{abusch-1997}'s modal-layer ULC holds for (matrix, embedded), then @cite{klecha-2016}'s value-level attitudeTemporalConstraint .doxastic holds for the time components. Composes upperLimitConstraintModal_implies_value with the substrate's attitudeTemporalConstraint_derived_doxastic.

@cite{klecha-2016}'s analysis is complementary to @cite{hacquard-2006}'s positional account: position determines WHICH TIME (high modal = speech time = present orientation; low modal = event time = past orientation), modal base kind determines WHICH DIRECTION (DOX blocks future, CIR permits future). The Klecha2016 docstring §4 (line 44) records the prose claim; this bridge makes it kernel-checked.

@cite{hacquard-2006}'s positionToOrientation covers past + present but is silent on future (the position-to-orientation map has no future case). @cite{klecha-2016}'s ModalBaseKind.permitsOrientation adds the future-orientation discriminator. Together they cover all three orientations.

theorem Klecha2016.klecha_hacquard_complementary : Hacquard2006.positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.aboveAsp = Core.Modality.TemporalOrientation.present ∧ Hacquard2006.positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.belowAsp = Core.Modality.TemporalOrientation.past ∧ Core.Modality.ModalBaseKind.circumstantial.permitsOrientation Core.Time.Tense.GramTense.future = true ∧ Core.Modality.ModalBaseKind.doxastic.permitsOrientation Core.Time.Tense.GramTense.future = false

Phase F bridge — Klecha-Hacquard complementarity: @cite{hacquard-2006}'s positionToOrientation covers past + present from modal position; @cite{klecha-2016}'s ModalBaseKind.permitsOrientation covers future from modal base kind. The conjunction below confirms the four cells: (aboveAsp → present), (belowAsp → past), (circumstantial permits future), (doxastic blocks future).

The cross-framework auditor (0.230.453) flagged the genuine Klecha-Ogihara divergence: not past-under-past (where they converge — both predict simultaneous via Ogihara's zero-tense vs Klecha's DOX+NPST), but hope + past with future-oriented reading. @cite{klecha-2016}'s CIR+NPST mechanism (cell §6 above) uniformly handles "Martina hoped Carissa got pregnant" with the future-oriented reading; @cite{ogihara-1996}'s PastReading enum classifies past morphology only and has no machinery for future-under-modal.

The bridge below makes Klecha's coverage of the case kernel-checked. @cite{ogihara-1996}'s silence is the absence of any theorem in Studies/Ogihara1996.lean covering this configuration; that absence is a substantive empirical claim about the scope of Ogihara's mechanism.

theorem Klecha2016.klecha_covers_hope_future_oriented_reading (hopeTime embRT : ℤ) (h : embRT > hopeTime) : Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial hopeTime embRT ∧ Core.Time.Tense.GramTense.nonpast.constrains embRT hopeTime

Phase F bridge — Klecha covers hope + past with future-oriented reading via CIR + NPST (cell §6 above); @cite{ogihara-1996}'s machinery does not.

theorem Klecha2016.klecha_actualHistoryBase_eq_substrate_metaphysicalAlternatives {W : Type u_1} (history : Core.Modality.HistoricalAlternatives.WorldHistory W ℤ) (concept : Semantics.Tense.DeRe.TimeConcept W Unit Unit ℤ) (matrix : Core.Context.KContext W Unit Unit ℤ) : have dr := { concept := concept, holderContext := matrix }; Semantics.Tense.DeRe.TemporalDeReReading.metaphysicalAlternatives history dr = Core.Modality.HistoricalAlternatives.actualHistoryBase history matrix.toSituation

Substrate bridge: @cite{klecha-2016}'s actual-history base actualHistoryBase history matrix.toSituation IS the substrate's TemporalDeReReading.metaphysicalAlternatives (defined in Theories/Semantics/Tense/DeRe.lean) for a TemporalDeReReading whose holderContext projects to matrix. The substrate's metaphysical-alternatives constructor was designed to recover Klecha's DOX behavior; this theorem makes the equivalence kernel-checked (provable by rfl).