[Egr26]: Size-Sensitive Sequence of Tense in Hungarian

[Egr26]

János Egressy shows that the availability of the simultaneous reading of a past-under-past configuration in Hungarian depends on a clause-internal property of the embedded clause, not on the matrix verb or on the complementizer hogy (which is an edge marker, not a C head — Hungarian has no CP, [EK23]):

• Non-speech-reporting clauses (perception, dreaming, belief — clauses that do not encode the content of a verbal/representational sign) pattern like English: a past-under-past clause has a simultaneous reading (and, pragmatics permitting, a back-shifted one).
• Speech-reporting clauses (the content of say/shout/growl) pattern like Japanese: only the back-shifted reading.

The analysis: speech-reporting clauses carry an extra Say layer (Say > Foc > T) above the bare TP of non-speech-reporting clauses ([Maj21], [Kri23]). The simultaneous reading comes from the optional LF deletion of the embedded PAST under an agreeing matrix PAST — the Sequence of Tense Rule of [Ogi96] / [OS12]. Crucially this SOT-Agree obeys the Williams Cycle ([Wil03a]), i.e. [Kei19]'s selective opacity generalized from movement to Agree: an Agree dependency from T cannot cross a larger Say projection. So it crosses a TP (simultaneous available) but is blocked by a SayP (back-shift only). Williams-Cycle sensitivity favors the SOT-Agree analysis over a res-movement (de re) account of simultaneity ([Abu88], [Abu97]), which would be unboundedly free (see de_re_overgenerates).

Formalization strategy

The opacity is derived, not stipulated: the Say head sits at fValue 5 in the shared functional sequence (Syntax.Minimalist), and the SOT transparency of a complement is exactly ComplementSize.transparentToSOTAgree (fLevel < fValue .Say). This reuses the very machinery that derives the ban on hyperraising and Hindi long-distance Agree ([Kei20]); see sot_is_selective_opacity. There is no language-wide "SOT stage" parameter — the two Hungarian clause types reproduce the two values of the binary SOTParameter clause-internally (nonSpeech_eq_relative, speech_eq_absolute).

The licensing interface

Past-under-past embeddings have a simultaneous and a backward-shifted reading (and, with an intervening future, a forward-shifted one). Rival accounts — relational/feature ([KZ18]), deletion ([Ogi19]), res-movement de re, clause-size ([Egr26]) — disagree only about when each reading is licensed, not about what a reading is: a reading is which comparison atom (Core.Order) the embedded reference time bears to its anchor. Tense.embeddedFrame puts the anchor at the matrix event time, so the three readings are exactly the frame predicates (isPast_iff_atom and kin).

A licensing theory is one LocalLicense — off an immediately containing clause and the clause it contains, which atoms are licensed; profile folds a license pairwise along the c-command chain, so an intervening tense re-anchors.

structure Egressy2026.Node : Type

A node in an embedding chain: a clause's morphological tense as a relative comparison cell (past = notAfter, the ≤ of [KZ18]) and its framework-neutral size grade (a Minimalist clause provides it as ClauseSpine.fLevel).

• tense : Finset Ordering

  The clause's tense as a relative comparison cell to its anchor.

• size : ℕ

  The clause's framework-neutral size grade.

@[reducible, inline]

abbrev Egressy2026.LocalLicense : Type

A licensing theory: given a containing clause and the clause it immediately contains, which comparison atoms hold between the contained reference time and its anchor.

Equations

• Egressy2026.LocalLicense = (Egressy2026.Node → Egressy2026.Node → Finset Ordering)

def Egressy2026.profile (L : LocalLicense) : Node → List Node → List (Finset Ordering)

Compose a license pairwise along the c-command chain (matrix first): the licensed reading-set at each embedding level. Adjacency-local — not a fold or product — so an intervening tense re-anchors and blocking propagates ([Ogi96]'s past-under-will-under-past).

Equations

• Egressy2026.profile L x✝ [] = []
• Egressy2026.profile L x✝ (c :: rest) = L x✝ c :: Egressy2026.profile L c rest

def Egressy2026.Simultaneous (s : Finset Ordering) : Prop

The simultaneous reading is licensed iff the eq atom is.

Equations

• Egressy2026.Simultaneous s = (Ordering.eq ∈ s)

def Egressy2026.Backshifted (s : Finset Ordering) : Prop

The backward-shifted reading is licensed iff the lt atom is.

Equations

• Egressy2026.Backshifted s = (Ordering.lt ∈ s)

def Egressy2026.ForwardShifted (s : Finset Ordering) : Prop

The forward-shifted reading is licensed iff the gt atom is.

Equations

• Egressy2026.ForwardShifted s = (Ordering.gt ∈ s)

@[instance_reducible]

instance Egressy2026.instDecidableSimultaneous (s : Finset Ordering) : Decidable (Simultaneous s)

Equations

• Egressy2026.instDecidableSimultaneous s = Egressy2026.instDecidableSimultaneous._aux_1 s

@[instance_reducible]

instance Egressy2026.instDecidableBackshifted (s : Finset Ordering) : Decidable (Backshifted s)

Equations

• Egressy2026.instDecidableBackshifted s = Egressy2026.instDecidableBackshifted._aux_1 s

@[instance_reducible]

instance Egressy2026.instDecidableForwardShifted (s : Finset Ordering) : Decidable (ForwardShifted s)

Equations

• Egressy2026.instDecidableForwardShifted s = Egressy2026.instDecidableForwardShifted._aux_1 s

For an embedded frame whose perspective time is the matrix event time (Tense.embeddedFrame), the licensed atom is its R-vs-P comparison, and the three named readings are exactly ReichenbachFrame.isPast/isPresent/isFuture.

theorem Egressy2026.isPast_iff_atom {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : f.isPast ↔ compare f.referenceTime f.perspectiveTime = Ordering.lt

theorem Egressy2026.isPresent_iff_atom {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : f.isPresent ↔ compare f.referenceTime f.perspectiveTime = Ordering.eq

theorem Egressy2026.isFuture_iff_atom {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : f.isFuture ↔ compare f.referenceTime f.perspectiveTime = Ordering.gt

def Egressy2026.sizeGatedLicense (boundary : ℕ) : LocalLicense

Generic size gate: an opaque clause (size not below boundary) loses the simultaneous (eq) atom; a transparent one keeps the full relative tense. This is the size half of a clause-size SOT account; it is not by itself the [Egr26] license, which also requires an agreeing past (LocalLicense.gate, egressyLicense). On uniformly past-under-past data the two coincide; they diverge once an intervening future appears.

Equations

• Egressy2026.sizeGatedLicense boundary x✝ c = if c.size < boundary then c.tense else c.tense.erase Ordering.eq

def Egressy2026.LocalLicense.gate (L : LocalLicense) (g : Node → Node → Bool) : LocalLicense

Refine a license by an extra gate: keep its reading set, but drop the simultaneous atom .eq wherever the gate fails. A theory composes its licensing conditions as successive gates — the SOT rule is a size gate refined by an agreeing-past gate, i.e. (sizeGatedLicense b).gate agreeingPast.

Equations

• L.gate g a c = if g a c = true then L a c else (L a c).erase Ordering.eq

Pragmatic narrowing (layer 2: a constraint on the grammatical reading set)

Grammar (a LocalLicense) emits the grammatically available reading set; a pragmatic inference then narrows it — direct perception (one cannot perceive a past event), a cessation implicature, etc. A narrowing is intersection with a context-conditioned constraint (a further point-algebra relation), so it can only remove readings, never license a new one — the grammar/pragmatics boundary, free from Finset.inter_subset_left rather than a stipulated law. The context C is whatever the inference consults.

@[reducible, inline]

abbrev Egressy2026.Narrowing (C : Type u_1) : Type u_1

A pragmatic narrowing: the point-algebra constraint it imposes, as a function of the context the inference consults.

Equations

• Egressy2026.Narrowing C = (C → Finset Ordering)

def Egressy2026.Narrowing.apply {C : Type u_1} (n : Narrowing C) (ctx : C) (s : Finset Ordering) : Finset Ordering

Narrow a grammatically-licensed reading set: intersect with the constraint.

Equations

• n.apply ctx s = s ∩ n ctx

theorem Egressy2026.Narrowing.apply_subset {C : Type u_1} (n : Narrowing C) (ctx : C) (s : Finset Ordering) : n.apply ctx s ⊆ s

Pragmatics filters, never licenses: narrowing only removes readings.

The two clause types and their size

inductive Egressy2026.ClauseType : Type

The clause-internal distinction [Egr26] draws: whether an embedded clause encodes the content of a verbal/representational sign. This is a property of the clause, independent of the matrix verb (hall 'hear' and gondol 'think' embed either type) and of hogy.

• nonSpeechReporting : ClauseType

  Perception, dreaming, belief: no Say layer, a bare TP.

• speechReporting : ClauseType

  The content of a verbal/representational sign: an extra Say layer (SayP).

@[instance_reducible]

instance Egressy2026.instDecidableEqClauseType : DecidableEq ClauseType

Equations

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

def Egressy2026.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Egressy2026.instReprClauseType : Repr ClauseType

Equations

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

def Egressy2026.ClauseType.complementSize : ClauseType → Minimalist.ComplementSize

The structural size of each clause type in the shared functional sequence: non-speech-reporting = TP, speech-reporting = SayP (Say > Foc > T).

Equations

• Egressy2026.ClauseType.nonSpeechReporting.complementSize = Minimalist.ComplementSize.tP
• Egressy2026.ClauseType.speechReporting.complementSize = Minimalist.ComplementSize.sayP

theorem Egressy2026.speech_larger_than_nonspeech : ClauseType.nonSpeechReporting.complementSize.fLevel < ClauseType.speechReporting.complementSize.fLevel

Speech-reporting clauses are strictly larger than non-speech-reporting ones (SayP dominates TP).

SOT-Agree opacity is selective opacity (the Williams Cycle)

def Egressy2026.sotProbe : Minimalist.Probe.Profile

The Sequence-of-Tense probe: a T-probe whose horizon is the Say layer. Deletion-under-Agree of an embedded PAST searches down from a matrix T and is terminated by a Say head ([Egr26], generalizing [Kei19]).

Equations

• Egressy2026.sotProbe = { probeHead := Minimalist.Cat.T, horizon := some Minimalist.Cat.Say }

def Egressy2026.nonSpeechSpine : List Minimalist.Cat

Projected heads of a non-speech-reporting clause (a bare TP): no Say.

Equations

• Egressy2026.nonSpeechSpine = [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T]

def Egressy2026.speechSpine : List Minimalist.Cat

Projected heads of a speech-reporting clause (a SayP): contains Say.

Equations

• Egressy2026.speechSpine = [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.Say]

theorem Egressy2026.sot_crosses_TP : sotProbe.transparentToLabel nonSpeechSpine = true

The SOT probe crosses a TP: a non-speech-reporting clause is transparent.

theorem Egressy2026.sot_blocked_by_SayP : sotProbe.transparentToLabel speechSpine = false

The SOT probe is blocked by a SayP: a speech-reporting clause is opaque.

theorem Egressy2026.sot_is_selective_opacity : ClauseType.nonSpeechReporting.complementSize.transparentToSOTAgree = sotProbe.transparentToLabel nonSpeechSpine ∧ ClauseType.speechReporting.complementSize.transparentToSOTAgree = sotProbe.transparentToLabel speechSpine

The unification. SOT-Agree opacity is the same selective-opacity mechanism that the syntax layer uses for movement and Agree: the fValue-keyed ComplementSize.transparentToSOTAgree agrees with the horizon-keyed Probe.transparentToLabel of sotProbe on both clause types. (Compare Minimalist.Probe a_movement_typology for hyperraising.)

theorem Egressy2026.sot_opaque_above_say (cs : Minimalist.ComplementSize) (h : Minimalist.fValue Minimalist.Cat.Say ≤ cs.fLevel) : cs.transparentToSOTAgree = false

Upward entailment ([Kei20]): the SayP boundary is monotone — any complement at or above the Say layer is opaque to SOT-Agree. (Speas–Tenny SA, Force, and C all sit at or above Say.)

The Egressy license and the predictions

The Sequence-of-Tense rule is a LocalLicense: the Say-boundary size gate, refined by an agreeing-past gate (SOT deletion needs an agreeing PAST). The predictions are the interface's Simultaneous/Backshifted over licensed atom sets, not a bespoke reading function.

def Egressy2026.sayBoundary : ℕ

The Say boundary: the Say layer's grade on the clause-size scale.

Equations

• Egressy2026.sayBoundary = Minimalist.ComplementSize.sayP.fLevel

def Egressy2026.clauseNode (tense : Finset Ordering) (ct : ClauseType) : Node

A clause node: a tense cell (notAfter = past, after = future — the ungated reading set of [KZ18]) and the neutral size of its ClauseType.

Equations

• Egressy2026.clauseNode tense ct = { tense := tense, size := ct.complementSize.fLevel }

def Egressy2026.pastMatrix : Node

A past matrix clause (the container; only its tense matters to licensing).

Equations

• Egressy2026.pastMatrix = { tense := Core.Order.notAfter, size := 0 }

def Egressy2026.agreeingPast : Node → Node → Bool

The agreeing-past gate: SOT deletion needs both the container and the contained clause to be morphologically past ([Ogi96]).

Equations

• Egressy2026.agreeingPast a c = (a.tense == Core.Order.notAfter && c.tense == Core.Order.notAfter)

def Egressy2026.egressyLicense : LocalLicense

[Egr26]'s license: the Say-boundary size gate refined by the agreeing-past gate. The size gate blocks simultaneity in speech-reporting (SayP) clauses; the agreeing-past refinement additionally blocks it under an intervening future (see ex18).

Equations

• Egressy2026.egressyLicense = (Egressy2026.sizeGatedLicense Egressy2026.sayBoundary).gate Egressy2026.agreeingPast

def Egressy2026.toReadings (s : Finset Ordering) : List Tense.EmbeddedTenseReading

Bridge from licensed atoms to the legacy EmbeddedTenseReading (atoms are canonical; this adapter feeds the binary SOTParameter comparison).

Equations

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

theorem Egressy2026.nonSpeech_both : Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting)) ∧ Backshifted (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting))

Non-speech-reporting (TP) clauses license both readings.

theorem Egressy2026.speech_backshift_only : ¬Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting)) ∧ Backshifted (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting))

Speech-reporting (SayP) clauses license only the back-shifted reading.

theorem Egressy2026.simultaneous_iff_nonSpeech (ct : ClauseType) : Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ct)) ↔ ct = ClauseType.nonSpeechReporting

The core asymmetry: simultaneity is blocked exactly in speech-reporting clauses.

Unification with the binary SOT parameter

Hungarian is not at a language-wide "SOT stage": its two clause types realize the two values of the binary SOTParameter ([OS12]) clause-internally — a non-speech-reporting clause behaves like an English (.relative) complement, a speech-reporting one like a Japanese (.absolute) one.

theorem Egressy2026.nonSpeech_eq_relative : toReadings (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting)) = Tense.availableReadings Tense.SOTParameter.relative

A non-speech-reporting clause reproduces the English (.relative) parameter.

theorem Egressy2026.speech_eq_absolute : toReadings (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting)) = Tense.availableReadings Tense.SOTParameter.absolute

A speech-reporting clause reproduces the Japanese (.absolute) parameter.

Empirical data ([Egr26], §2)

The verbs are grounded in Hungarian.Predicates; clause types are assigned by the embedding predicate (perception/cognition → non-speech-reporting; communication → speech-reporting). All examples are past-under-past with the embedded copula volt 'was'.

structure Egressy2026.SOTDatum : Type

A past-under-past judgment: matrix verb, the embedded clause type, and whether the simultaneous reading is observed.

• matrixVerb : String

  Matrix verb (Hungarian surface form)

• matrixGloss : String

  English gloss of the matrix verb

• clauseType : ClauseType

  The embedded clause type

• example_ : String

  Example sentence

• simultaneousObserved : Bool

  Is the simultaneous reading observed?

def Egressy2026.instReprSOTDatum.repr : SOTDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Egressy2026.instReprSOTDatum : Repr SOTDatum

Equations

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

def Egressy2026.ex4_lat : SOTDatum

ex. (4): direct perception with lát 'see' — simultaneous (only).

Equations

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

def Egressy2026.ex5_hall : SOTDatum

ex. (5): direct perception with hall 'hear' — simultaneous (only).

Equations

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

def Egressy2026.ex6_almodik : SOTDatum

ex. (6): dreaming with álmodik — simultaneous (only).

Equations

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

def Egressy2026.ex7_gondol : SOTDatum

ex. (7): belief with gondol 'think' — simultaneous and back-shifted.

Equations

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

def Egressy2026.ex8_aggaszt : SOTDatum

ex. (8): subject clause with aggaszt 'worry' — simultaneous and back-shifted.

Equations

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

def Egressy2026.ex11_mond : SOTDatum

ex. (11a): saying with mond 'say' — back-shifted only.

Equations

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

def Egressy2026.ex11_rikolt : SOTDatum

ex. (11b): shouting with rikolt 'shout' — back-shifted only.

Equations

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

def Egressy2026.ex11_morog : SOTDatum

ex. (11c): growling with morog 'growl' — back-shifted only.

Equations

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

def Egressy2026.allData : List SOTDatum

All single-embedding judgments.

Equations

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

def Egressy2026.predictsSimultaneous (d : SOTDatum) : Bool

The grammatical prediction via the Egressy license: is the simultaneous reading available for this datum's clause type (under a past matrix)?

Equations

• Egressy2026.predictsSimultaneous d = decide (Egressy2026.Simultaneous (Egressy2026.egressyLicense Egressy2026.pastMatrix (Egressy2026.clauseNode Core.Order.notAfter d.clauseType)))

theorem Egressy2026.all_data_match : (allData.all fun (d : SOTDatum) => d.simultaneousObserved == predictsSimultaneous d) = true

Every datum's observed simultaneous availability matches the prediction.

Fragment grounding: matrix verbs are the past forms of the lexical entries.

theorem Egressy2026.ex4_verb_from_fragment : ex4_lat.matrixVerb = Hungarian.Predicates.lat.formPastDef

theorem Egressy2026.ex5_verb_from_fragment : ex5_hall.matrixVerb = Hungarian.Predicates.hall.formPastDef

theorem Egressy2026.ex7_verb_from_fragment : ex7_gondol.matrixVerb = Hungarian.Predicates.gondol.formPastDef

theorem Egressy2026.ex11_verb_from_fragment : ex11_mond.matrixVerb = Hungarian.Predicates.mond.formPastDef

Pragmatic narrowing: direct perception is simultaneous-only

For the direct-perception examples (4)–(6) the back-shifted reading is excluded for pragmatic reasons — one cannot directly perceive a past event — even though it is grammatically available (nonSpeech_both). This is a layer-2 Narrowing: direct perception intersects the grammatical reading set with the overlapping (=) constraint, leaving simultaneous-only (direct_perception_narrows).

def Egressy2026.directPerceptionData : List SOTDatum

The direct-perception data (perception and dreaming).

Equations

• Egressy2026.directPerceptionData = [Egressy2026.ex4_lat, Egressy2026.ex5_hall, Egressy2026.ex6_almodik]

theorem Egressy2026.direct_perception_simultaneous : (directPerceptionData.all fun (d : SOTDatum) => d.simultaneousObserved && toReadings (egressyLicense pastMatrix (clauseNode Core.Order.notAfter d.clauseType)) == [Tense.EmbeddedTenseReading.shifted, Tense.EmbeddedTenseReading.simultaneous]) = true

Direct-perception clauses are observed with the simultaneous reading, while grammatically they are non-speech-reporting (both readings available); the absence of the back-shifted reading is pragmatic.

def Egressy2026.directPerception : Narrowing Unit

Direct perception as a layer-2 Narrowing: it imposes the overlapping (=) constraint — only a simultaneous reading is perceivable.

Equations

• Egressy2026.directPerception x✝ = Core.Order.overlapping

theorem Egressy2026.direct_perception_narrows : directPerception.apply () (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.nonSpeechReporting)) = Core.Order.overlapping

The prose fact as a theorem: direct perception narrows the grammatically both-readings non-speech license down to simultaneous-only.

Multiple embedding and locality ([Egr26], §2.3)

Simultaneity is computed locally between structurally adjacent clauses ([Ogi96]): profile folds egressyLicense pairwise down the chain (matrix first). The simultaneity at each level is Simultaneous of the licensed atoms.

def Egressy2026.simProfile (chain : List Node) : List Bool

The per-level simultaneity profile of an embedded chain under a past matrix.

Equations

• Egressy2026.simProfile chain = List.map (fun (s : Finset Ordering) => decide (Egressy2026.Simultaneous s)) (Egressy2026.profile Egressy2026.egressyLicense Egressy2026.pastMatrix chain)

def Egressy2026.ex16 : List Node

ex. (16): shout > see > be. The intermediate (content of the shout) is speech-reporting → back-shifted; the deepest (Mari's perception) is non-speech-reporting → simultaneous. Only adjacent clauses interact.

Equations

• Egressy2026.ex16 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting]

theorem Egressy2026.ex16_profile : simProfile ex16 = [false, true]

def Egressy2026.ex17 : List Node

ex. (17): hear > shout > be. Intermediate (perception of the shouting) → simultaneous; deepest (content of the shout) → back-shifted. Opposite of (16).

Equations

• Egressy2026.ex17 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting]

theorem Egressy2026.ex17_profile : simProfile ex17 = [true, false]

def Egressy2026.ex10 : List Node

ex. (10): dream > see > be, all non-speech-reporting → simultaneous throughout.

Equations

• Egressy2026.ex10 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.nonSpeechReporting]

theorem Egressy2026.ex10_profile : simProfile ex10 = [true, true]

def Egressy2026.ex15 : List Node

ex. (15): shout > growl > be, all speech-reporting → back-shifted throughout.

Equations

• Egressy2026.ex15 = [Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting]

theorem Egressy2026.ex15_profile : simProfile ex15 = [false, false]

def Egressy2026.ex18 : List Node

Past-under-will-under-past (English; [Ogi96], discussed by [Egr26]): said > will claim > was. The intervening future will (after) is not an agreeing past, so the deepest was has no simultaneous reading — the agreeingPast gate blocks it, independently of size (English is size-insensitive here).

Equations

• Egressy2026.ex18 = [Egressy2026.clauseNode Core.Order.after Egressy2026.ClauseType.speechReporting, Egressy2026.clauseNode Core.Order.notAfter Egressy2026.ClauseType.speechReporting]

theorem Egressy2026.ex18_no_simultaneous : simProfile ex18 = [false, false]

Williams-Cycle support over an unbounded de re alternative ([Egr26], §3.3)

An unbounded res-movement (de re) derivation would move the embedded PAST to an A-position inside the matrix VP, unstopped by the Say layer — hence size-blind. Egressy argues the Williams Cycle rules this out: a size-blind mechanism would license simultaneity for speech-reporting clauses, contrary to fact. The foil below ([Abu88], [Abu97]) is exactly that size-blind account; the restricted de re of [OS12] (and the Polish account of Mucha, Renans & Romoli) is a different, constrained mechanism this argument does not, on its own, refute.

def Egressy2026.deReUnrestricted : LocalLicense

The unbounded (size-blind) de re foil: it licenses every reading. Local to this study — it is Egressy's reductio against unbounded res-movement, not a neutral SOT mechanism.

Equations

• Egressy2026.deReUnrestricted x✝¹ x✝ = Core.Order.unrestricted

theorem Egressy2026.de_re_overgenerates : Simultaneous (deReUnrestricted pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting)) ∧ ¬Simultaneous (egressyLicense pastMatrix (clauseNode Core.Order.notAfter ClauseType.speechReporting))

The unbounded de re foil overgenerates: size-blind, it licenses simultaneity for a speech-reporting clause, which egressyLicense correctly blocks. This refutes unbounded res-movement, not the restricted de re of [OS12].