Levin (2026): The door pushed open

@cite{levin-2026}

The door pushed open: an English intransitive resultative construction with transitive-only verbs. Journal of East Asian Linguistics 35:3.

Core contribution

Identifies a neglected class of English intransitive resultatives — The door pushed open, The cork pulled free, The door slammed shut — where the base verb is transitive-only outside the construction. These verbs (push, slam, pull) cannot occur intransitively without the result phrase: *The door pushed.

Proposes that these "intr-push open" resultatives are the anticausative variant of the causative alternation, with their transitive counterparts (Pat pushed the door open) as the causative variant. The resultative construction itself licenses the alternation that the verb lacks in isolation.

Key empirical findings

1. Verb restriction: only verbs of exerting force (Levin §12) and verbs of surface contact (§18 hitting, §10.4 wiping subtypes)
2. Adjective restriction: only open, closed, shut, free, loose, flat — all describing spatially instantiated states
3. Verb–adjective combination is critical: neither alone suffices
4. Discourse licensing: anticausative conditions — cause recoverable in context or identity unknown to speaker
5. Semantic licensing: subject DP must be capable of autonomous motion ("projectile" — entity imbued with force that can act without continuous external involvement)
6. Proper Containment Condition (@cite{rappaport-hovav-levin-2012}): when the cause is continuously involved, the causative variant is required — blocking the intr-push open pattern

Architecture

This study connects four existing layers:

• Core.Lexical.LevinClass: verb classes lack causative alternation (§12, §18)
• Theories.Semantics.Causation.Resultatives: construction adds CAUSE; PCC maps onto the independent-source/tightness infrastructure
• Fragments.English.Predicates: verb and adjective entries
• Phenomena.ArgumentStructure.DiathesisAlternations: existing alternation data

The central theoretical insight — that constructions can license alternation behavior that verbs lack in isolation — is a construction grammar point that the current verb-level participatesIn infrastructure does not directly accommodate. This file formalizes the specific case.

Verb inventory

The verbs attested in intr-push open resultatives describe the application of force to an entity. They are drawn from two subclasses of manner verbs: verbs of exerting force (§12) and verbs of surface contact (§18 hitting, §10.4 wiping).

Note: scrape and sweep are Levin §10.4 (wipe) verbs, but in intr-push open they participate through their surface contact sense, not their removing sense. Wipe verbs as a class DO show the causative alternation (they lexicalize CoS). These verbs enter the construction because only their force-application component is relevant, not the removal result.

def Levin2026.intrPushOpenClasses : List Semantics.Lexical.LevinClass

The core Levin classes for intr-push open verbs. Verbs of exerting force (§12 = pushPull) and verbs of surface contact, hitting subtype (§18.1 = hit). Wipe verbs (§10.4) also participate but are handled separately (see all_verbs_from_predicted_classes).

Equations

• Levin2026.intrPushOpenClasses = [Semantics.Lexical.LevinClass.pushPull, Semantics.Lexical.LevinClass.hit]

theorem Levin2026.all_classes_no_causative_alternation : (intrPushOpenClasses.all fun (x : Semantics.Lexical.LevinClass) => !x.participatesIn Semantics.Lexical.DiathesisAlternation.causativeInchoative) = true

All core intr-push open verb classes lack the causative alternation in isolation. This is the key precondition: the verb alone does not alternate, so the construction must license the alternation.

theorem Levin2026.agrees_with_diathesis_data : (Phenomena.ArgumentStructure.DiathesisAlternations.Data.ci_hit.result == Phenomena.ArgumentStructure.DiathesisAlternations.Data.AlternationResult.blocked) = true

Cross-reference: the existing alternation data in DiathesisAlternations.Data already records that hit (§18.1) is blocked for causative/inchoative. Our theorem agrees.

theorem Levin2026.all_classes_pure_manner : (intrPushOpenClasses.all fun (x : Semantics.Lexical.LevinClass) => x.rootEntailments == Semantics.Lexical.Roots.RootEntailments.pureManner) = true

All core classes are pure manner roots (@cite{beavers-koontz-garboden-2020}): they encode no state, no result, no causation. The result and causation come from the construction.

theorem Levin2026.all_classes_no_cos_no_causation : (intrPushOpenClasses.all fun (c : Semantics.Lexical.LevinClass) => have mc := c.meaningComponents; mc.contact && mc.motion && !mc.changeOfState && !mc.causation) = true

All core classes encode contact and motion but NOT change of state and NOT causation. This is why they don't show the causative alternation (@cite{fillmore-1970}): no scalar change is lexicalized.

theorem Levin2026.push_is_pushPull : Fragments.English.Predicates.Verbal.push.levinClass = some Semantics.Lexical.LevinClass.pushPull

Fragment verb entries confirm the classification.

theorem Levin2026.pull_is_pushPull : Fragments.English.Predicates.Verbal.pull.levinClass = some Semantics.Lexical.LevinClass.pushPull

theorem Levin2026.kick_is_hit : Fragments.English.Predicates.Verbal.kick.levinClass = some Semantics.Lexical.LevinClass.hit

Construction-dependent alternation (@cite{goldberg-1995})

The key derivation: these verbs cannot alternate alone (shown above), but they CAN alternate inside the resultative construction. The resultative adds CoS + causation via semanticContribution; the composed meaning has all four components needed for the causative alternation. No new alternation logic is needed — predictedAlternation on the fused result fires automatically.

This formalizes the paper's central insight (§3): "when such verbs are found in a resultative, the construction as a whole describes a change of state ... properties of the resultative construction itself are implicated in the 'loosening' of transitivity that characterizes intr-push open resultatives."

theorem Levin2026.pushPull_alone_no_alternation : Semantics.Lexical.LevinClass.pushPull.meaningComponents.predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative = false

PushPull alone: no causative alternation.

theorem Levin2026.pushPull_alternates_in_resultative : ConstructionGrammar.predictedAlternationInConstruction Semantics.Lexical.LevinClass.pushPull.meaningComponents ConstructionGrammar.resultative Semantics.Lexical.DiathesisAlternation.causativeInchoative = true

PushPull in the resultative: causative alternation predicted. The construction adds CoS + causation → the composed meaning has changeOfState && causation, which is the precondition.

theorem Levin2026.hit_alone_no_alternation : Semantics.Lexical.LevinClass.hit.meaningComponents.predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative = false

Hit alone: no causative alternation.

theorem Levin2026.hit_alternates_in_resultative : ConstructionGrammar.predictedAlternationInConstruction Semantics.Lexical.LevinClass.hit.meaningComponents ConstructionGrammar.resultative Semantics.Lexical.DiathesisAlternation.causativeInchoative = true

Hit in the resultative: causative alternation predicted.

theorem Levin2026.all_classes_alternate_in_resultative : (intrPushOpenClasses.all fun (c : Semantics.Lexical.LevinClass) => ConstructionGrammar.predictedAlternationInConstruction c.meaningComponents ConstructionGrammar.resultative Semantics.Lexical.DiathesisAlternation.causativeInchoative) = true

All core intr-push-open classes alternate in the resultative.

Event structure shift (bridge to EventStructure)

The same fusion operation that predicts new alternations also predicts template shift: manner verbs (activity template) become accomplishments inside the resultative. This connects to telicity, result state diagnostics (again/re- ambiguity), and CAUSE structure.

theorem Levin2026.pushPull_is_activity : Semantics.Lexical.LevinClass.pushPull.eventTemplate = Features.EventStructure.Template.activity

PushPull alone is an activity (no CoS, no CAUSE).

theorem Levin2026.pushPull_accomplishment_in_resultative : (Semantics.Lexical.LevinClass.pushPull.meaningComponents.fuse ConstructionGrammar.resultative.semanticContribution).predictedTemplate = Features.EventStructure.Template.accomplishment

PushPull in the resultative shifts to accomplishment (the construction adds [CAUSE [BECOME [STATE]]]).

theorem Levin2026.hit_is_activity' : Semantics.Lexical.LevinClass.hit.eventTemplate = Features.EventStructure.Template.activity

Hit alone is an activity.

theorem Levin2026.hit_accomplishment_in_resultative : (Semantics.Lexical.LevinClass.hit.meaningComponents.fuse ConstructionGrammar.resultative.semanticContribution).predictedTemplate = Features.EventStructure.Template.accomplishment

Hit in the resultative shifts to accomplishment.

theorem Levin2026.pushPull_dual_in_resultative : (Semantics.Lexical.LevinClass.pushPull.meaningComponents.fuse ConstructionGrammar.resultative.semanticContribution).predictedTemplate = Features.EventStructure.Template.accomplishment ∧ (Semantics.Lexical.LevinClass.pushPull.meaningComponents.fuse ConstructionGrammar.resultative.semanticContribution).predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative = true ∧ (Semantics.Lexical.LevinClass.pushPull.meaningComponents.fuse ConstructionGrammar.resultative.semanticContribution).predictedTemplate.intransitiveVariant = some Features.EventStructure.Template.achievement

Full dual prediction for pushPull in the resultative: template shift AND alternation AND intransitive variant, all from one fusion.

theorem Levin2026.pushPull_vendler_shift : Semantics.Lexical.LevinClass.pushPull.eventTemplate.vendlerClass = Features.VendlerClass.activity ∧ (Semantics.Lexical.LevinClass.pushPull.meaningComponents.fuse ConstructionGrammar.resultative.semanticContribution).predictedTemplate.vendlerClass = Features.VendlerClass.accomplishment

Vendler class shift: pushPull goes from atelic activity to telic accomplishment inside the resultative.

Middle construction parallel (§2, examples 17–18)

The paper shows pound enters the middle construction only with a result phrase: "*This kind of metal pounds easily" vs "This kind of metal pounds flat easily." The existing predictedAlternationInConstruction infrastructure derives this — the middle alternation requires CoS, which comes from the resultative construction, not the verb.

theorem Levin2026.hit_no_middle_alone : Semantics.Lexical.LevinClass.hit.meaningComponents.predictedAlternation Semantics.Lexical.DiathesisAlternation.middle = false

Hit-class verbs (including pound) cannot enter the middle alone.

theorem Levin2026.hit_middle_in_resultative : ConstructionGrammar.predictedAlternationInConstruction Semantics.Lexical.LevinClass.hit.meaningComponents ConstructionGrammar.resultative Semantics.Lexical.DiathesisAlternation.middle = true

Hit-class verbs CAN enter the middle inside the resultative. This derives the paper's observation (18b) from the same mechanism.

Adjective inventory

Only a small set of adjectives heads the result phrase in intr-push open resultatives. Each describes a spatially instantiated state — a state whose attainment requires the entity to be in a specific spatial configuration with respect to a reference entity.

Three semantic subtypes:

1. Barrier configuration: open, closed, shut — spatial configuration of a barrier (door, gate, window) relative to its frame
2. Unattachment: free, loose — freedom from spatial contiguity with a reference entity (frame, bottle, ground)
3. Surface orientation: flat — orientation relative to a reference surface

@[reducible, inline]

abbrev Levin2026.SpatialAdjType : Type

Reuse the theory-level SpatialConfigType from Adjective.Theory.

Equations

• Levin2026.SpatialAdjType = Semantics.Gradability.SpatialConfigType

theorem Levin2026.all_attested_adjs_spatial : ([Fragments.English.Predicates.Adjectival.open_, Fragments.English.Predicates.Adjectival.closed_, Fragments.English.Predicates.Adjectival.shut, Fragments.English.Predicates.Adjectival.free_, Fragments.English.Predicates.Adjectival.loose, Fragments.English.Predicates.Adjectival.flat].all fun (x : Fragments.English.Predicates.Adjectival.AdjectivalPredicateEntry) => x.spatialConfigType.isSome) = true

All six attested adjectives have a spatial classification in their Fragment entries (structural, not string-based).

theorem Levin2026.all_attested_adjs_closed_scale : ([Fragments.English.Predicates.Adjectival.open_, Fragments.English.Predicates.Adjectival.closed_, Fragments.English.Predicates.Adjectival.shut, Fragments.English.Predicates.Adjectival.free_, Fragments.English.Predicates.Adjectival.loose, Fragments.English.Predicates.Adjectival.flat].all fun (x : Fragments.English.Predicates.Adjectival.AdjectivalPredicateEntry) => x.scaleType == Core.Scale.Boundedness.closed) = true

All attested adjectives are closed-scale (absolute) in @cite{kennedy-2007}'s terms. Spatially instantiated states have crisp endpoints (fully open vs. fully closed).

Adjectives in senses that are NOT spatially instantiated do not appear in intr-push open resultatives, even when they occur in transitive resultatives. The non-spatial senses of free ("free of charge", "free of debris") and loose ("loose shoelaces") are not attested. Adjectives like bald, firm, senseless, red have no spatialConfigType in the Fragment and are never attested in intr-push open resultatives (examples 57b–60b).

Transitive–intransitive pairing

The paper's central argument (§3): tr-push open and intr-push open form a causative alternation pair. The transitive is the causative variant; the intransitive is the anticausative variant. Both share the same verb–adjective combination and the same constructional meaning:

• Causative: [Agent_effector V NP] CAUSE [NP BECOME Adj]
• Anticausative: [NP BECOME Adj] (cause suppressed)

structure Levin2026.AlternationPair : Type

An alternation pair: transitive and intransitive resultative with the same verb–adjective combination.

• verb : String
• adjective : String
• transitive : String
• intransitive : String
• bareIntransitive : String
• verbClass : Semantics.Lexical.LevinClass
• adjType : SpatialAdjType

@[implicit_reducible]

instance Levin2026.instReprAlternationPair : Repr AlternationPair

Equations

• Levin2026.instReprAlternationPair = { reprPrec := Levin2026.instReprAlternationPair.repr }

def Levin2026.instReprAlternationPair.repr : AlternationPair → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Levin2026.instBEqAlternationPair : BEq AlternationPair

Equations

• Levin2026.instBEqAlternationPair = { beq := Levin2026.instBEqAlternationPair.beq }

def Levin2026.instBEqAlternationPair.beq : AlternationPair → AlternationPair → Bool

Equations

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

def Levin2026.push_open : AlternationPair

Push–open (examples 19, 20; 10a,b).

Equations

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

def Levin2026.pull_free : AlternationPair

Pull–free (examples 21, 22; 13a,b).

Equations

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

def Levin2026.slam_shut : AlternationPair

Slam–shut (fn. 11; intransitive from example 23). Note: slam is polysemous — in Pat slammed the door / The door slammed it has a closing-with-impact sense that independently shows the causative alternation. The .hit classification here applies to the surface-contact sense, not the closing sense. The transitive resultative is not explicitly given in the paper but is implied by the alternation pair analysis.

Equations

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

def Levin2026.punch_open : AlternationPair

Punch–open (intransitive from example 11a; transitive implied).

Equations

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

def Levin2026.fling_open : AlternationPair

Fling–open (intransitive from example 33; transitive implied).

Equations

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

def Levin2026.scrape_free : AlternationPair

Scrape–free (intransitive from example 39; transitive implied).

Equations

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

def Levin2026.smack_flat : AlternationPair

Smack–flat (intransitive from example 48; transitive implied).

Equations

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

def Levin2026.thump_closed : AlternationPair

Thump–closed (intransitive from example 12a; transitive from 12b).

Equations

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

def Levin2026.alternationPairs : List AlternationPair

Equations

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

theorem Levin2026.all_verbs_from_predicted_classes : (alternationPairs.all fun (d : AlternationPair) => intrPushOpenClasses.contains d.verbClass || d.verbClass == Semantics.Lexical.LevinClass.wipe) = true

All pairs use verbs from the predicted classes (pushPull, hit — or wipe for scrape/sweep).

theorem Levin2026.per_pair_alternation_core : ((List.filter (fun (x : AlternationPair) => intrPushOpenClasses.contains x.verbClass) alternationPairs).all fun (p : AlternationPair) => !p.verbClass.participatesIn Semantics.Lexical.DiathesisAlternation.causativeInchoative && ConstructionGrammar.predictedAlternationInConstruction p.verbClass.meaningComponents ConstructionGrammar.resultative Semantics.Lexical.DiathesisAlternation.causativeInchoative) = true

Each core-class pair (pushPull, hit) is blocked alone but gains the causative alternation inside the resultative construction. Wipe verbs (scrape/sweep) are excluded: they independently alternate because they lexicalize CoS; they enter the construction through their surface-contact sense, not their removing sense.

theorem Levin2026.push_open_adj_agrees : Fragments.English.Predicates.Adjectival.open_.spatialConfigType = some push_open.adjType

Each pair's adjType agrees with the Fragment entry's spatialConfigType.

theorem Levin2026.pull_free_adj_agrees : Fragments.English.Predicates.Adjectival.free_.spatialConfigType = some pull_free.adjType

theorem Levin2026.slam_shut_adj_agrees : Fragments.English.Predicates.Adjectival.shut.spatialConfigType = some slam_shut.adjType

theorem Levin2026.punch_open_adj_agrees : Fragments.English.Predicates.Adjectival.open_.spatialConfigType = some punch_open.adjType

theorem Levin2026.fling_open_adj_agrees : Fragments.English.Predicates.Adjectival.open_.spatialConfigType = some fling_open.adjType

theorem Levin2026.scrape_free_adj_agrees : Fragments.English.Predicates.Adjectival.free_.spatialConfigType = some scrape_free.adjType

theorem Levin2026.smack_flat_adj_agrees : Fragments.English.Predicates.Adjectival.flat.spatialConfigType = some smack_flat.adjType

theorem Levin2026.thump_closed_adj_agrees : Fragments.English.Predicates.Adjectival.closed_.spatialConfigType = some thump_closed.adjType

Negative evidence: verb alone doesn't suffice

Verbs outside the predicted classes do not license intr-push open even with an appropriate adjective (examples 51–56).

def Levin2026.blockedVerbs : List (String × String × String)

Verbs that occur in transitive resultatives with the relevant adjectives but lack intr-push open counterparts.

Equations

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

Negative evidence: adjective alone doesn't suffice

Even in their spatially instantiated senses, the adjectives can appear in transitive resultatives with verbs of the right type, yet the transitive resultative lacks an intr-push open counterpart when the COMBINATION is wrong (examples 57–60).

def Levin2026.blockedCombinations : List (String × String × String)

Equations

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

Causal dynamics and event decomposition

The constructional meaning of resultatives (§3, example 25): [Action denoted by verb] causes [change into state denoted by RP]

For tr-push open (§3, example 30): [Sam_effector push the door] CAUSE [the door BECOME open]

The constructional CAUSE comes from the resultative, not from the verb. The constructional BECOME maps to CoSType.inception (¬open → open).

def Levin2026.resultativeBECOME : Features.ChangeOfState.CoSType

The constructional BECOME in resultatives = inception (¬P → P). This connects to the existing ChangeOfState infrastructure.

Equations

• Levin2026.resultativeBECOME = Features.ChangeOfState.CoSType.inception

theorem Levin2026.push_open_uses_make : Semantics.Causation.Resultatives.resultativeCausativeBuilder = Features.Causative.make

The resultative uses the .make builder (sufficiency).

Key contrast: intr-push-open ≠ freeze-solid

"The river froze solid" is a noncausative resultative where freeze independently shows the causative alternation; the verbal alternation plus the noncausative subconstruction explain why it surfaces without a causer.

"The door pushed open" is fundamentally different: push does NOT independently alternate; the construction adds the CAUSE that the verb lacks. This is an anticausative licensed by the construction, not a lexically noncausative.

Per-scenario causal models for these contrasts live below in §7 (HammerFlat, KickIntoField, FreezeSolid, etc.) on the BoolSEM substrate, using BoolSEM.causallySufficientOn / completesForEffectOn from Core.Causal.SEM.Counterfactual.

theorem Levin2026.freeze_alternates_push_does_not : Semantics.Lexical.LevinClass.otherCoS.participatesIn Semantics.Lexical.DiathesisAlternation.causativeInchoative = true ∧ Semantics.Lexical.LevinClass.pushPull.participatesIn Semantics.Lexical.DiathesisAlternation.causativeInchoative = false

Freeze independently shows the causative alternation; push does not. This confirms the classification: freeze solid is a standard noncausative resultative with an alternating verb, while push open must be an anticausative licensed by the construction.

PCC and the independent-source analysis

The Proper Containment Condition (@cite{rappaport-hovav-levin-2012}): "When a change of state is properly contained within a causing act, the argument representing that act must be expressed in the same clause as the verb describing the change of state."

This maps onto the independent-source/tightness analysis already formalized in Causation/Resultatives.lean:

• Projectile (door after a push): the door has kinetic energy — an independent source. Once pushed, the door continues to swing without the agent. The agent's involvement is NOT continuously required. → The theme has an independent source → the cause is not necessary → anticausative OK.

• Continuous involvement (nailing a door shut): the agent must sustain force throughout. The door has NO independent source of motion. → No independent source → the cause IS necessary → the anticausative is blocked (PCC requires expressing the cause).

The PCC tightness analysis (projectile vs continuous, with the intervening-source breakdown of necessity) is formalized on the BoolSEM substrate below by IndependentSourceBreaksNecessity (§7) — see independent_source_breaks_necessity for the canonical not-tight witness.

Note: the witness is *our model*, not Levin 2019's specific
sentence-licensing argument. A genuine refutation theorem against
Goldberg & Jackendoff's licensing-not-necessity stance — using this
scenario as the disagreement witness — is the natural next step;
currently deferred. 

Anticausative discourse conditions

@cite{rappaport-hovav-2014} identifies two discourse situations where the anticausative variant is preferred over the causative:

1. The cause is recoverable from the discourse context — it has been established earlier or follows from the natural course of events (§5, examples 62–68).
2. The speaker does not know the identity of the cause — the existence of a cause can be inferred but its identity is unknown (§5, examples 69–71; McCawley 1978).

Intr-push open resultatives are found in precisely these two contexts.

inductive Levin2026.CauseStatus : Type

How the cause relates to the discourse context.

• recoverableInContext : CauseStatus

  Cause established in prior discourse or natural course of events. "The dry soil thawed ... the roots pulled free." (§5, ex. 64)

• identityUnknown : CauseStatus

  Cause inferable but identity unknown to speaker. "The door pushed open and a man walked in." (§5, ex. 70)

• notRecoverable : CauseStatus

  Cause novel and not recoverable; causative variant required.

@[implicit_reducible]

instance Levin2026.instDecidableEqCauseStatus : DecidableEq CauseStatus

Equations

• Levin2026.instDecidableEqCauseStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.instReprCauseStatus : Repr CauseStatus

Equations

• Levin2026.instReprCauseStatus = { reprPrec := Levin2026.instReprCauseStatus.repr }

def Levin2026.instReprCauseStatus.repr : CauseStatus → ℕ → Std.Format

Equations

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

def Levin2026.anticausativeLicensed : CauseStatus → Bool

The anticausative variant is licensed when the cause is recoverable or unknown.

Equations

• Levin2026.anticausativeLicensed Levin2026.CauseStatus.recoverableInContext = true
• Levin2026.anticausativeLicensed Levin2026.CauseStatus.identityUnknown = true
• Levin2026.anticausativeLicensed Levin2026.CauseStatus.notRecoverable = false

theorem Levin2026.recoverable_licenses : anticausativeLicensed CauseStatus.recoverableInContext = true

theorem Levin2026.unknown_licenses : anticausativeLicensed CauseStatus.identityUnknown = true

theorem Levin2026.not_recoverable_blocks : anticausativeLicensed CauseStatus.notRecoverable = false

The projectile property

The subject DP must be capable of autonomous motion: it must be able to move along the trajectory defined by the result state without requiring an external agent's sustained participation (§6).

The attested subjects qualify as "projectiles" (@cite{kearns-2000}): entities that move due to their own kinetic energy and can impart this energy to another entity through contact. This includes entities that are not machines but are construed as force-imbued (doors after a push, corks in bottles, roots in thawing soil).

The same types of entities pass the "What X did" diagnostic for effectors (fn. 17): agents, natural forces, machines, and projectiles.

inductive Levin2026.ThemeMotionCapacity : Type

Classification of the theme (subject DP).

• animate : ThemeMotionCapacity

  Self-energetic entity (agent, animal).

• machine : ThemeMotionCapacity

  Machine with independent power source (tractor, vehicle).

• projectile : ThemeMotionCapacity

  Entity imbued with force via the verbal action: after a push, the door continues to swing without the agent's involvement. Includes entities construed as moving under transferred kinetic energy (doors, corks, roots, prongs).

• requiresContinuousForce : ThemeMotionCapacity

  Entity requiring continuous external manipulation to move: nails being hammered, instruments being wielded.

@[implicit_reducible]

instance Levin2026.instDecidableEqThemeMotionCapacity : DecidableEq ThemeMotionCapacity

Equations

• Levin2026.instDecidableEqThemeMotionCapacity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.instReprThemeMotionCapacity : Repr ThemeMotionCapacity

Equations

• Levin2026.instReprThemeMotionCapacity = { reprPrec := Levin2026.instReprThemeMotionCapacity.repr }

def Levin2026.instReprThemeMotionCapacity.repr : ThemeMotionCapacity → ℕ → Std.Format

Equations

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

def Levin2026.canBeIntrPushOpenSubject : ThemeMotionCapacity → Bool

Whether a theme can serve as subject of intr-push open.

Equations

• Levin2026.canBeIntrPushOpenSubject Levin2026.ThemeMotionCapacity.animate = true
• Levin2026.canBeIntrPushOpenSubject Levin2026.ThemeMotionCapacity.machine = true
• Levin2026.canBeIntrPushOpenSubject Levin2026.ThemeMotionCapacity.projectile = true
• Levin2026.canBeIntrPushOpenSubject Levin2026.ThemeMotionCapacity.requiresContinuousForce = false

theorem Levin2026.projectile_licenses : canBeIntrPushOpenSubject ThemeMotionCapacity.projectile = true

theorem Levin2026.animate_licenses : canBeIntrPushOpenSubject ThemeMotionCapacity.animate = true

theorem Levin2026.machine_licenses : canBeIntrPushOpenSubject ThemeMotionCapacity.machine = true

theorem Levin2026.continuous_force_blocks : canBeIntrPushOpenSubject ThemeMotionCapacity.requiresContinuousForce = false

Entities requiring continuous external manipulation are blocked. "My father nailed the door shut" (§6, ex. 74) is OK, but "*The root cellar door nailed shut" (§6, ex. 75) is unacceptable.

Connection to directed motion

The same verbs appear intransitively in directed motion event descriptions (§7, examples 84–85):

• "The tennis ball slammed into the net." (84a)
• "The chair scraped across the floor." (84b)

These share the same licensing condition: the theme must be capable of autonomous motion. This provides independent support.

Note: natural forces (storm, wind) are attested as subjects of directed motion (85b) but NOT of intr-push open resultatives, because the relevant adjectives cannot be predicated of them (*an open storm/wind).

structure Levin2026.DirectedMotionDatum : Type

A directed motion event description with a surface-contact verb.

• verb : String
• sentence : String
• themeType : ThemeMotionCapacity

def Levin2026.instReprDirectedMotionDatum.repr : DirectedMotionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Levin2026.instReprDirectedMotionDatum : Repr DirectedMotionDatum

Equations

• Levin2026.instReprDirectedMotionDatum = { reprPrec := Levin2026.instReprDirectedMotionDatum.repr }

@[implicit_reducible]

instance Levin2026.instBEqDirectedMotionDatum : BEq DirectedMotionDatum

Equations

• Levin2026.instBEqDirectedMotionDatum = { beq := Levin2026.instBEqDirectedMotionDatum.beq }

def Levin2026.instBEqDirectedMotionDatum.beq : DirectedMotionDatum → DirectedMotionDatum → Bool

Equations

• Levin2026.instBEqDirectedMotionDatum.beq { verb := a, sentence := a_1, themeType := a_2 } { verb := b, sentence := b_1, themeType := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Levin2026.instBEqDirectedMotionDatum.beq x✝¹ x✝ = false

def Levin2026.ball_slammed : DirectedMotionDatum

Equations

• Levin2026.ball_slammed = { verb := "slam", sentence := "The tennis ball slammed into the net.", themeType := Levin2026.ThemeMotionCapacity.projectile }

def Levin2026.chair_scraped : DirectedMotionDatum

Equations

• Levin2026.chair_scraped = { verb := "scrape", sentence := "The chair scraped across the floor.", themeType := Levin2026.ThemeMotionCapacity.projectile }

def Levin2026.horse_banged : DirectedMotionDatum

Equations

• Levin2026.horse_banged = { verb := "bang", sentence := "The run-away horse banged into the fence.", themeType := Levin2026.ThemeMotionCapacity.animate }

def Levin2026.truck_smacked : DirectedMotionDatum

Equations

• Levin2026.truck_smacked = { verb := "smack", sentence := "The truck smacked into the retaining wall.", themeType := Levin2026.ThemeMotionCapacity.machine }

def Levin2026.directedMotionData : List DirectedMotionDatum

Equations

• Levin2026.directedMotionData = [Levin2026.ball_slammed, Levin2026.chair_scraped, Levin2026.horse_banged, Levin2026.truck_smacked]

theorem Levin2026.directed_motion_themes_autonomous : (directedMotionData.all fun (x : DirectedMotionDatum) => canBeIntrPushOpenSubject x.themeType) = true

All directed motion themes satisfy the autonomous motion condition, paralleling intr-push open.

Natural forces (storm, wind) are attested as directed motion subjects — (85b) "The storm swept through the valley" — but NOT in intr-push open resultatives. The blocking mechanism is the adjective restriction: the relevant adjectives cannot be predicated of natural forces (*an open storm), so no licensed verb–adjective combination exists. The theme passes the autonomous motion test but the adjective filter blocks it independently.

The licensing conjunction

An intr-push open resultative is licensed iff ALL of:

1. The verb is from a force-application class (§12, §18)
2. The adjective describes a spatially instantiated state
3. The discourse context licenses cause suppression
4. The theme is capable of autonomous motion

def Levin2026.isLicensed (verbClass : Semantics.Lexical.LevinClass) (adj : Fragments.English.Predicates.Adjectival.AdjectivalPredicateEntry) (causeStatus : CauseStatus) (theme : ThemeMotionCapacity) : Bool

Full licensing check for an intr-push open resultative.

Equations

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

theorem Levin2026.door_pushed_open_licensed : isLicensed Semantics.Lexical.LevinClass.pushPull Fragments.English.Predicates.Adjectival.open_ CauseStatus.recoverableInContext ThemeMotionCapacity.projectile = true

"The door pushed open" in a recoverable-cause context is licensed.

theorem Levin2026.door_pushed_open_licensed_unknown : isLicensed Semantics.Lexical.LevinClass.pushPull Fragments.English.Predicates.Adjectival.open_ CauseStatus.identityUnknown ThemeMotionCapacity.projectile = true

"The door pushed open" in a cause-unknown context is licensed.

theorem Levin2026.blocked_no_context : isLicensed Semantics.Lexical.LevinClass.pushPull Fragments.English.Predicates.Adjectival.open_ CauseStatus.notRecoverable ThemeMotionCapacity.projectile = false

Blocked: cause not recoverable.

theorem Levin2026.blocked_continuous_force : isLicensed Semantics.Lexical.LevinClass.pushPull Fragments.English.Predicates.Adjectival.open_ CauseStatus.recoverableInContext ThemeMotionCapacity.requiresContinuousForce = false

Blocked: theme requires continuous force (PCC).

theorem Levin2026.blocked_wrong_verb_class : isLicensed Semantics.Lexical.LevinClass.break_ Fragments.English.Predicates.Adjectival.open_ CauseStatus.recoverableInContext ThemeMotionCapacity.projectile = false

Blocked: verb class wrong (break is a CoS verb, not force).

theorem Levin2026.blocked_wrong_adjective : isLicensed Semantics.Lexical.LevinClass.pushPull Levin2026.red_✝ CauseStatus.recoverableInContext ThemeMotionCapacity.projectile = false

End-to-end: the full argument chain

1. push is pushPull (§12) → pure manner, no CoS, no causation
2. No causative alternation for pushPull alone (meaning-component prediction)
3. Fusion: resultative construction adds CoS + causation → composed meaning now predicts the causative alternation
4. Resultative construction adds CAUSE (non-empty CausalDynamics)
5. Constructional BECOME = inception (CoSType.inception)
6. Constructional CAUSE = .make (sufficiency, completion event)
7. Anticausative: cause suppressed under discourse licensing
8. PCC: projectile has independent energy → cause not continuously needed
9. Theme passes autonomous-motion check → anticausative OK

theorem Levin2026.end_to_end_push_open : Semantics.Lexical.LevinClass.pushPull.participatesIn Semantics.Lexical.DiathesisAlternation.causativeInchoative = false ∧ (Semantics.Lexical.LevinClass.pushPull.rootEntailments == Semantics.Lexical.Roots.RootEntailments.pureManner) = true ∧ ConstructionGrammar.predictedAlternationInConstruction Semantics.Lexical.LevinClass.pushPull.meaningComponents ConstructionGrammar.resultative Semantics.Lexical.DiathesisAlternation.causativeInchoative = true ∧ (resultativeBECOME == Features.ChangeOfState.CoSType.inception) = true ∧ (Semantics.Causation.Resultatives.resultativeCausativeBuilder == Features.Causative.make) = true ∧ anticausativeLicensed CauseStatus.recoverableInContext = true ∧ canBeIntrPushOpenSubject ThemeMotionCapacity.projectile = true

FilledResultative: bundling lexical material with the construction

The construction grammar layer (MeaningComponents, fusion, alternation prediction) carries the structural content. FilledResultative bundles the lexical fillers as proof obligations on the type — the filling must satisfy the Boolean-level alternation prediction.

This is the formal reflex of @cite{levin-2026}'s analysis: a resultative is a construction filled with specific lexical material (verb class, adjective).

The structural-causation layer for these resultatives lives in §7 below on the BoolSEM substrate (see HammerFlat, KickIntoField, etc.). Linking a specific FilledResultative to its BoolSEM model would be a separate study extension.

structure Levin2026.FilledResultative : Type

A resultative construction instantiated with its lexical fillers.

• verbClass : Semantics.Lexical.LevinClass

  The verb's Levin class (manner root)

• adjective : Fragments.English.Predicates.Adjectival.AdjectivalPredicateEntry

  The result-state adjective (from Fragment)

• construction : ConstructionGrammar.ArgStructureConstruction

  The argument structure construction (typically resultative)

• alternationPredicted : ConstructionGrammar.predictedAlternationInConstruction self.verbClass.meaningComponents self.construction Semantics.Lexical.DiathesisAlternation.causativeInchoative = true

  The construction adds what the verb lacks: fusion predicts the causative alternation for the composed meaning.

• adjSpatial : self.adjective.spatialConfigType.isSome = true

  The adjective describes a spatially instantiated state.

def Levin2026.FilledResultative.canAnticausativize (fr : FilledResultative) (cause : CauseStatus) (theme : ThemeMotionCapacity) : Bool

Whether this filled resultative can surface as an anticausative (intr-push open), given discourse and theme conditions. Checks the verb class restriction in addition to discourse/theme.

Equations

• fr.canAnticausativize cause theme = (Levin2026.intrPushOpenClasses.contains fr.verbClass && Levin2026.anticausativeLicensed cause && Levin2026.canBeIntrPushOpenSubject theme)

Concrete instances

def Levin2026.pushOpen_filled : FilledResultative

Equations

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

def Levin2026.pullFree_filled : FilledResultative

Equations

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

def Levin2026.slamShut_filled : FilledResultative

Equations

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

FilledResultative → licensing

The isLicensed function and the FilledResultative type encode the same conditions from different angles. isLicensed is a flat Boolean check; FilledResultative bundles the conditions as proof obligations. The bridge theorem shows they agree: any FilledResultative with appropriate discourse and theme conditions passes isLicensed.

theorem Levin2026.filled_implies_licensed (fr : FilledResultative) (cause : CauseStatus) (theme : ThemeMotionCapacity) (hClass : intrPushOpenClasses.contains fr.verbClass = true) (hCause : anticausativeLicensed cause = true) (hTheme : canBeIntrPushOpenSubject theme = true) : isLicensed fr.verbClass fr.adjective cause theme = true

A FilledResultative whose verb class is in intrPushOpenClasses passes isLicensed for any licensed cause status and theme.

theorem Levin2026.pushOpen_filled_licensed : isLicensed pushOpen_filled.verbClass pushOpen_filled.adjective CauseStatus.recoverableInContext ThemeMotionCapacity.projectile = true

Concrete: pushOpen_filled passes isLicensed in a recoverable-cause, projectile context.

theorem Levin2026.pushOpen_anticausative_licensed : pushOpen_filled.canAnticausativize CauseStatus.recoverableInContext ThemeMotionCapacity.projectile = true

The anticausative of pushOpen_filled is licensed in the right discourse context.

theorem Levin2026.pushOpen_anticausative_blocked_no_context : pushOpen_filled.canAnticausativize CauseStatus.notRecoverable ThemeMotionCapacity.projectile = false

The anticausative is blocked when the cause is not recoverable.

theorem Levin2026.pushOpen_anticausative_blocked_continuous : pushOpen_filled.canAnticausativize CauseStatus.recoverableInContext ThemeMotionCapacity.requiresContinuousForce = false

The anticausative is blocked when the theme requires continuous force.

FilledResultative ↔ end-to-end chain

The end_to_end_push_open theorem proved 9 conjuncts individually. pushOpen_filled encodes three of those (alternation prediction, spatial adjective, causal consistency) as proof obligations on the type. The remaining conditions (discourse, theme) are runtime parameters.

theorem Levin2026.pushOpen_filled_covers_core : ConstructionGrammar.predictedAlternationInConstruction pushOpen_filled.verbClass.meaningComponents pushOpen_filled.construction Semantics.Lexical.DiathesisAlternation.causativeInchoative = true ∧ pushOpen_filled.adjective.spatialConfigType.isSome = true

pushOpen_filled subsumes the core of end_to_end_push_open: the type's proof obligations cover the alternation prediction and the spatial-adjective step.

Connection to ResultativeType

Intr-push open resultatives are anticausativeProperty in the Goldberg & Jackendoff typology (added to ResultativeType for @cite{levin-2026}). This closes the loop between the FilledResultative type and the broader resultative classification.

def Levin2026.filledToResultativeType : FilledResultative → Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.ResultativeType

Map a FilledResultative to its ResultativeType. All intr-push open resultatives are anticausative property resultatives: the verb is transitive-only, the adjective heads a property result phrase, and the cause is suppressed. The transitive counterpart (tr-push open) would be causativeProperty, but is modeled separately.

Equations

• Levin2026.filledToResultativeType x✝ = Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.ResultativeType.anticausativeProperty

theorem Levin2026.anticausative_not_noncausative : filledToResultativeType pushOpen_filled ≠ Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.ResultativeType.noncausativeProperty

Anticausative property is distinct from noncausative property (freeze solid): the former has a suppressed cause, the latter has no constructional cause at all.

Mandarin cognate

The paper (§1) motivates the English analysis by drawing parallels to Mandarin, where the verb tuī "push" similarly cannot occur intransitively outside resultative constructions (example 4: tuī fān "push-upend"; examples 5–6 show tuī alone cannot appear intransitively). The Mandarin cognate compound tuī-kāi "push-open" exists as a V-V compound in the Fragment — this bridge connects it to the English analysis.

theorem Levin2026.mandarin_tui_kai_is_cognate : Fragments.Mandarin.Resultatives.tui_kai.gloss = "push-open" ∧ Fragments.Mandarin.Resultatives.tui_kai.orientation = Semantics.Causation.Resultatives.ResultOrientation.objectOriented

The Mandarin push-open compound is the cross-linguistic cognate: same verb meaning (push), same result meaning (open), object-oriented.

theorem Levin2026.resultative_cause_matches_make_verb : Fragments.English.Predicates.Verbal.make.causative = some Semantics.Causation.Resultatives.resultativeCausativeBuilder

Resultative CAUSE matches the Fragment entry for "make".

theorem Levin2026.resultative_cause_differs_from_cause_verb : Fragments.English.Predicates.Verbal.cause.causative ≠ some Semantics.Causation.Resultatives.resultativeCausativeBuilder

Resultative CAUSE ≠ "cause" verb (.make ≠ .cause).

Per-scenario causal models

Each causative resultative maps to a concrete BoolSEM V where the verbal subevent causally determines the result vertex. Sufficiency and completion are stated via the canonical BoolSEM.causallySufficientOn / completesForEffectOn predicates so kernel reduction closes the structural theorems via unfold + rfl.

Per-scenario inductive V enums give Fintype + DecidableEq + Repr so developDetOn reduces structurally without native_decide.

inductive Levin2026.HammerFlat.V : Type

• hammering : V
• flat : V

@[implicit_reducible]

instance Levin2026.HammerFlat.instDecidableEqV : DecidableEq V

Equations

• Levin2026.HammerFlat.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.HammerFlat.instFintypeV : Fintype V

Equations

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

def Levin2026.HammerFlat.instReprV.repr : V → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Levin2026.HammerFlat.instReprV : Repr V

Equations

• Levin2026.HammerFlat.instReprV = { reprPrec := Levin2026.HammerFlat.instReprV.repr }

def Levin2026.HammerFlat.varList : List V

Equations

• Levin2026.HammerFlat.varList = [Levin2026.HammerFlat.V.hammering, Levin2026.HammerFlat.V.flat]

def Levin2026.HammerFlat.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Levin2026.HammerFlat.model : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Levin2026.HammerFlat.instIsDeterministicVBoolModel : Core.Causal.SEM.IsDeterministic model

Equations

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

theorem Levin2026.HammerFlat.hammer_sufficient_for_flat : model.causallySufficientOn varList Core.Causal.Valuation.empty 1 V.hammering V.flat

theorem Levin2026.HammerFlat.hammer_completes_flat : model.completesForEffectOn varList Core.Causal.Valuation.empty 1 V.hammering V.flat

inductive Levin2026.KickIntoField.V : Type

• kicking : V
• in_field : V

@[implicit_reducible]

instance Levin2026.KickIntoField.instDecidableEqV : DecidableEq V

Equations

• Levin2026.KickIntoField.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.KickIntoField.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Levin2026.KickIntoField.instReprV : Repr V

Equations

• Levin2026.KickIntoField.instReprV = { reprPrec := Levin2026.KickIntoField.instReprV.repr }

def Levin2026.KickIntoField.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Levin2026.KickIntoField.varList : List V

Equations

• Levin2026.KickIntoField.varList = [Levin2026.KickIntoField.V.kicking, Levin2026.KickIntoField.V.in_field]

def Levin2026.KickIntoField.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Levin2026.KickIntoField.model : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Levin2026.KickIntoField.instIsDeterministicVBoolModel : Core.Causal.SEM.IsDeterministic model

Equations

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

theorem Levin2026.KickIntoField.kick_sufficient_for_field : model.causallySufficientOn varList Core.Causal.Valuation.empty 1 V.kicking V.in_field

theorem Levin2026.KickIntoField.kick_completes_field : model.completesForEffectOn varList Core.Causal.Valuation.empty 1 V.kicking V.in_field

inductive Levin2026.LaughSilly.V : Type

• laughing : V
• silly : V

@[implicit_reducible]

instance Levin2026.LaughSilly.instDecidableEqV : DecidableEq V

Equations

• Levin2026.LaughSilly.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.LaughSilly.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Levin2026.LaughSilly.instReprV : Repr V

Equations

• Levin2026.LaughSilly.instReprV = { reprPrec := Levin2026.LaughSilly.instReprV.repr }

def Levin2026.LaughSilly.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Levin2026.LaughSilly.varList : List V

Equations

• Levin2026.LaughSilly.varList = [Levin2026.LaughSilly.V.laughing, Levin2026.LaughSilly.V.silly]

def Levin2026.LaughSilly.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Levin2026.LaughSilly.model : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Levin2026.LaughSilly.instIsDeterministicVBoolModel : Core.Causal.SEM.IsDeterministic model

Equations

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

theorem Levin2026.LaughSilly.laugh_sufficient_for_silly : model.causallySufficientOn varList Core.Causal.Valuation.empty 1 V.laughing V.silly

"The river froze solid" — noncausative resultative. Empty graph captures the absence of constructional CAUSE.

inductive Levin2026.FreezeSolid.V : Type

• freezing : V
• solid : V

@[implicit_reducible]

instance Levin2026.FreezeSolid.instDecidableEqV : DecidableEq V

Equations

• Levin2026.FreezeSolid.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.FreezeSolid.instFintypeV : Fintype V

Equations

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

def Levin2026.FreezeSolid.instReprV.repr : V → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Levin2026.FreezeSolid.instReprV : Repr V

Equations

• Levin2026.FreezeSolid.instReprV = { reprPrec := Levin2026.FreezeSolid.instReprV.repr }

def Levin2026.FreezeSolid.varList : List V

Equations

• Levin2026.FreezeSolid.varList = [Levin2026.FreezeSolid.V.freezing, Levin2026.FreezeSolid.V.solid]

def Levin2026.FreezeSolid.graph : Core.Causal.CausalGraph V

Empty graph: no causal relations (noncausative resultative).

Equations

• Levin2026.FreezeSolid.graph = { parents := fun (x : Levin2026.FreezeSolid.V) => ∅ }

noncomputable def Levin2026.FreezeSolid.model : Core.Causal.BoolSEM V

Equations

• Levin2026.FreezeSolid.model = { graph := Levin2026.FreezeSolid.graph, mech := fun (x : Levin2026.FreezeSolid.V) => Core.Causal.Mechanism.const false }

@[implicit_reducible]

noncomputable instance Levin2026.FreezeSolid.instIsDeterministicVBoolModel : Core.Causal.SEM.IsDeterministic model

Equations

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

theorem Levin2026.FreezeSolid.freeze_not_sufficient : ¬model.causallySufficientOn varList Core.Causal.Valuation.empty 1 V.freezing V.solid

Freezing is NOT sufficient for solidity in the empty-edge model.

"Drink the teapot dry" — passive chain: drinking → tea_removal → teapot_dry. Tight because tea_removal has no independent source.

inductive Levin2026.DrinkTeapotDry.V : Type

• drinking : V
• tea_removal : V
• teapot_dry : V

@[implicit_reducible]

instance Levin2026.DrinkTeapotDry.instDecidableEqV : DecidableEq V

Equations

• Levin2026.DrinkTeapotDry.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.DrinkTeapotDry.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Levin2026.DrinkTeapotDry.instReprV : Repr V

Equations

• Levin2026.DrinkTeapotDry.instReprV = { reprPrec := Levin2026.DrinkTeapotDry.instReprV.repr }

def Levin2026.DrinkTeapotDry.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Levin2026.DrinkTeapotDry.varList : List V

Equations

• Levin2026.DrinkTeapotDry.varList = [Levin2026.DrinkTeapotDry.V.drinking, Levin2026.DrinkTeapotDry.V.tea_removal, Levin2026.DrinkTeapotDry.V.teapot_dry]

def Levin2026.DrinkTeapotDry.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Levin2026.DrinkTeapotDry.model : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Levin2026.DrinkTeapotDry.instIsDeterministicVBoolModel : Core.Causal.SEM.IsDeterministic model

Equations

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

theorem Levin2026.DrinkTeapotDry.drink_completes_dry : model.completesForEffectOn varList Core.Causal.Valuation.empty 1 V.drinking V.teapot_dry

Tight despite being a chain: removing drinking leaves tea_removal undetermined (no independent source), so teapot_dry doesn't fire.

inductive Levin2026.KickDoorDirect.V : Type

• kicking : V
• door_open : V

@[implicit_reducible]

instance Levin2026.KickDoorDirect.instDecidableEqV : DecidableEq V

Equations

• Levin2026.KickDoorDirect.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.KickDoorDirect.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Levin2026.KickDoorDirect.instReprV : Repr V

Equations

• Levin2026.KickDoorDirect.instReprV = { reprPrec := Levin2026.KickDoorDirect.instReprV.repr }

def Levin2026.KickDoorDirect.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Levin2026.KickDoorDirect.varList : List V

Equations

• Levin2026.KickDoorDirect.varList = [Levin2026.KickDoorDirect.V.kicking, Levin2026.KickDoorDirect.V.door_open]

def Levin2026.KickDoorDirect.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Levin2026.KickDoorDirect.model : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Levin2026.KickDoorDirect.instIsDeterministicVBoolModel : Core.Causal.SEM.IsDeterministic model

Equations

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

theorem Levin2026.KickDoorDirect.kick_door_completes_direct : model.completesForEffectOn varList Core.Causal.Valuation.empty 1 V.kicking V.door_open

NOT-tight case: kick → ball_motion → door_open + ball_energy → ball_motion. Ball has its own independent energy source, so kicking is not necessary for door_open in this model.

*In our model*, parallel mechanisms break but-for necessity. This
is an illustration of the general independent-source phenomenon
rather than a direct formalization of any specific paper's
sentence-licensing argument. 

inductive Levin2026.IndependentSourceBreaksNecessity.V : Type

• kicking : V
• ball_motion : V
• ball_energy : V
• door_open : V

@[implicit_reducible]

instance Levin2026.IndependentSourceBreaksNecessity.instDecidableEqV : DecidableEq V

Equations

• Levin2026.IndependentSourceBreaksNecessity.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Levin2026.IndependentSourceBreaksNecessity.instFintypeV : Fintype V

Equations

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

@[implicit_reducible]

instance Levin2026.IndependentSourceBreaksNecessity.instReprV : Repr V

Equations

• Levin2026.IndependentSourceBreaksNecessity.instReprV = { reprPrec := Levin2026.IndependentSourceBreaksNecessity.instReprV.repr }

def Levin2026.IndependentSourceBreaksNecessity.instReprV.repr : V → ℕ → Std.Format

Equations

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

def Levin2026.IndependentSourceBreaksNecessity.varList : List V

Equations

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

def Levin2026.IndependentSourceBreaksNecessity.graph : Core.Causal.CausalGraph V

Equations

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

noncomputable def Levin2026.IndependentSourceBreaksNecessity.model : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance Levin2026.IndependentSourceBreaksNecessity.instIsDeterministicVBoolModel : Core.Causal.SEM.IsDeterministic model

Equations

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

def Levin2026.IndependentSourceBreaksNecessity.ballHasEnergyBg : Core.Causal.Valuation fun (x : V) => Bool

Equations

• Levin2026.IndependentSourceBreaksNecessity.ballHasEnergyBg = Core.Causal.Valuation.empty.extend Levin2026.IndependentSourceBreaksNecessity.V.ball_energy true

theorem Levin2026.IndependentSourceBreaksNecessity.independent_source_breaks_necessity : ¬model.completesForEffectOn varList ballHasEnergyBg 1 V.kicking V.door_open

NOT tight: removing kicking still allows ball_energy → ball_motion → door_open. The kick is not necessary.