@cite{egressy-2026}: Size-Sensitive Sequence of Tense in Hungarian

@cite{egressy-2026}

Empirical data from @cite{egressy-2026}, who shows that Hungarian is a partial SOT language: the simultaneous reading of past-under-past is available in structurally small complements (TP, without hogy 'that') but blocked in full CP complements (with hogy).

Key Empirical Findings

1. CP complements (with hogy): shifted reading only

   • Ági tudta, hogy Mari beteg volt. → only "Mari was sick before Ági knew"

2. Bare TP complements (no hogy): both shifted and simultaneous readings

   • Ági tudta Marit betegnek. → ambiguous: shifted or simultaneous

3. Temporal adverb diagnostics: akkor 'then' forces temporal anchoring and disambiguates complement size effects

4. Williams Cycle: Hungarian is mid-cycle — CP has become opaque to tense Agree while TP remains transparent

Data Organization

Theory-neutral empirical judgments, followed by bridge theorems connecting these to @cite{zeijlstra-2012}'s Agree-based SOT theory: fragment grounding, complement-size mapping, per-datum predictions, Williams Cycle classification, and temporal adverb diagnostics.

inductive Egressy2026.HungarianComplementType : Type

Hungarian complement types distinguished by structural size.

The key empirical distinction: complements with the overt complementizer hogy 'that' are full CPs; complements without hogy are structurally smaller (TP-sized).

• hogyCP : HungarianComplementType

  Full CP with hogy 'that' — opaque to SOT

• bareTP : HungarianComplementType

  Bare finite complement without hogy — transparent to SOT

@[implicit_reducible]

instance Egressy2026.instDecidableEqHungarianComplementType : DecidableEq HungarianComplementType

Equations

• Egressy2026.instDecidableEqHungarianComplementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Egressy2026.instReprHungarianComplementType.repr : HungarianComplementType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Egressy2026.instReprHungarianComplementType : Repr HungarianComplementType

Equations

• Egressy2026.instReprHungarianComplementType = { reprPrec := Egressy2026.instReprHungarianComplementType.repr }

def Egressy2026.HungarianComplementType.hasHogy : HungarianComplementType → Bool

Whether the complement type includes the complementizer hogy.

Equations

• Egressy2026.HungarianComplementType.hogyCP.hasHogy = true
• Egressy2026.HungarianComplementType.bareTP.hasHogy = false

structure Egressy2026.SOTJudgment : Type

An empirical SOT judgment: a past-under-past sentence with its complement type and available readings.

Each entry records:

• The matrix verb
• The complement type (CP with hogy vs bare TP)
• Whether the simultaneous reading is available
• Whether the shifted reading is available (always true)

• matrixVerb : String

  Matrix verb (Hungarian)

• matrixGloss : String

  Matrix verb gloss

• complementType : HungarianComplementType

  Complement type

• example_ : String

  Example sentence

• shiftedGloss : String

  English translation (shifted reading)

• simultaneousGloss : Option String

  English translation (simultaneous reading, if available)

• simultaneousAvailable : Bool

  Is the simultaneous reading available?

• shiftedAvailable : Bool

  Is the shifted reading available? (always true)

def Egressy2026.instReprSOTJudgment.repr : SOTJudgment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Egressy2026.instReprSOTJudgment : Repr SOTJudgment

Equations

• Egressy2026.instReprSOTJudgment = { reprPrec := Egressy2026.instReprSOTJudgment.repr }

def Egressy2026.instBEqSOTJudgment.beq : SOTJudgment → SOTJudgment → Bool

Equations

• One or more equations did not get rendered due to their size.
• Egressy2026.instBEqSOTJudgment.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Egressy2026.instBEqSOTJudgment : BEq SOTJudgment

Equations

• Egressy2026.instBEqSOTJudgment = { beq := Egressy2026.instBEqSOTJudgment.beq }

CP complements (with hogy): shifted only

def Egressy2026.pastUnderPast_hogyCP_tudta : SOTJudgment

@cite{egressy-2026}, ex. (9): Ági tud-t-a, hogy Mari beteg vol-t. 'Ági know-PST-3SG that Mari sick be-PST' → Shifted only: Mari was sick before Ági's knowing

Equations

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

def Egressy2026.pastUnderPast_hogyCP_mondta : SOTJudgment

@cite{egressy-2026}, ex. (11a): Ági mond-t-a, hogy Mari beteg vol-t. 'Ági say-PST-3SG that Mari sick be-PST' → Shifted only in full CP

Equations

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

def Egressy2026.pastUnderPast_hogyCP_hitte : SOTJudgment

@cite{egressy-2026}, ex. (11b): Ági hit-t-e, hogy Mari beteg vol-t. 'Ági believe-PST-3SG that Mari sick be-PST' → Shifted only in full CP

Equations

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

Bare TP complements (without hogy): both readings

def Egressy2026.pastUnderPast_bareTP_tudta : SOTJudgment

@cite{egressy-2026}, ex. (10): Ági tud-t-a Mari-t beteg-nek. 'Ági know-PST-3SG Mari-ACC sick-DAT' → Both readings: shifted and simultaneous

Equations

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

def Egressy2026.allJudgments : List SOTJudgment

All SOT judgments from the study.

Equations

• Egressy2026.allJudgments = [Egressy2026.pastUnderPast_hogyCP_tudta, Egressy2026.pastUnderPast_hogyCP_mondta, Egressy2026.pastUnderPast_hogyCP_hitte, Egressy2026.pastUnderPast_bareTP_tudta]

def Egressy2026.cpJudgments : List SOTJudgment

CP complement judgments: shifted only.

Equations

• Egressy2026.cpJudgments = List.filter (fun (x : Egressy2026.SOTJudgment) => x.complementType == Egressy2026.HungarianComplementType.hogyCP) Egressy2026.allJudgments

def Egressy2026.tpJudgments : List SOTJudgment

Bare TP judgments: both readings.

Equations

• Egressy2026.tpJudgments = List.filter (fun (x : Egressy2026.SOTJudgment) => x.complementType == Egressy2026.HungarianComplementType.bareTP) Egressy2026.allJudgments

theorem Egressy2026.hogyCP_tudta_no_simultaneous : pastUnderPast_hogyCP_tudta.simultaneousAvailable = false

All CP complement judgments block the simultaneous reading.

theorem Egressy2026.hogyCP_mondta_no_simultaneous : pastUnderPast_hogyCP_mondta.simultaneousAvailable = false

theorem Egressy2026.hogyCP_hitte_no_simultaneous : pastUnderPast_hogyCP_hitte.simultaneousAvailable = false

theorem Egressy2026.bareTP_tudta_simultaneous : pastUnderPast_bareTP_tudta.simultaneousAvailable = true

Bare TP judgments allow the simultaneous reading.

theorem Egressy2026.all_shifted_available : (allJudgments.all fun (x : SOTJudgment) => x.shiftedAvailable) = true

All judgments have the shifted reading available.

theorem Egressy2026.no_cp_simultaneous : (cpJudgments.all fun (j : SOTJudgment) => !j.simultaneousAvailable) = true

No CP judgment has the simultaneous reading.

theorem Egressy2026.all_tp_simultaneous : (tpJudgments.all fun (x : SOTJudgment) => x.simultaneousAvailable) = true

All bare TP judgments have the simultaneous reading.

Prove that the string literals in Data.lean match the Fragment entries. This ensures the data is derived from fragments, not independently stipulated.

theorem Egressy2026.tudta_from_fragment : pastUnderPast_hogyCP_tudta.matrixVerb = Fragments.Hungarian.Predicates.tud.formPastDef

tudta in Data.lean is the past definite form of tud.

theorem Egressy2026.mondta_from_fragment : pastUnderPast_hogyCP_mondta.matrixVerb = Fragments.Hungarian.Predicates.mond.formPastDef

mondta in Data.lean is the past definite form of mond.

theorem Egressy2026.hitte_from_fragment : pastUnderPast_hogyCP_hitte.matrixVerb = Fragments.Hungarian.Predicates.hisz.formPastDef

hitte in Data.lean is the past definite form of hisz.

theorem Egressy2026.bareTP_tudta_from_fragment : pastUnderPast_bareTP_tudta.matrixVerb = Fragments.Hungarian.Predicates.tud.formPastDef

The bare TP tudta also matches the past definite form. (Both CP and bare TP examples use definite conjugation with tud.)

theorem Egressy2026.glosses_from_fragments : pastUnderPast_hogyCP_tudta.matrixGloss = "knew" ∧ pastUnderPast_hogyCP_mondta.matrixGloss = "said" ∧ pastUnderPast_hogyCP_hitte.matrixGloss = "believed"

Glosses match fragment glosses.

def Egressy2026.complementTypeToSize : HungarianComplementType → Minimalist.ComplementSize

Map Hungarian complement types to structural complement sizes.

• hogy-CP → full CP (fValue 6, phase-sized, opaque)
• bare TP → TP (fValue 2, sub-phase, transparent)

Equations

• Egressy2026.complementTypeToSize Egressy2026.HungarianComplementType.hogyCP = Minimalist.ComplementSize.cP
• Egressy2026.complementTypeToSize Egressy2026.HungarianComplementType.bareTP = Minimalist.ComplementSize.tP

theorem Egressy2026.hogyCP_is_cP : complementTypeToSize HungarianComplementType.hogyCP = Minimalist.ComplementSize.cP

hogy-CP maps to CP.

theorem Egressy2026.bareTP_is_tP : complementTypeToSize HungarianComplementType.bareTP = Minimalist.ComplementSize.tP

Bare TP maps to TP.

theorem Egressy2026.hogy_fragment_matches_mapping : complementTypeToSize HungarianComplementType.hogyCP = Fragments.Hungarian.FunctionWords.hogy.complementSize

The hogy fragment entry and the complementTypeToSize function agree.

theorem Egressy2026.hogyCP_opaque : (complementTypeToSize HungarianComplementType.hogyCP).transparentToTenseAgree = false

hogy-CP is opaque to tense Agree.

theorem Egressy2026.bareTP_transparent : (complementTypeToSize HungarianComplementType.bareTP).transparentToTenseAgree = true

Bare TP is transparent to tense Agree.

theorem Egressy2026.hogyCP_predicted_readings : Minimalist.Tense.AgreeSOT.availableReadingsBySize (complementTypeToSize HungarianComplementType.hogyCP) = [Semantics.Tense.EmbeddedTenseReading.shifted]

Predicted readings for hogy-CP: shifted only.

theorem Egressy2026.bareTP_predicted_readings : Minimalist.Tense.AgreeSOT.availableReadingsBySize (complementTypeToSize HungarianComplementType.bareTP) = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

Predicted readings for bare TP: both shifted and simultaneous.

For each empirical judgment, prove that the observed availability of the simultaneous reading matches what availableReadingsBySize predicts for the complement type.

def Egressy2026.judgmentMatchesPrediction (j : SOTJudgment) : Bool

Helper: check if a judgment's simultaneous availability matches the theoretical prediction. The prediction is: simultaneous is available iff the complement is transparent to tense Agree.

Equations

• Egressy2026.judgmentMatchesPrediction j = (j.simultaneousAvailable == (Egressy2026.complementTypeToSize j.complementType).transparentToTenseAgree)

theorem Egressy2026.tudta_hogyCP_matches : judgmentMatchesPrediction pastUnderPast_hogyCP_tudta = true

tudta + hogy-CP: no simultaneous reading, as predicted.

theorem Egressy2026.mondta_hogyCP_matches : judgmentMatchesPrediction pastUnderPast_hogyCP_mondta = true

mondta + hogy-CP: no simultaneous reading, as predicted.

theorem Egressy2026.hitte_hogyCP_matches : judgmentMatchesPrediction pastUnderPast_hogyCP_hitte = true

hitte + hogy-CP: no simultaneous reading, as predicted.

theorem Egressy2026.tudta_bareTP_matches : judgmentMatchesPrediction pastUnderPast_bareTP_tudta = true

tudta + bare TP: simultaneous reading available, as predicted.

theorem Egressy2026.all_judgments_match : allJudgments.all judgmentMatchesPrediction = true

All judgments match predictions.

def Egressy2026.hungarianStage : Minimalist.Tense.AgreeSOT.WilliamsCycleStage

Hungarian's Williams Cycle stage.

Equations

• Egressy2026.hungarianStage = Minimalist.Tense.AgreeSOT.WilliamsCycleStage.partialSOT

theorem Egressy2026.hungarian_partial_sot : Minimalist.Tense.AgreeSOT.readingsByStage hungarianStage (complementTypeToSize HungarianComplementType.bareTP) = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous] ∧ Minimalist.Tense.AgreeSOT.readingsByStage hungarianStage (complementTypeToSize HungarianComplementType.hogyCP) = [Semantics.Tense.EmbeddedTenseReading.shifted]

Hungarian's partial SOT matches the empirical pattern: both readings in TP, shifted only in CP.

def Egressy2026.englishStage : Minimalist.Tense.AgreeSOT.WilliamsCycleStage

English, by contrast, is full SOT — both readings in all complement types.

Equations

• Egressy2026.englishStage = Minimalist.Tense.AgreeSOT.WilliamsCycleStage.fullSOT

theorem Egressy2026.english_full_sot (ct : HungarianComplementType) : Minimalist.Tense.AgreeSOT.readingsByStage englishStage (complementTypeToSize ct) = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]

def Egressy2026.japaneseStage : Minimalist.Tense.AgreeSOT.WilliamsCycleStage

Japanese is non-SOT — shifted only in all complement types.

Equations

• Egressy2026.japaneseStage = Minimalist.Tense.AgreeSOT.WilliamsCycleStage.noSOT

theorem Egressy2026.japanese_no_sot (ct : HungarianComplementType) : Minimalist.Tense.AgreeSOT.readingsByStage japaneseStage (complementTypeToSize ct) = [Semantics.Tense.EmbeddedTenseReading.shifted]

The temporal adverb előző nap 'the day before' forces the shifted reading. In hogy-CP complements (where only shifted is available), this is compatible. In bare TP complements (where both readings are available), it selects the shifted reading. This provides independent evidence that the CP complement really does lack the simultaneous reading, rather than there being some other blocking effect.

theorem Egressy2026.elozo_nap_compat_hogyCP : Fragments.Hungarian.TemporalDeictic.elozo_nap.forcesShifted = true ∧ (complementTypeToSize HungarianComplementType.hogyCP).transparentToTenseAgree = false

előző nap is compatible with hogy-CP (shifted-only) complements, because it itself forces the shifted reading.

theorem Egressy2026.aznap_diagnoses_bareTP : Fragments.Hungarian.TemporalDeictic.aznap.compatSimultaneous = true ∧ (complementTypeToSize HungarianComplementType.bareTP).transparentToTenseAgree = true

aznap 'that day' can diagnose the simultaneous reading in bare TP, because it is compatible with both readings.

theorem Egressy2026.akkor_shifts : Fragments.Hungarian.TemporalDeictic.akkor.shiftsPerspective = true

Hungarian akkor 'then' shifts perspective, like all cross-linguistic "then" adverbs.

@cite{egressy-2026} uses the definite/indefinite conjugation split as independent evidence for complement size. hogy-CP triggers definite conjugation; bare complements may allow indefinite.

The fragment entries record both conjugation forms, so we can verify
that the matrix verb forms in the data entries are the expected
conjugation type. 

theorem Egressy2026.hogyCP_uses_definite_conjugation : pastUnderPast_hogyCP_tudta.matrixVerb = Fragments.Hungarian.Predicates.tud.formPastDef ∧ pastUnderPast_hogyCP_mondta.matrixVerb = Fragments.Hungarian.Predicates.mond.formPastDef ∧ pastUnderPast_hogyCP_hitte.matrixVerb = Fragments.Hungarian.Predicates.hisz.formPastDef

All hogy-CP judgments use the definite conjugation past form.